Computing Reachable Simulations

We study the problem of computing reachable blocks of the 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. The interest in computing simulation blocks stems from the fact that simulation provides a better state space reduction than other equivalence notions such as bisimilarity, yet retaining enough precision for model checking. On the other hand, the problem turns out to be significantly harder than the one for the bisimulation case. We put forward a sound algorithm manipulating state partitions and relations between their blocks, suited for processing infinite-state systems. This is a joint work with Pierre Ganty and Francesco Ranzato. Contributed talk given by Nicolas Manini

Authors

• Nicolas Manini

Keywords

No keywords are indexed for this paper.