Determinizing timed automata.

Nathalie Bertrand
INRIA Rennes Bretagne Atlantique
Friday, 20 May, 2011 - 14:00

Timed automata are frequently used to model real-time systems. Essentially timed automata are an extension of finite automata with guards and resets of continuous variables (called clocks) evolving at the same pace. They are extensively used in the context of validation of real-time systems. One of the reasons for this popularity is that, despite the fact that they represent infinite state systems, their reachability is decidable, thanks to the construction of the region graph abstraction.

As for other models, determinization is a key issue for several validation problems, such as monitoring, implementability and testing. However, not all timed automata can be determinized, and determinizability itself is undecidable. After introducing timed automata, we will review existing approaches to get round their unfeasible determinization. Then we will expose a novel game-based algorithm which, given a timed automaton, produces either a deterministic equivalent or a deterministic over-approximation, and which subsumes all other known contributions.