## Real-time logics: complexity and expressiveness

R. Alur and T. Henzinger. Real-time logics: complexity and expressiveness. In Fifth Annual IEEE Symposium on Logic in Computer Science (Philadelphia, PA, 1990), pp. 390–401, IEEE Comput. Soc. Press, Los Alamitos, CA, 1990.

#### Abstract:

A theory of timed state sequences is introduced as a symbiosis of a theory of discrete time and of the theory of the natural numbers with linear order and monadic predicates, put together via a monotone function that maps every state (natural number) to its "time". The theory is shown to be (nonelementarily) decidable, and its expressive power is characterized by $&oslash;mega$-regular sets, in contrast to many more expressive variants that are shown to be highly undecidable (with the validity problem being $\Pi\sp 1\sb 1$-complete). This implies that most real-time logics proposed in the literature cannot be decided. Further, however, two elementary (EXPSPACE-complete) real-time temporal logics, the so-called TPTL and MTL$\sb \rm P$, are identified as expressively complete fragments of the theory of timed state sequences. Out of that the authors conclude that these two logics are well suited for the specification and verification of real-time systems.

@INCOLLECTION{alur90:_real,
author = {R. Alur and T. Henzinger},
title = {Real-time logics: complexity and expressiveness},
booktitle = {Fifth Annual IEEE Symposium on Logic in Computer Science (Philadelphia,
PA, 1990)},
publisher = {IEEE Comput. Soc. Press},
year = {1990},
pages = {390--401},
abstract = {
A theory of timed state sequences is introduced as a symbiosis of
a theory of discrete time and of the theory of the natural numbers
with linear order and monadic predicates, put together via a monotone
function that maps every state (natural number) to its "time".
The theory is shown to be (nonelementarily) decidable, and its expressive
power is characterized by $\omega$-regular sets, in contrast to many
more expressive variants that are shown to be highly undecidable
(with the validity problem being $\Pi\sp 1\sb 1$-complete). This
implies that most real-time logics proposed in the literature cannot
be decided.
Further, however, two elementary (EXPSPACE-complete) real-time temporal
logics, the so-called TPTL and MTL$\sb {\rm P}$, are identified as
expressively complete fragments of the theory of timed state sequences.
Out of that the authors conclude that these two logics are well suited
for the specification and verification of real-time systems. }
}


Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33

Hybrid Logics
Resources