Stutter-Invariant Languages, omega-Automata, and Temporal Logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Temporal logic and ω-automata are two ofthe common frameworks for specifying properties of reactive systems in modern verification tools. In this paper we unify these two frameworks in the linear time setting for the specification of stutter-invariant properties, which are used in the context ofpartial-order verification. We will observe a simple variant oflinear time propositional temporal logic (LTL) for expressing exactly the stutter-invariant ω-regular languages. The complexity of, and algorithms for, all the relevant decision procedures for this logic remain essentially the same as with ordinary LTL. In particular, satisfiability remains PSPACE-complete and temporal formulas can be converted to at most exponential sized ω-automata. More importantly, we show that the improved practical algorithms for conversion ofL TL formulas to automata, used in model-checking tools such as SPIN, which typically produce much smaller than worst-case output, can be modified to incorporate this extension to LTL with the same benefits. In this way, the specification mechanism in temporal logic-based tools that employ partial-order reduction can be extended to incorporate all stutter-invariant ω-regular properties.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings
PublisherSpringer Berlin Heidelberg
Pages236-248
Number of pages13
Volume1633
ISBN (Electronic)978-3-540-48683-1
ISBN (Print)978-3-540-66202-0
DOIs
Publication statusPublished - 1999

Fingerprint Dive into the research topics of 'Stutter-Invariant Languages, omega-Automata, and Temporal Logic'. Together they form a unique fingerprint.

Cite this