Abstract
In this paper we extend the automata-theoretic framework for reasoning about infinite-state sequential systems to handle also the global model-checking problem. Our framework is based on the observation that states of such systems, which carry a finite but unbounded amount of information, can be viewed as nodes in an infinite tree, and transitions between states can be simulated by finite-state automata. Checking that the system satisfies a temporal property can then be done by a two-way automaton that navigates through the tree. The framework is known for local model checking. For branching time properties, the framework uses two-way alternating automata. For linear time properties, the framework uses two-way path automata. In order to solve the global model-checking problem we show that for both types of automata, given a regular tree, we can construct a nondeterministic word automaton that accepts all the nodes in the tree from which an accepting run of the automaton can start.
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
Alur, R., La Torre, S., Madhusudan, P.: Modular strategies for infinite games on recursive game graphs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 67–79. Springer, Heidelberg (2003)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. IC 98(2), 142–170 (1992)
Burkart, O., Quemener, Y.-M.: Model checking of infinite graphs defined by graph grammars. In: 1st Infinity. ENTCS, vol. 6 (1996)
Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992)
Burkart, O., Steffen, B.: Composition, decomposition and model checking of pushdown processes. Nordic J. Comput. 2, 89–125 (1995)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pp. 1–12 (1962)
Burkart, O.: Model checking rationally restricted right closures of recognizable graphs. In: 2nd Infinity (1997)
Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. In: 4th Infinity. ENTCS, vol. 68(6) (2002)
Cachat, T.: Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 556–569. Springer, Heidelberg (2003)
Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLASÂ 8(2) (1986)
Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 66–78. Springer, Heidelberg (2001)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. FMSD 1, 275–288 (1992)
Chen, H., Wagner, D.: Mops: an infrastructure for examining security properties of software. In: 9th CCS, pp. 235–244. ACM, New York (2002)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: 32nd FOCS, pp. 368–377 (1991)
Emerson, E.A., Jutla, C., Sistla, A.P.: On model-checking for fragments of μ- calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)
Esparza, J., Kucera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 316–339. Springer, Heidelberg (2001)
Emerson, E.A.: Model checking and the μ-calculus. In: Descriptive Complexity and Finite Models, pp. 185–214. AMS (1997)
Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)
Janin, D., Walukiewicz, I.: Automata for the modal μ-calculus and related results. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer, Heidelberg (1995)
Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Kupferman, O., Piterman, N., Vardi, M.Y.: Model checking linear properties of prefix-recognizable systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 371–385. Springer, Heidelberg (2002)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes (1994)
Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 36–52. Springer, Heidelberg (2000)
Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)
Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and secondorder logic. TCS 37, 51–75 (1985)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. TCSÂ 54 (1987)
Pnueli, A.: The temporal logic of programs. In: 18th FOCS, pp. 46–57 (1977)
Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)
Piterman, N., Vardi, M.Y.: Micro-macro stack systems: A new frontier of decidability for sequential systems. In: 18th LICS, pp. 381–390. IEEE, Los Alamitos (2003)
Rabin, M.O.: Automata on infinite objects and Church’s problem. AMS (1972)
Stirling, C., Walker, D.: Local model checking in the modal μ-calculus. TCS 89(1), 161–177 (1991)
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 628. Springer, Heidelberg (1998)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. ICÂ 115(1) (1994)
Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Wilke, T.: CTL+ is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, p. 110. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Piterman, N., Vardi, M.Y. (2004). Global Model-Checking of Infinite-State Systems. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive