Saving Space in a Time Efficient Simulation Algorithm

A number of algorithms are available for computing the simulation relation on Kripke structures and on labelled transition systems representing concurrent systems. Among them, the algorithm by Ranzato and Tapparo [2007] has the best time complexity, while the algorithm by Gentilini et al. [2003] - successively corrected by van Glabbeek and Ploeger [2008] - has the best space complexity. Both space and time complexities are critical issues in a simulation algorithm, in particular memory requirements are crucial in the context of model checking when dealing with large state spaces.We propose here a new simulation algorithm thatis obtained as a space saving modification of the time efficient algorithm by Ranzato and Tapparo: a symbolic representation of sets is embedded in thisalgorithm so that any set of states manipulated by the algorithm can be efficiently stored as a set of blocks of a suitable state partition. It turns out that this new simulation algorithm retains a space complexity comparable with Gentilini et al.´s algorithm while improving on Gentilini et al.´s time bound.