Logic in Computer Science (LICS 1990)

Paper: On the limits of efficient temporal decidability (at LICS 1990)

Authors: Emerson, E.A. Evangelist, M. Srinivasan, J.

Abstract

An analysis is made of the contribution of the temporal operators alone to the complexity of deciding temporal logics by suppressing the role the usual Boolean connectives play in determining lower bounds on the complexity of their decision procedures. Several temporal logics are exhibited which can state many properties useful in describing temporal systems and which restrict combinations of temporal and Boolean operators so as to be decidable in low deterministic polynomial time. It is also shown that relaxing any of the constraints placed on the syntax of these logics results in intractability, thereby demonstrating that there is a fine line separating tractably decidable sets of temporal formulas from intractable ones

BibTeX

  @InProceedings{EmersonEvangelistSr-Onthelimitsofeffici,
    author = 	 {Emerson, E.A. and Evangelist, M. and Srinivasan, J.},
    title = 	 {On the limits of efficient temporal decidability},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {464--475},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }