Abstract
We present a unified game-based approach for branching-time model checking of hierarchical systems. Such systems are exponentially more succinct than standard state-transition graphs, as repeated sub-systems are described only once. Early work on model checking of hierarchical systems shows that one can do better than a naive algorithm that “flattens” the system and removes the hierarchy.
Given a hierarchical system \(\mathcal S\) and a branching-time specification ψ for it, we reduce the model-checking problem (does \(\mathcal S\) satisfy ψ?) to the problem of solving a hierarchical game obtained by taking the product of \(\mathcal S\) with an alternating tree automaton \({\mathcal A}_\psi\) for ψ. Our approach leads to clean, uniform, and improved model-checking algorithms for a variety of branching-time temporal logics. In particular, by improving the algorithm for solving hierarchical parity games, we are able to solve the model-checking problem for the μ-calculus in Pspace and time complexity that is only polynomial in the depth of the hierarchy. Our approach also leads to an abstraction-refinement paradigm for hierarchical systems. The abstraction maintains the hierarchy, and is obtained by merging both states and sub-systems into abstract states.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM TOPLAS 27(4), 786–818 (2005)
Alur, R., Chaudhuri, S., Etessami, K., Madhusudan, P.: On-the-fly reachability and cycle detection for recursive state machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 61–76. Springer, Heidelberg (2005)
Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)
Alur, R., Kannan, S., Yannakakis, M.: Communicating hierarchical state machines. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 169–178. Springer, Heidelberg (1999)
Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)
de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol. 1536. Springer, Heidelberg (1998)
Drusinsky, D., Harel, D.: On the power of bounded concurrency I: Finite automata. J. of the ACM 41(3), 517–539 (1994)
Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: FOCS 1991, pp. 368–377 (1991)
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)
Göller, S., Lohrey, M.: Fixpoint logics on hierarchical structures. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 483–494. Springer, Heidelberg (2005)
Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. J. of Inf. & Comp. 173, 1–19 (2002)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. of the ACM 47(2), 312–360 (2000)
La Torre, S., Napoli, M., Parente, M., Parlato, G.: Verification of scope-dependent hierarchical state machines. Inf. Comput. 206(9-10), 1161–1177 (2008)
Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society, Los Alamitos (1988)
Murano, A., Napoli, M., Parente, M.: Program complexity in hierarchical module checking. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 318–332. Springer, Heidelberg (2008)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logics and Models of Concurrent Systems. NATO Advanced Summer Institutes, vol. F-13, pp. 123–144. Springer, Heidelberg (1985)
Qadeer, S.: Taming concurrency: A program verification perspective. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, p. 5. Springer, Heidelberg (2008)
Rabinovich, A.: Complexity of equivalence problems for concurrent systems of finite agents. J. of Inf. & Comp. 139(2), 111–129 (1997)
Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aminof, B., Kupferman, O., Murano, A. (2010). Improved Model Checking of Hierarchical Systems. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-11319-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11318-5
Online ISBN: 978-3-642-11319-2
eBook Packages: Computer ScienceComputer Science (R0)