Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation

Details Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation

2006-12-22

arxiv.org/abs/cs/0612120v2

Computer Science

Logic in Computer Science

Keywords: Abstract interpretation, abstract model checking, strong preservation, Paige-Tarjan algorithm, refinement algorithm

Scientific paper

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 model checking that bisimulation is equivalent to strong preservation of CTL, or, equivalently, of Hennessy-Milner logic. Drawing on these observations, 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 possibly non-partitioning 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 is a straight instance of GPT on 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 first show how a well-known efficient algorithm for computing stuttering equivalence can be viewed as a simple instance of GPT. We then instantiate GPT in order to design a new efficient algorithm for computing simulation equivalence that is competitive with the best available algorithms. Finally, we show how GPT allows to compute new strongly preserving abstract models by providing an efficient algorithm that computes the coarsest refinement of a given partition that strongly preserves the language generated by the reachability operator.

Affiliated with

Also associated with

No associations

Rating

Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-531051