Efficient Verification of Timed Automata

Advisors : F. Herbreteau, and I. Walukiewicz
Institution : Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Team : Formal Methods, Modelling and Verification group

Keywords

Real-time Systems, Model-checking, Timed Automata, Algorithmics.

Description

Timed automata[1] are finite automata extended with clocks that can be reset and tested on the transitions. Clocks hence measure the delay between actions of the automaton. Timed automata are widely used to model real-time systems and for model-checking real-time specifications.

Clocks are real-valued variables, hence the state-space of a timed automaton is infinite (and even not countable). To overcome this problem, verification algorithms use a symbolic representation of the executions of the automaton. The symbolic representation must further be abstracted[2] in order to guarantee its finiteness. The efficiency of the verification algorithms heavily rely on the coarseness of the abstraction[3].

These last years, we have proposed several optimizations of the abstractions and the underlying algorithms[4,5,6,7,8,9]. The goals of this thesis are:

Bibliography