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