In this paper we propose an efficient algorithmic solution to the problem of determining a Bisimulation Relation on a finite structure.
Starting from a set-theoretic point of view we propose an algorithm that optimizes the solution to the Relational Coarsest Partition problem given by Paige and Tarjan in 1987 and its use in model-checking packages is discussed and tested.
Our algorithm reaches, in particular cases, a linear solution.
Keywords: Bisimulation, Automata, Verification.
