Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Second Annual IEEE Symposium on

Logic in Computer Science (LICS 1987)

Paper: On the Eventuality Operator in Temporal Logic (at LICS 1987)

Authors: A. Prasad Sistla Lenore D. Zuck

Abstract

We consider RTL, a linear time propositional temporal logic whose only modalities are the ◊ (eventually) operator and its dual - □ (always). Although less expressive than the full temporal logic, RTL is the fragment of temporal logic that is used most often and in many verification systems. Indeed, most properties of distributed systems discussed in the literature are RTL properties. Another advantage of RTL over the full temporal logic is in the decidability procedure; while deciding satisfiability of a formula in full temporal logic is a PSPACE complete procedure, doing that for an RTL formula is in co-NP. We characterize the class of ω-regular languages that are definable in RTL and show simple translations between ω-regular sets and RTL formulae that define them. We explore the applications of RTL in reasoning about communication systems and the relationship between RTL and several fragments of Interval Modal Logic.

BibTeX

  @InProceedings{SistlaZuck-OntheEventualityOpe,
    author = 	 {A. Prasad Sistla and Lenore D. Zuck},
    title = 	 {On the Eventuality Operator in Temporal Logic},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {153--166},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski