top

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.

Download: [pdf] 

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

BibTeX: (download)

@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},
  address = {Los Alamitos, CA},
  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