PhD Defense
Pierre-Alain Reynier
Title of the thesis
Verification of timed and distributed systems:
models, algorithms and implementability.
Day and location
Thursday June 21st in Cachan at 2pm.
Salle Condorcet, Bâtiment D'Alembert, École Normale Supérieure
de Cachan.
Access
Composition of the jury
Abstract of the thesis
With the development of computer science, the number and the role of critical systems
always grow. A large part of these systems presents timing aspects expressing some
quantitative constraints on time elapsing. The results presented in this thesis fall into
the framework of automated verification of distributed and timed systems. We consider
different models obtained as extensions of timed automata and Petri nets. In a first
part, we study these models both independently, proving new undecidability results for
timed automata with silent transitions, and by looking at links between them.
We propose a translation from extended timed automata to time Petri nets, and compare
relative expressive power of timed automata and timed Petri nets. The second part of our
work deals with problems in algorithmic of verification. We propose an algorithm for
forward analysis of timed automata with diagonal constraints, and a notion of unfolding
for networks of timed automata together with different methods for building a finite and
complete prefix of it. Finally, we are interested in a notion of implementability for timed
automata and propose an algorithm for robust verification of linear temporal logic.
Keywords
Formal verification, Timed automata, Petri nets, Distributed systems, Expressivity, Algorithmic, Implementability.
Homepage of Pierre-Alain Reynier