4 papers
Computing Stuttering Simulations
Francesco Ranzato, Francesco Tapparo
Stuttering bisimulation is a well-known behavioral equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorde…
An efficient simulation algorithm based on abstract interpretation
Francesco Ranzato, Francesco Tapparo
A number of algorithms for computing the simulation preorder are available. Let Sigma denote the state space, -> the transition relation and Psim the partition of Sigma induced by…
Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation
Francesco Ranzato, Francesco Tapparo
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…
Generalized Strong Preservation by Abstract Interpretation
Francesco Ranzato, Francesco Tapparo
Standard abstract model checking relies on abstract Kripke structures which approximate concrete models by gluing together indistinguishable states, namely by a partition of the co…