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...

• Type: Journal
• Year: 2008
• Where: IANDC
• Authors: Francesco Ranzato, Francesco Tapparo
• Keywords: Algorithm, IANDC 2008, State Partitions, Strong Preservation