A number of algorithms for computing the simulation preorder on Kripke structures and on labelled transition systems are available. Among them, the algorithm by Ranzato and Tapparo [2007] has the best time complexity,while the algorithm by Gentilini

Similarity is a well known weakening of bisimilarity where one system is required to simulate the other and vice versa. It has been shown that the subgraph bisimilarity problem, a variation of the subgraph isomorphism problem where isomorphism is weakened to bisimilarity, is NP-complete. We show that the subgraph similarity problem and some related variations thereof still remain NP-complete.

It is well known that simulation equivalence is an appropriate abstraction to be used in model checking because it strongly preserves ACTL* and provides a better space reduction than bisimulation equivalence. However, computing simulation equivalence is harder than computing bisimulation equivalence. A number of algorithms for computing simulation equivalence exist. Let Sigma denote the state space, rarr the transition relation and Psimthe partition of Sigma induced by simulation equivalence. The algorithms by Henzinger, Henzinger, Kopke and by Bloom and Paige run in O(|Sigma||rarr|)-time and, as far as time-complexity is concerned, they are the best available algorithms. However, these algorithms have the drawback of a quadratic space complexity that is bounded from below by Omega(|Sigma|2). The algorithm by Gentilini, Piazza, Policriti appears to be the best algorithm when both time and space complexities are taken into account. Gentilini et al.'s algorithm runs in O(|Psim|2|rarr|)-time while the space complexity is in O(|Psim|2+ |Sigma| log(|Psim|)). We present here a new efficient simulation equivalence algorithm that is obtained as a modification of Henzinger et al.'s algorithm and whose correctness is based on some techniques used in recent applications of abstract interpretation to model checking. Our algorithm runs in O(|Psim||rarr|)-time and O(|Psim||Sigma|)-space. Thus, while retaining a space complexity which is lower than quadratic, our algorithm improves the best known time bound.

Abstract Many algorithms have been proposed to minimally refine abstract transition systems in order to get strong preservation relatively to a given temporal specification language. These algorithms compute a state equivalence, namely they work on abstractions which are partitions of system states. This is restrictive because, in a generic abstract interpretation-based view, state partitions are just one particular type of abstraction, and therefore it could well happen that the refined partition constructed by the algorithm is not the optimal generic abstraction. On the other hand, it has been already noted that the well-known concept of complete abstract interpretation is related to strong preservation of abstract model checking. This paper establishes a precise correspondence between complete abstract interpretation and strongly preserving abstract model checking, by showing that the problem of minimally refining an abstract model checking in order to get strong preservation can be formulated as a complete domain refinement in abstract interpretation, which always admits a fixpoint solution. As a consequence of these results, we show that some well-known behavioural equivalences used in process algebra like bisimulation and stuttering and their corresponding partition refinement algorithms can be elegantly characterized in pure abstract interpretation as completeness properties.