Abstract
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.