1993-1996: PhD Thesis.

My work (under the supervision of Prof. Olivier Roux ) consisted in using and adapting existing formalisms for the verification of ELECTRE programs. I started by searching for results in the literature, among which the following is most relevant for our topic: model checking of the temporal logic TCTL is decidable on timed automata, but it is undecidable for hybrid automata. The logic TCTL is suitable for expressing most properties of interest for ELECTRE programs. But for modeling the programs themselves, we need a subclass of hybrid automata that strictly includes timed automata. This is because timed automata may only have continuously running clocks, while the ``task-preemption'' operation in ELECTRE does require ``freezing'' of clocks. Therefore, my work consisted in finding a subclass of hybrid automata expressive enough for modeling ELECTRE programs, while still decidable for a fragment of TCTL powerful enough to express time-critical properties. This lead to defining the so-called strongly non-Zeno hybrid automata, characterized by the following: all cyclic runs have a minimal duration uniformly low-bounded by some strictly positive real, and all finite runs can be continued at infinity. I have then obtained:
Vlad Rusu