Partial Order Reductions for Bisimulation Checking

Partial order methods have been introduced to avoid the state explosion problem in verification resulting from the representation of multiple interleavings of concurrent transitions. The basic idea is to build a reduced state space on which certain properties hold if and only if they hold for the full state space. Most often, the considered properties are linear-time properties. In this paper we suggest novel branching time reduction techniques which allow checking bisimulation equivalence on reduced state spaces. Our reduction takes place on bisimulation game graphs, thus jointly treating the systems under consideration. We show that reduction preserves winning strategies of the two players in the bisimulation game.