Bisimulation; Non-well-founded sets; OBDDs; Rank-based methods; Verification

We propose an efficient algorithmic solution to the problem of determining a Bisimulation Relation on a finite structure working both on the explicit and on the implicit (symbolic) representation. As far as the explicit case is concerned, starting …