Seminar details
Abstract: 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.
