Computing Reachable Simulations

We study the problem of computing the reachable blocks of simulation equivalence and design algorithms for this problem by interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. Following an investigation of the decidability and complexity aspects of this problem, we put forward several sound algorithms with varying completeness guarantees as well as a symbolic procedure manipulating state partitions and relations between their blocks, suited for processing infinite state systems. We show that the symbolic algorithm comes with better termination guarantees and, through empirical evidence, runs faster in general.