Rank-Based Simulation on Acyclic Graphs

The simulation preorder is widely used both as a behavioral relation in concurrent systems, and as an abstraction tool to reduce the state space in model checking, were memory requirement is clearly a critical issue. Therefore, in this context a simulation algorithm should address both time and space efficiency. In this paper, we rely on the notion of rank to design an efficient simulation algorithm. It turns out that such algorithm outperforms-both in terms of time and in terms of space-the best simulation algorithms in the literature, on the class of acyclic graphs.