An efficient simulation algorithm on Kripke structures

A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let $varSigma $ denote the state space, ${rightarrow }$ the transition relation and $P_{mathrm {sim}}$ the partition of $varSigma $ induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is $|P_{mathrm {sim}}|^2$ , other algorithms are devised to attain the best time complexity $O(|P_{mathrm {sim}}||{rightarrow }|)$ . We present a novel simulation algorithm which is both space and time efficient: it runs in $O(|P_ {mathrm {sim}}|^2 log |P_{mathrm {sim}}| + |varSigma |log |varSigma |)$ space and $O(|P_{mathrm {sim}}||{rightarrow }|log |varSigma |)$ time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity.