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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. R. Büchi. On a decision method in restricted second-order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science, 1960. Stanford University Press, 1962.
E. A. Emerson. Temporal and modal logics. In J. van Leeuwen, editor, Handbook of Theoret. Comput. Sci., volume B, pages 995–1072. Elsevier, Amsterdam, 1990.
K. Etessami. Stutter-invariant languages, ω-automata, and temporal logic. Technical Report BL011272-980611-07TM, Bell Laboratories, June 11 1998.
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification oflinear temporal logic. In PSTV95, Protocol Specification Testing and Verification, pages 3–18, 1995.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proc. 6th Ann. IEEE Symp. on Logic in Computer Science, pages 406–415, 1991.
G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.
G. J. Holzmann and D. Peled. An improvement in formal verification. In 7th International Conference on Formal Description Techniques, pages 177–194, 1994.
O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. Journal of Logic and Computation, 7:1–14, 1997.
L. Lamport. What good is temporal logic. In R. E. A. Mason, editor, Information Processing’ 83: Proc. IFIP 9th World Computer Congress, pages 657–668, 1983.
L. Lamport. The temporal logic ofactions. ACM Transactions on Programming Languages and Systems, pages 872–923, 1994.
Z. Manna and A. Pnueli. Specification and verification ofconcurren t programs by ω-automata. In Proc. 14th Ann. ACM Symp. on Principles of Programming Languages, pages 1–12, 1987.
K. McMillan, 1998. See http://www-cad.eecs.berkeley.edu/kenmcmil for recent versions ofSMV and its documentation.
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.
D. Peled. Combining partial order reductions with on-the-fly model checking. Formal Methods in System Design, 8:39–64, 1996.
D. Peled and T. Wilke. Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters, 63:243–246, 1997.
A. Pnueli. The temporal logic ofprograms. In Proc. 18th Symp. on Foundations of Computer Science, pages 46–57, 1977.
A. Rabinovich. Expressive completeness oftemp oral logic ofactions. In Mathematical Foundations of Computer Science, pages 229–238, August 1998.
A. P. Sistla and E. M. Clarke. The complexity ofprop ositional linear temporal logics. Journal of the ACM, 32(3):733–749, 1985.
A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.
Thomas, W. Classifying regular events in symbolic logic. Journal of Computer and System Sciences, 25:360–376, 1982.
A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1:297–322, 1992.
M. Y. Vardi and P. Wolper. Reasoning about infinite computation. Information and Computation, 115:1–37, 1994.
Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56:72–99, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Etessami, K. (1999). Stutter-Invariant Languages, ω-Automata, and Temporal Logic. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_22
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive