Advertisement

Abstract

We define, for any partition of a state space and for formulas of the modal μ-calculus, two variants of precision for abstractions that have that partition set as state space. These variants are defined via satisfaction parity games in which the Refuter can replace a concrete state with any state in the same partition before, respectively after, a quantifier move. These games are independent of the kind of abstraction. Our first variant makes the abstraction games of de Alfaro et al. model-independent, captures the definition of precision given by Shoham & Grumberg, and corresponds to generalized Kripke modal transition systems. Our second variant is then shown, for a fixed abstraction function, to render more precise abstractions through μ-automata without fairness. We discuss tradeoffs of both variants in terms of the size of abstractions, the perceived cost of their synthesis via theorem provers, and the preservation of equations that are valid over concrete models. Finally, we sketch a combination of both abstraction methods.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: Uncertainty, but with precision. In: Proc. of LICS’04, pp. 170–179. IEEE Comp. Soc. Press, Los Alamitos (2004)Google Scholar
  2. 2.
    Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 244–263. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  5. 5.
    Cleaveland, R., Iyer, S.P., Yankelevich, D.: Optimality in abstractions of model checking. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 51–63. Springer, Heidelberg (1995)Google Scholar
  6. 6.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proc. of POPL’77, pp. 238–252. ACM Press, New York (1977)Google Scholar
  7. 7.
    Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)Google Scholar
  8. 8.
    Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM TOPLAS 19(2), 253–291 (1997)CrossRefGoogle Scholar
  9. 9.
    Dams, D., Namjoshi, K.S.: Automata as abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)Google Scholar
  10. 10.
    Fecher, H., Huth, M.: Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Godefroid, P., Huth, M.: Model checking vs. generalized model checking: semantic minimization for temporal logics. In: Godefroid, P., Huth, M. (eds.) Proc. of LICS 2005, pp. 158–167. IEEE Comp. Soc. Press, Los Alamitos (2005)Google Scholar
  14. 14.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Gurfinkel, A., Wei, O., Chechik, M.: Systematic construction of abstractions for model-checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Janin, D., Walukiewicz, I.: Automata for the modal mu-calculus and related results. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, Springer, Heidelberg (1995)Google Scholar
  17. 17.
    Jurdziński, M.: Deciding the winner in parity games is in UP∩co-UP. Information Processing Letters 68(3), 119–124 (1998)CrossRefMathSciNetGoogle Scholar
  18. 18.
    Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proc. of LICS’90, pp. 108–117. IEEE Comp. Soc. Press, Los Alamitos (1990)Google Scholar
  20. 20.
    Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th International Symposium on Programming, pp. 337–351 (1981)Google Scholar
  21. 21.
    Schmidt, D.A.: Closed and logical relations for over- and under-approximation of powersets. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)Google Scholar
  22. 22.
    Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. In: Proc. of LICS 2006, pp. 399–410. IEEE Comp. Soc. Press, Los Alamitos (2006)Google Scholar
  23. 23.
    Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)Google Scholar
  24. 24.
    Wilke, T.: Alternating tree automata, parity games, and modal μ-calculus. Bull. Soc. Math. Belg. 8(2), 359–391 (2001)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Harald Fecher
    • 1
  • Michael Huth
    • 2
  1. 1.Christian-Albrechts-University KielGermany
  2. 2.Imperial College LondonUnited Kingdom

Personalised recommendations