An automata-theoretic approach to branching-time model checking

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 [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 et 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.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time Temporal Logic, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.100, October 19-22, 1997
• 2: Henrik Reif Andersen , Bart Vergauwen, Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion, Proceedings of the 7th International Conference on Computer Aided Verification, p.142-154, July 03-05, 1995
• 3: Henrik Reif Andersen, Model checking and Boolean graphs, Symposium proceedings on 4th European symposium on programming, p.1-19, January 1992, Rennes, France
• 4: Proceedings on Temporal logic in specification, October 1987
• 5: Catriel Beeri, On the menbership problem for functional and multivalued dependencies in relational databases, ACM Transactions on Database Systems (TODS), v.5 n.3, p.241-259, Sept. 1980 [doi>10.1145/320613.320614]
• 6: Catriel Beeri , Philip A. Bernstein, Computational problems related to the design of normal form relational schemas, ACM Transactions on Database Systems (TODS), v.4 n.1, p.30-59, March 1979 [doi>10.1145/320064.320066]
• 7: Orna Bernholtz , Orna Grumberg, Branching Time Temporal Logic and Amorphous Tree Automata, Proceedings of the 4th International Conference on Concurrency Theory, p.262-277, August 23-26, 1993
• 8: Girish Bhat , Rance Cleaveland, Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.107-126, March 27-29, 1996
• 9: G. Bhat , R. Cleaveland, Efficient model checking via the equational /spl mu/-calculus, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.304, July 27-30, 1996
• 10: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 11: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 12: Edmund M. Clarke , Orna Grumberg , David E. Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.124-175, June 01-04, 1993
• 13: Rance Cleaveland , Bernhard Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus, Formal Methods in System Design, v.2 n.2, p.121-147, April 1993 [doi>10.1007/BF01383878]
• 14: C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
• 15: DOWLING, 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.
• 16: E. Allen Emerson, Automata, Tableaux and Temporal Logics (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.79-88, June 17-19, 1985
• 17: E. Allen Emerson, Automated temporal reasoning about reactive systems, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, p.41-101, April 1996, Banff, Canada
• 18: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 19: 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.
• 20: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 21: E. Allen Emerson , Charanjit S. Jutla , A. Prasad Sistla, On Model-Checking for Fragments of µ-Calculus, Proceedings of the 5th International Conference on Computer Aided Verification, p.385-396, June 28-July 01, 1993
• 22: EMERSON, E. A., AND LEI, C.-L. 1986. Efficient model checking in fragments of the propositional /x-calculus. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June). pp. 267-278.
• 23: E. Allen Emerson , A. Prasad Sistla, Deciding branching time logic, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.14-24, December 1984 [doi>10.1145/800057.808661]
• 24: FISCHER, M. J., AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194-211.
• 25: Erich Grädel , Igor Walukiewicz, Guarded Fixed Point Logic, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.45, July 02-05, 1999
• 26: Raymond Greenlaw , H. James Hoover , Walter L. Ruzzo, Limits to parallel computation: P-completeness theory, Oxford University Press, Inc., New York, NY, 1995
• 27: Thomas A. Henzinger , Orna Kupferman , Moshe Y. Vardi, A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking, Proceedings of the 7th International Conference on Concurrency Theory, p.514-529, August 26-29, 1996
• 28: IMMERMAN, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384-406.
• 29: C. Jard , T. Jeron, On-line model checking for finite linear temporal logic specifications, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.189-196, February 1990, Grenoble, France
• 30: JONES, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68-75.
• 31: JUTLA, C.S. 1990. Automata on infinite objects and modal logics of programs. Ph.D. dissertation, Univ. Texas, Austin, Texas.
• 32: 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.
• 33: KOZEN, D. 1983. Results on the propositional/x-calculus. Theoret. Comput. Sci. 27, 333-354.
• 34: Orna Kupferman , Moshe Y. Vardi, On the Complexity of Branching Modular Model Checking (Extended Abstract), Proceedings of the 6th International Conference on Concurrency Theory, p.408-422, August 21-24, 1995
• 35: Orna Kupferman , Moshe Y. Vardi, Module Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.75-86, August 03, 1996
• 36: Orna Kupferman , Moshe Y. Vardi, Model Checking Revisited, Proceedings of the 9th International Conference on Computer Aided Verification, p.36-47, June 22-25, 1997
• 37: O. Kupferman , M. Y. Vardi, Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.81, June 21-24, 1998
• 38: Orna Kupferman , Moshe Y. Vardi, Modular Model Checking, Revised Lectures from the International Symposium on Compositionality: The Significant Difference, p.381-401, September 08-12, 1997
• 39: Orna Kupferman , Moshe Y. Vardi, Weak alternating automata and tree automata emptiness, Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.224-233, May 24-26, 1998, Dallas, Texas, United States [doi>10.1145/276698.276748]
• 40: KUPFERMAN, 0., AND VARDI, M. Y. 1999a. Church's problem revisited. Bull. Symb. Logic 5, 2, 245-263.
• 41: Orna Kupferman , Moshe Y. Vardi, Robust Satisfaction, Proceedings of the 10th International Conference on Concurrency Theory, p.383-398, August 24-27, 1999
• 42: KUPFERMAN, 0., VARDI, M. Y., AND WOLPER, P. 1997. Module checking. Inf. Comput. to appear.
• 43: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 44: Kim Guldstrand Larsen, Efficient Local Correctness Checking, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.30-43, June 29-July 01, 1992
• 45: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 46: Nancy Lynch, Log Space Recognition and Translation of Parenthesis Languages, Journal of the ACM (JACM), v.24 n.4, p.583-590, Oct. 1977 [doi>10.1145/322033.322037]
• 47: Milena Mihail , Christos H. Papadimitriou, On the Random Walk Method for Protocol Testing, Proceedings of the 6th International Conference on Computer Aided Verification, p.132-141, June 21-23, 1994
• 48: MIYANO, S., AND HAYASHI, T. 1984. Alternating finite automata on ~0-words. Theoret. Comput. Sci. 32, 321-330.
• 49: D E Muller , A Saoudi , P E Schupp, Alternating automata, the weak monadic theory of the tree, and its complexity, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.275-283, September 1986, Rennes, France
• 50: 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.
• 51: David, E. Muller , Paul, E. Schupp, Alternating automata on infinite trees, Theoretical Computer Science, v.54 n.2-3, p.267-276, Oct. 1987 [doi>10.1016/0304-3975(87)90133-2]
• 52: PNUELI, A. 1981. The temporal semantics of concurrent programs. Theoret. Comput. Sci. 13, 45-60.
• 53: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 54: RABIN, M.O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.
• 55: 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.
• 56: SAVITCH, W.J. 1970. Relationship between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177-192.
• 57: G Slutzki, Alternating tree automata, Theoretical Computer Science, v.41 n.2-3, p.305-318, Dec. 1985
• 58: Colin Stirling, Games and Modal Mu-Calculus, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.298-312, March 27-29, 1996
• 59: Colin Stirling , David Walker, Local model checking in the modal mu-calculus, Theoretical Computer Science, v.89 n.1, p.161-177, Oct. 21, 1991
• 60: Robert S. Streett , E. Allen Emerson, The Propositional Mu-Calculus is Elementary, Proceedings of the 11th Colloquium on Automata, Languages and Programming, p.465-472, July 16-20, 1984
• 61: TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146-160.
• 62: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 63: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]
• 64: M. Y. Vardi, On the complexity of modular model checking, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.101, June 26-29, 1995
• 65: M Y Vardi , L Stockmeyer, Improved upper and lower bounds for modal logics of programs, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.240-251, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22173]
• 66: Moshe Y. Vardi , Pierre Wolper, Yet Another Process Logic (Preliminary Version), Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.501-512, June 06-08, 1983
• 67: 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.
• 68: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• 69: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]
• 70: Bart Vergauwen , Johan Lewi, A Linear Local Model Checking Algorithm for CTL, Proceedings of the 4th International Conference on Concurrency Theory, p.447-461, August 23-26, 1993
• 71: VISSER, W. 1998. Efficient CTL* model checking using games and automata. Ph.D. dissertation. Manchester University.
• 72: VISSER, W., AND BARRINGER, H. 1999. CTL* model checking for SPIN. In Software Tools for Technology Transfer. Lecture Notes in Computer Science, Springer-Verlag, New York.
• 73: B. Willems & P. ; Wolper, Partial-Order Methods for Model Checking: From Linear Time to Branching Time, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.294, July 27-30, 1996
• 74: WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control, 56, 1-2, 72-99.
• 75: Pierre Wolper, On the Relation of Programs and Computations to Models of Temporal Logic, Temporal Logic in Specification, p.75-123, April 08-10, 1987

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Algorithms, Verification