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.
- ALUR, R., HENZINGER, T. A., AND KUPFERMAN, 0. 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.]] Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- BEERI, C. 1980. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Datab. Syst. 5, 3 (Sept.), 241-259.]] Google Scholar
- BEERI, C., AND BERNSTEIN, P.A. 1979. Computational problems related to the design of normal form relational schemas. ACM Trans. Datab. Syst. 4, 1 (Mar.), 30-59.]] Google Scholar
- BERNHOLTZ, 0., AND GRUMBERG, 0. 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.]] Google Scholar
- BHAT, G., AND CLEAVELAND, R. 1996a. Efficient local model-checking for fragments of the modal /x-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.]] Google Scholar
- BHAT, G., AND CLEAVELAND, R. 1996b. Efficient model checking via the equational/x-calculus. In Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 304-312.]] Google Scholar
- CHANDRA, A. K., KOZEN, D. C., AND STOCKMEYER, L.J. 1981. Alternation. J. ACM 28, 1 (Jan.), 114-133.]] Google Scholar
- CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst. 8, 2 (Apr.), 244-263.]] Google Scholar
- CLARKE, E. M., GRUMBERG, 0., 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.]] Google Scholar
- CLEAVELAND, R. 1993. A linear-time model-checking algorithm for the alternation-free modal /x-calculus. Form. Meth. Syst. Des. 2, 121-147.]] Google Scholar
- COURCOUBETIS, C., VARDI, M. Y., WOLPER, P., AND YANNAKAKIS, M. 1992. Memory efficient algorithms for the verification of temporal properties. Form. Meth. Syst. Des. 1,275-288.]] Google Scholar
- 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.]]Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- 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.]]Google Scholar
- 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.]] Google Scholar
- EMERSON, E. A., JUTLA, C., AND SISTLA, A. P. 1993. On model-checking for fragments of /x-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.]] Google Scholar
- 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.]]Google Scholar
- 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.]] Google Scholar
- FISCHER, M. J., AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194-211.]]Google Scholar
- 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.]] Google Scholar
- GREENLAW, R., HOOVER, H. J., AND RUZZO, W.L. 1995. Limits of parallel computation. Oxford University Press, Oxford, England.]] Google Scholar
- HENZINGER, T. A., KUPFERMAN, 0., 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.]] Google Scholar
- IMMERMAN, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384-406.]]Google Scholar
- 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.]] Google Scholar
- JONES, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68-75.]]Google Scholar
- JUTLA, C.S. 1990. Automata on infinite objects and modal logics of programs. Ph.D. dissertation, Univ. Texas, Austin, Texas.]]Google Scholar
- 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.]]Google Scholar
- KOZEN, D. 1983. Results on the propositional/x-calculus. Theoret. Comput. Sci. 27, 333-354.]]Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., 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.]] Google Scholar
- KUPFERMAN, 0., AND VARDI, M. Y. 1999a. Church's problem revisited. Bull. Symb. Logic 5, 2, 245-263.]]Google Scholar
- KUPFERMAN, 0., AND VARDI, M. Y. 1999b. Robust satisfaction. In Proceedings of the lOth Conference on Concurrency Theory. Lecture Notes in Computer Science. Springer-Verlag, New York.]] Google Scholar
- KUPFERMAN, 0., VARDI, M. Y., AND WOLPER, P. 1997. Module checking. Inf. Comput. to appear.]]Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- LICHTENSTEIN, 0., 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.]] Google Scholar
- LYNCH, N. 1977. Log space recognition and translation of parenthesis languages. J. ACM 24, 4 (Oct.), 583-590.]] Google Scholar
- 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.]] Google Scholar
- MIYANO, S., AND HAYASHI, T. 1984. Alternating finite automata on ~0-words. Theoret. Comput. Sci. 32, 321-330.]]Google Scholar
- 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.]] Google Scholar
- 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.]]Google Scholar
- MULLER, D. E., AND SCHUPP, P.E. 1987. Alternating automata on infinite trees. Theoret. Comput. Sci. 54, 267-276.]] Google Scholar
- PNUELI, A. 1981. The temporal semantics of concurrent programs. Theoret. Comput. Sci. 13, 45-60.]]Google Scholar
- 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.]] Google Scholar
- RABIN, M.O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.]]Google Scholar
- 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.]]Google Scholar
- SAVITCH, W.J. 1970. Relationship between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177-192.]]Google Scholar
- SLUTZKI, G. 1985. Alternating tree automata. Theoret. Comput. Sci. 41, 305-318.]] Google Scholar
- 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.]] Google Scholar
- STIRLING, C., AND WALKER, D. 1991. Local model checking in the modal Mu-calculus. Theoret. Comput. Sci. 89, 1, 161-177.]] Google Scholar
- STREET, R. S., AND EMERSON, E.A. 1984. An elementary decision procedure for the/x-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.]] Google Scholar
- TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146-160.]]Google Scholar
- THOMAS, W. 1990. Automata on infinite objects. Handb. Theoret. Comput. Sci., 165-191.]] Google Scholar
- 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.]] Google Scholar
- 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.]] Google Scholar
- VARDI, M. Y., AND STOCKMEYER, L. 1985. Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th Annual ACM Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM, New York, pp. 240-251.]] Google Scholar
- 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.]] Google Scholar
- 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.]]Google Scholar
- VARDI, M. Y., AND WOLPER, P. 1986b. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32, 2 (Apr.), 182-221.]] Google Scholar
- VARDI, M. Y., AND WOLPER, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1 (Nov.), 1-37.]] Google Scholar
- 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.]] Google Scholar
- VISSER, W. 1998. Efficient CTL* model checking using games and automata. Ph.D. dissertation. Manchester University.]]Google Scholar
- 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.]]Google Scholar
- WILLEMS, B., AND WOLPER, P. 1996. Partial-order methods for model checking: From linear time to branching time. In Proceedings of the l lth Annual Symposium on Logic in Computer Science. (New Brunswick, N.J., July).]] Google Scholar
- WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control, 56, 1-2, 72-99.]]Google Scholar
- 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.]] Google Scholar
Index Terms
- An automata-theoretic approach to branching-time model checking
Recommendations
Branching-Time Model-Checking of Probabilistic Pushdown Automata
In this paper we study complexity of the model-checking problem for probabilistic pushdown automata (pPDA) and qualitative fragments of two branching-time logics PCTL* and PECTL*. We prove tha this problem is in 2-EXPTIME for pPDA and qualitative PCTL*. ...
Branching-time model-checking of probabilistic pushdown automata
In this paper we study the model-checking problem for probabilistic pushdown automata (pPDA) and branching-time probabilistic logics PCTL and PCTL^@?. We show that model-checking pPDA against general PCTL formulae is undecidable, but we yield positive ...
An automata-theoretic approach to modular model checking
In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...
Comments