Generalizing the Paige-Tarjan algorithm by abstract interpretation

10 years 12 months ago
Generalizing the Paige-Tarjan algorithm by abstract interpretation
act Interpretation Francesco Ranzato and Francesco Tapparo Dipartimento di Matematica Pura ed Applicata, Universit`a di Padova, Italy 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 eps of the PT algorithm from an abstract interpretation perspective, which allows us to reason on strong preservation in the context of arbitrary (temporal) languages and ic abstract models, possibly different from standard state partitions, specified by interpretation. This leads us to design a generalized Paige-Tarjan algorithm, called 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...
Francesco Ranzato, Francesco Tapparo
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Francesco Ranzato, Francesco Tapparo
Comments (0)