An automata-theoretic approach to branching-time model checking

© ACM, 2000 This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Journal of the ACM (JACM) Volume 47 , Issue 2 (March 2000), http://doi.acm.org/10.1145/333979.333987

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Finite automata; Temporal logic; model checking

Abstract :

[en] 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, automate-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] 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 can they be used to obtain optimal decision procedures, as was shown by Muller ct al., 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.

Disciplines :

Computer science

Author, co-author :

Kupferman, Orna; Hebrew University of Jerusalem > Computer Science department

Vardi, Moshe Y; Rice University > Computer Science departement

Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)

Language :

English

Title :

An automata-theoretic approach to branching-time model checking

Publication date :

2000

Journal title :

Journal of the ACM

ISSN :

0004-5411

Publisher :

Association for Computing Machinery, New York, United States

Volume :

Issue :

Pages :

312-360

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 01 December 2009

Statistics

Number of views

70 (2 by ULiège)

Number of downloads

540 (4 by ULiège)

More statistics

Scopus citations^®

397

Scopus citations^®
without self-citations

318

OpenCitations

292

Bibliography

ALUR, R., HENZINGER, T. A., AND KUPFERMAN, O. 1997. Alternating-time temporal logic. In , Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 100-109.
ANDERSEN, H. R., AND VERGAUWEN, B. 1995. Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In Computer Aided Verification, Proceedings of the 7th International Conference (Liege, Belgium, July). Lecture Notes in Computer Science, vol. 939. Springer-Verlag, New York, pp. 142-154.
ANDERSON, H. R. 1992. Model checking and boolean graphs. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 582. Springer-Verlag, New York, pp. 1-19.
BANIEQBAL, B., AND BARRINGER, H. 1987. Temporal logic with fixed points. In Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, vol. 398. Springer-Verlag, New York, pp. 62-74.
BEERI, C. 1980. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Datab. Syst. 5, 3 (Sept.), 241-259.
BEERI, C., AND BERNSTEIN, P. A. 1979. Computational problems related to the design of normal form relational schémas. ACM Trans. Datab. Syst. 4, 1 (Mar.), 30-59.
BERNHOLTZ, O., AND GRUMBERG, O. 1993. Branching time temporal logic and amorphous tree automata. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 262-277.
BHAT, G., AND CLEAVELAND, R. 1996a. Efficient local model-checking for fragments of the modal /i-calculus. In Proceedings of the 1996 Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science, vol. 1055. Springer-Verlag, Berlin, Germany.
BIIAT, G., AND CLEAVELAND, R. 1996b. Efficient model checking via the equational ft-calculus. In Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 304-312.
CHANDRA, A. K., KOZEN, D. C., AND STOCKMEYER, L. J. 1981. Alternation. J. ACM 28, 1 (Jan.), 114-133.
CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prag. Lang. Syst. 8, 2 (Apr.), 244-263.
CLARKE, E. M., GRUMBERG, O., AND LONG, D. 1993. Verification tools for finite-state concurrent systems. In Decade of Concurrency-Reflections and Perspectives (Proceedings of REX School) J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 803. Springer-Verlag, New York, pp. 124-175.
CLEAVELAND, R. 1993. A linear-time model-checking algorithm for the alternation-free modal fi-calculus. Form. Meth. Syst. Des. 2; 121-147.
CouRCOUBETis, C., VARDi, M. Y., WoLPER, P., AND YANNAKAKis, M. 1992. Memory efficient algorithms for the verification of temporal properties. Form. Meth. Syst. Des. l, 275-288.
BOWLING, W. F., AND GALLIER, J. H. 1984. Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Prog. 1, 3, 267-284.
EMERSON, E. A. 1985. Automata, tableaux, and temporal logics. In Proceedings of the Workshop on Logic of Programs. Lecture Notes in Computer Science, vol. 193. Springer-Verlag, New York, pp. 79-87.
EMERSON, E. A. 1996. Automated temporal reasoning about reactive systems. In Proceedings of the VIII-th BANFF Higher Order Workshop. Lecture Notes in Computer Science, vol. 1043. Springer-Verlag, New York, pp. 41-101.
EMERSON, E. A., AND HALPERN, J. Y. 1986. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. J. ACM 33, 1 (Jan.), 151-178.
EMERSON, E. A., AND JUTLA, C. 1988. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of.Computer Science (White Plains, N.Y., Oct.) IEEE Computer Society Press, Los Alamitos, Calif., pp. 328-337.
EMERSON, E. A., AND JUTLA, C. 1991. Tree automata, Mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (San Juan, P.R., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 368-377.
EMERSON, E. A., JUTLA, C., AND SISTLA, A. P. 1993. On model-checking for fragments of fi-calculus. In Computer Aided Verification, Proceedings of the 5th International Conference (Elounda, Crete, June). Lecture Notes in Computer Science, vol. 697. Springer-Verlag, New York, pp. 385-396.
EMERSON, E. A., AND LEI, C.-L. 1986. Efficient model checking in fragments of the prepositional /i-calculus. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June), pp. 267-278.
EMERSON, E. A., AND SISTLA, A. P. 1984. Deciding branching time logic. In Proceedings of the 16th Annual ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM, New York, pp. 14-24.
FISCHER, M. J., AND LADNER, R. E. 1979. Prepositional dynamic logic of regular programs. J. Comput. Syst. Sei. 18, 194-211.
GRAEDEL, E., AND WALUKIEWICZ, I. 1999. Guarded fixed point logic. In Proceedings of the 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.
GREENLAW, R., HOOVER, H. J., AND Ruzzo, W. L. 1995. Limits of parallel computation. Oxford University Press, Oxford, England.
HENZINGER, T. A., KUPFERMAN, O., AND VARDI, M. Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In Proceedings of the 7th Conference on Concurrency Theory (Pisa, Italy, Aug.). Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, New York, pp. 514-529.
IMMERMAN, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sei. 22, 3, 384-406.
JARD, C., AND JERON, T. 1989. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proceedings of the International Workshop (Grenoble, Switzerland, June). Lecture Notes in Computer Science, vol. 407. Springer-Verlag, New York, pp. 189-196.
JONES, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sei. 11, 68-75.
JUTLA, C. S. 1990. Automata on infinite objects and modal logics of programs. Ph.D. dissertation, Univ. Texas, Austin, Texas.
KOZEN, D. 1977. Lower bounds for natural proof systems. In Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. IEEE Computer Science Press, Los Alamitos, Calif., pp. 254-266.
KOZEN, D. 1983. Results on the propositional -calculus. Theoret. Comput. Sei. 27, 333-354.
KUPFERMAN, O., AND VARDI, M. Y. 1995. On the complexity of branching modular model checking. In Proceedings of the 6th Conference on Concurrency Theory (Philadelphia, Pa., Aug.). Lecture Notes in Computer Science, vol. 962. Springer-Verlag, New York, pp. 408-422.
KUPFERMAN, O., AND VARDI, M. Y. 1996. Module checking. In Computer Aided Verification, Proceedings of the 8th International Conference. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, pp. 75-86.
KUPFERMAN, O., AND VARDI, M. Y. 1997. Module checking revisited. In Computer Aided Verification, Proceedings of the 9th International Conference. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 36-47.
KUPFERMAN, O., AND VARDI, M. Y. 1998a. Freedom, weakness, and determinism: From lineartime to branching-time. In Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 81-92.
KUPFERMAN, O., AND VARDI, M. Y. 1998b. Modular model checking. In Proceedings of the Compositionality Workshop. Lecture Notes in Computer Science, vol. 1536. Springer-Verlag, New York, pp. 381-401.
KUPFERMAN, O., AND VARDI, M. Y. 1998c. Weak alternating automata and tree automata emptiness. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing (Dallas, Tex., May 23-26). ACM, New York, pp. 224-233.
KUPFERMAN, O., AND VARDI, M. Y. 1999a. Church's problem revisited. Bull. Symb. Logic 5, 2, 245-263.
KUPFERMAN, O., AND VARDI, M. Y. 1999b. Robust satisfaction. In Proceedings of the. 10th Conference on Concurrency Theory. Lecture Notes in Computer Science. Springer-Verlag, New York.
KUPFERMAN, O., VARDI, M. Y., AND WOLPER, P. 1997. Module checking. Inf. Comput. to appear. LAMPORT, L. 1980. Sometimes is sometimes "not never"-On the temporal logic of programs. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, ACM, New York, pp. 174-185.
LARSEN, K. G. 1992. Efficient local correctness checking. In Proceedings of the 4th Conference on Computer Aided Verification (Montreal, Que., Canada, June). Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 30-43.
LICHTENSTEIN, O., AND PNUELI, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan.) ACM, New York, pp. 97-107.
LYNCH, N. 1977. Log space recognition and translation of parenthesis languages. J. ACM 24, 4 (Oct.), 583-590.
MIHAIL, M., AND PAPADEMITRIOU, C. H. 1994. On the random walk method for protocol testing. In Proceedings of the 5th Annual Conference on Computer Aided Verification (Stanford, Calif., June). Lecture Notes in Computer Science, vol. 818. Springer-Verlag, New York, pp. 132-141.
MIYANO, S., AND HAYASHI, T. 1984. Alternating finite automata on co-words. Theoret. Comput. Sei. 32, 321-330.
MULLER, D. E., SAOUDI, A., AND SCHUPP, P. E. 1986. Alternating'automata, the weak monadic theory of the tree and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag, New York.
MULLER, D. E., SAOUDI, A., AND SCHUPP, P. E. 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (Edinburgh, Scotland, July). IEEE Computer Society Press, Los Alamitos, Calif., pp. 422-427.
MULLER, D. E., AND SCHUPP, P. E. 1987. Alternating automata on infinite trees. Theoret. Comput. Sei. 54, 267-276.
PNUELI, A. 1981. The temporal semantics of concurrent programs. Theoret. Comput. Sei. 13, 45-60.
QUEILLE, J. P., AND SiFAKis, J. 1981. Specification and verification of concurrent systems in Cesar. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, New York, pp. 337-351.
RABIN, M. O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.
RABIN, M. O. 1970. Weakly definable relations and special automata. In Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory. North Holland, Amsterdam, New York, pp. 1-23.
SAVITCH, W. J. 1970. Relationship between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sei. 4, 177-192.
SLUTZKI, G. 1985. Alternating tree automata. Tlieoret. Comput. Sei. 41, 305-318.
STIRLING, C. 1996. Games and modal mu-calculus. In Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1055. Springer-Verlag, New York, pp. 298-312.
STIRLING, C., AND WALKER, D. 1991. Local model checking in the modal Mu-calculus. Tlieoret. Comput. Sei. 89, 1, 161-177.
STREET, R. S., AND EMERSON, E. A. 1984. An elementary decision procedure for the pi-calculus. In Proceedings of the llth International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 172. Springer-Verlag, New York, pp. 465-472.
TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146-160.
THOMAS, W. 1990. Automata on infinite objects. Handb. Theoret. Comput. Sei., 165-191.
VARDI, M. Y. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (San Francisco, Calif., May 5-7). ACM, New York, pp. 137-146.
VARDI, M. Y. 1995. On the complexity of modular model checking. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 101-111.
VARDI, M. Y., AND STOCKMEYER, L. 1985. Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th Annual ACAf Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM, New York, pp. 240-251.
VARDI, M. Y., AND WOLPER, P. 1984. Yet another process logic. In Logics of Programs. Lecture Notes in Computer Science, vol. 164. Springer-Verlag, New York, pp. 501-512.
VARDI, M. Y., AND WOLPER, P. 1986a. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June), pp. 322-331.
VARDI, M. Y., AND WOLPER, P. 1986b. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sei. 32, 2 (Apr.), 182-221.
VARDI, M. Y., AND WOLPER, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1 (Nov.), 1-37.
VERGAUWEN, B., AND LEWIS, J. 1993. A linear local model checking algorithm for CTL. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 447-461.
VISSER, W. 1998. Efficient CTL model checking using games and automata. Ph.D. dissertation. Manchester University.
VISSER, W., AND BARRINGER, H. 1999. CTL model checking for SPIN. In Sofnvare Tools for Technology Transfer. Lecture Notes in Computer Science, Springer-Verlag, New York.
WILLEMS, B., AND WOLPER, P. 1996. Partial-order methods for model checking: From linear time to branching time. In Proceedings of the llth Annual Symposium on Logic in Computer Science. (New Brunswick, N.J., July).
WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control, 56, 1-2, 72-99.
WOLPER, P. 1989. On the relation of programs and computations to models of temporal logic. In Proceedings of the Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 75-123.