Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation

TL;DR

This paper generalizes the Paige-Tarjan algorithm using abstract interpretation, enabling the computation of minimal models that strongly preserve various temporal logics and properties in state-based systems.

Contribution

It introduces the GPT algorithm, a generalized framework that extends Paige-Tarjan to abstract models and arbitrary languages, with applications to simulation, stuttering, and reachability preservation.

Findings

GPT encompasses existing algorithms like stuttering equivalence computation.

GPT can be instantiated to produce new efficient algorithms for simulation equivalence.

GPT enables the computation of coarsest refinements that strongly preserve reachability-based languages.

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