Timed alternating finite automata

Summary form only given. Traditionally, finite state automata are untimed or asynchronous models of computation in which only the ordering of events, not the time at which events occur, would affect the result of a computation. For real-time systems, it is important to augment these models of computation with a notion of time. We introduce timed alternating finite automata (TAFA), a class of alternating finite automata (AFA) extended with a finite set of real-valued clocks. We present an algebraic interpretation of TAFA, which parallels that of timed regular expressions and language equations. We further extend the equational representation of AFA to describe timed alternating finite automata, and explore solutions for such equations over time languages.