An efficient simulation algorithm based on abstract interpretation

A number of algorithms for computing the simulation preorder and equivalence are available. Let Sigma denote the state space,. the transition relation and P-sim the partition of Sigma induced by simulation equivalence. The algorithms by Henzinger, Henzinger, and Kopke and by Bloom and Paige run in O(|Sigma||-->|)-time and, as far as time complexity is concerned, they are the best available algorithms. However, these algorithms have the drawback of a space complexity that is more than quadratic in the size of the state space Sigma. The algorithm by Gentilini, Piazza, Policriti - subsequently corrected by van Glabbeek and Ploeger - appears to provide the best compromise between time and space complexity. Gentilini et al.'s algorithm runs in O(|P-sim|(2)|-->|)-time while the space complexity is in O(|P-sim|(2) + |Sigma| log |P-sim|). We present here a new efficient simulation algorithm that is obtained as a modi. cation of Henzinger et al.'s algorithm and whose correctness is based on some techniques used in applications of abstract interpretation to model checking. Our algorithm runs in O(|P-sim||-->|)-time and O(|P-sim||Sigma| log |Sigma|)-space. Thus, this algorithm improves the best known time bound while retaining an acceptable space complexity that is in general less than quadratic in the size of the state space |Sigma|. An experimental evaluation showed good comparative results w.r.t. Henzinger et al.'s algorithm. (C) 2009 Elsevier Inc. All rights reserved.