Abstract
Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only, as was shown by Muller et al., can they be used to obtain optimal decision procedures, but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking, and has enabled us to derive improved space complexity bounds for this long-standing problem.
The work of this author was supported by the Esprit BRA action REACT and by the Belgian Incentive Program “Information Technology” — Computer Science of the future, initiated by the Belgian State — Prime Minister's Office — Science Policy Office. Scientific responsibility is assumed by its authors.
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
C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. on Database Systems, 5:241–259, 1980.
O. Bernholtz and O. Grumberg. Branching time temporal logic and amorphous tree automata. In Proc. 4th Conferance on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 262–277, Hildesheim, August 1993. Springer-Verlag.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.
R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal Μ-calculus. Formal Methods in System Design, 2:121–147, 1993.
C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
E. A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, oct 1988.
E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science, pages 368–377, San Juan, Oct 1991.
E. A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of Μ-calculus. In Computer Aided Verification, Proc. 5th Int. Workshop, volume 697, pages 385–396, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. Workshop on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79–87. Springer-Verlag, 1985.
E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pages 997–1072, 1990.
E.A. Emerson. Automated temporal reasoning about reactive systems. In VIII-th BANFF Higher Order Workshop, 1994. unpublished abstract of forthcoming talk.
A.E. Emerson and A.P. Sistla. Deciding full branching time logics. Information and Control, 61(3):175–201, 1984.
C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189–196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
D. Kozen. Results on the prepositional Μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
L. Lamport. Sometimes is sometimes “not never” — on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174–185, January 1980.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposiumon Principles of Programming Languages, pages 97–107, New Orleans, January 1985.
D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267–276, 1987.
D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming. Springer-Verlag, 1986.
D. E. Muller, A. Saoudi, and P. E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, pages 422–427, Edinburgh, July 1988.
A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int'l Symp. on Programming, volume 137, pages 337–351. Springer-Verlag, Lecture Notes in Computer Science, 1981.
R. S. Street and E. A. Emerson. An elementary decision procedure for the mucalculus. In Proc. 11th Int. Colloquium on Automata, Languages and Programming, volume 172. Lecture Notes in Computer Science, Springer-Verlag, July 1984.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161–177, 1991.
W. Thomas. Automata on infinite objects. Handbook of theoretical computer science, pages 165–191, 1990.
M.Y. Vardi. A temporal fixpoint calculus. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 250–259, San Diego, January 1988.
B. Vergauwen and J. Lewi. A linear local model checking algorithm for ctl. In Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 447–461, Hildesheim, August 1993. Springer-Verlag.
M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240–251, 1985.
M.Y. Vardi and P. Wolper. Yet another process logic. In Logics of Programs, volume 398, pages 501–512. Lecture Notes in Computer Science, Springer-Verlag, 1984.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182–21, April 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 110(2), May 1994. (To appear).
P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.
P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75–123. Lecture Notes in Computer Science, Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernholtz, O., Vardi, M.Y., Wolper, P. (1994). An automata-theoretic approach to branching-time model checking (Extended abstract). In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_50
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive