Timed automaton

In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton. Further, clocks can be reset. Timed automata are a sub-class of a type hybrid automata. Timed automata can be used to model and analyse the timing behavior of computer systems, e.g., real-time systems or networks. Methods for checking both safety and liveness properties have been developed and intensively studied over the last 20 years. It has been shown that the state reachability problem for timed automata is decidable, which makes this an interesting sub-class of hybrid automata. Extensions have been extensively studied, among them stopwatches, real-time tasks, cost functions, and timed games. There exists a variety of tools to input and analyse timed automata and extensions, including the model checkers UPPAAL, Kronos, and the schedulability analyser TIMES. These tools are becoming more and more mature, but are still all academic research tools. Before formally defining what a timed automaton is, some examples are given. Consider the language of timed words over the unary alphabet such that there is an during the first time unit, and there is less than one time unit between two successive . A timed automaton recognizing this language, pictured nearby, uses a single clock , which should never be equal to one. This clock counts the time since the start of the run if no were emitted, or from the last emitted otherwise. This means that each time an is emitted, this clock is reset to zero. Consider the language of timed words over the binary alphabet such that each is followed by a in the next time unit. The timed automaton recognizing this language, pictured nearby, recalls whether or not there was an that was not yet followed by a .