Advertisement

An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation

  • Francesco Ranzato
  • Francesco Tapparo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

Abstract

The Paige and Tarjan algorithm (PT) for computing the coarsest refinement of a state partition which is a bisimulation on some Kripke structure is well known. It is also well known in abstract model checking that bisimulation is equivalent to strong preservation of CTL and in particular of Hennessy-Milner logic. Building on these facts, we analyze the basic steps of the PT algorithm from an abstract interpretation perspective, which allows us to reason on strong preservation in the context of generic inductively defined (temporal) languages and of abstract models specified by abstract interpretation. This leads us to design a generalized Paige-Tarjan algorithm, called GPT, for computing the minimal refinement of an abstract interpretation-based model that strongly preserves some given language. It turns out that PT can be obtained by instantiating GPT to the domain of state partitions for the case of strong preservation of Hennessy-Milner logic. We provide a number of examples showing that GPT is of general use. We show how two well-known efficient algorithms for computing simulation and stuttering equivalence can be viewed as simple instances of GPT. Moreover, we instantiate GPT in order to design a O(|Transitions||States|)-time algorithm for computing the coarsest refinement of a given partition that strongly preserves the language generated by the reachability operator EF.

Keywords

Model Check Abstract Interpretation Atomic Proposition Kripke Structure Abstract Domain 
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

  1. 1.
    Aho, A.V., Hopcroft, J.E., Ullman, J.D.: Data Structures and Algorithms. Addison-Wesley, Reading (1983)zbMATHGoogle Scholar
  2. 2.
    Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comp. Sci. 59, 115–131 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM POPL, pp. 238–252 (1977)Google Scholar
  5. 5.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM POPL, pp. 269–282 (1979)Google Scholar
  6. 6.
    Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven Univ (1996)Google Scholar
  7. 7.
    De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)zbMATHCrossRefGoogle Scholar
  8. 8.
    Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Automated Reasoning 31(1), 73–103 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples and refinements in abstract model checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)zbMATHMathSciNetGoogle Scholar
  11. 11.
    Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  12. 12.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462 (1995)Google Scholar
  14. 14.
    Kucera, A., Mayr, R.: Why is simulation harder than bisimulation? In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 594–610. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    van Glabbeek, R.J.: The linear time - branching time spectrum I: the semantics of concrete sequential processes. In: Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Francesco Ranzato
    • 1
  • Francesco Tapparo
    • 1
  1. 1.Dipartimento di Matematica Pura ed ApplicataUniversità di PadovaItaly

Personalised recommendations