A time and space efficient simulation algorithm

A number of algorithms for computing the simulation preorder are available. The best simulation algorithms are those by Gentilini, Piazza and Poli- criti (GPP) — subsequently corrected by van Glabbeek and Ploeger — and by Ranzato and Tapparo (RT). Let Σ denote the state space, -> the transition relation and Psim the partition of Σ induced by simulation equivalence. The algorithm GPP attains an optimal space bound of O(|Psim|^2 + |Σ| log |Psim|) — where optimal means that the space complexity is of the same order as the size of the output of the algorithm — while it runs in O(|Psim|^2|->|) time. The algorithm RT has the best time bound O(|Psim||->|) while it takes O(|Psim||Σ| log |Σ|) space. We present here a new time and space Efficient Simulation Algorithm (ESA) that runs in O(|Psim||->|) time and O(|Psim|^2 log |Σ| + |Σ| log |Psim|) space. Thus, ESA reaches in practice the optimal space bound of GPP while preserving the best time bound of RT. Analogously to GPP and RT, ESA is a symbolic algorithm, meaning that it maintains and iteratively refines a partition of the state space together with a preorder relation over this partition, while ESA achieves the above complexity bounds by following Hopcroft’s “process the smaller half” principle when updating some crucial data structures involving the blocks of the state partition.