An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation
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.
KeywordsModel Check Abstract Interpretation Atomic Proposition Kripke Structure Abstract Domain
- 3.Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
- 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.Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM POPL, pp. 269–282 (1979)Google Scholar
- 6.Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven Univ (1996)Google Scholar
- 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