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

**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} }