Logics, Automata and Classical Theories for Deciding Real Time
Jean-Francois Raskin - April 99

Abstract



In the theory underlying the automatic verification of reactive systems a class of languages, called ``the omega regular languages'', plays a central role. The omega regular languages are identified by formalisms from modal logic, like the linear temporal logic, from automata theory, like Buchi automata, and by classical theories, like the first and second order monadic logics. This class of languages and the formalisms that identify it have been intensively studied since the early seventies. A large number of interesting results are known about those formalisms, for example, they are all closed under all boolean operations and fully decidable, i.e. their satisfiability and validity problems are decidable.

Those formalisms are able to express qualitative temporal properties about executions of reactive systems, e.g. proper ordering between events. On the other hand, they can not be used to express quantitative temporal properties, for example a constraint on the amount of time between two events.

The formalisms that are able to specify quantitative real-time properties are called real-time formalisms. The real-time formalisms define classes of real-time languages. The properties of those languages are still not fully understood.
Several real-time formalisms have been proposed in the literature but those formalisms have drawbacks: undecidability problems, non closure under negation, etc. In this PhD thesis, we try to overcome some of those problems by proposing  a new family of real-time formalisms.

The logics, automata and classical theories that we propose here are (fully) decidable and closed under all boolean operations.
The expressiveness of those formalisms is studied and compared to the expressiveness of other real-time formalisms proposed in the literature. In particular, we show that those new formalisms identify a class of real-time languages that we propose to call, by analogy with the untimed case, the real-time omega regular languages. The problem of complete axiomatization of the logics that identify those languages is studied and solved.



If you are interested in a copy of the thesis or in obtaining the postscript file of the text, please let me know by email:
Jean-Francois Raskin.