Paper: A New Efficient Simulation Equivalence Algorithm (at LICS 2007)

Authors: Francesco Ranzato Francesco Tapparo

Abstract

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, \to the transition relation and P_sim the partition of \Sigma induced by simulation equivalence. The algorithms by Henzinger, Henzinger, Kopke and by Bloom and Paige run in O(|\Sigma||\to|)-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|\to|)-time while the space complexity is in O(|P_sim|^2 + |\Sigma| log(|P_sim|)). 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(|P_sim||\to|)-time and O(|P_sim||\Sigma|)-space. Thus, while retaining a space complexity which is lower than quadratic, our algorithm improves the best known time bound.

BibTeX

  @InProceedings{RanzatoTapparo-ANewEfficientSimula,
    author = 	 {Francesco Ranzato and Francesco Tapparo},
    title = 	 {A New Efficient Simulation Equivalence Algorithm},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {171--180},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }