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) \u2014 subsequently corrected by van Glabbeek and Ploeger \u2014 and by Ranzato and Tapparo (RT). Let \u3a3 denote the state space, -> the transition relation and Psim the partition of \u3a3 induced by simulation equivalence. The algorithm GPP attains an optimal space bound of O(|Psim|^2 + |\u3a3| log |Psim|) \u2014 where optimal means that the space complexity is of the same order as the size of the output of the algorithm \u2014 while it runs in O(|Psim|^2|->|) time. The algorithm RT has the best time bound O(|Psim||->|) while it takes O(|Psim||\u3a3| log |\u3a3|) space. We present here a new time and space Efficient Simulation Algorithm (ESA) that runs in O(|Psim||->|) time and O(|Psim|^2 log |\u3a3| + |\u3a3| 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\u2019s \u201cprocess the smaller half\u201d principle when updating some crucial data structures involving the blocks of the state partition