Rank-Based Symbolic Bisimulation (and Model Checking)

In this paper we propose an efficient symbolic algorithm for the problem of determining the maximum bisimulation on a finite structure. The starting point is an algorithm, on explicit representation of graphs, which saves both time and space exploiting the notion of rank. This notion provides a layering of the input model and allows to proceed bottom-up in the bisimulation computation. In this paper we give a procedure that allows to compute the rank of a graph working on its symbolic representation and requiring a linear number of symbolic steps. Then we embed it in a fully symbolic, rank-driven, bisimulation algorithm. Moreover, we show how the notion of rank can be employed to optimize the CTL Model Checking procedures.