A Toolset for deciding Behavioral Equivalences

Jean-Claude Fernandez and Laurent Mounier

Proceedings of CONCUR'91 (Amsterdam, The Netherlands), August 1991

Abstract:

This paper deals with verification methods based on equivalence relations between labeled transition systems. More precisely, we are concerned by two practical needs: how to efficiently minimize and compare labeled transition systems with respect to bisimulation or simulation-based equivalence relations. First, we recall the principle of the classical algorithms for the existing equivalence relations, which are based on successive partition refinements of the state space of the labeled transition systems under consideration. However, in spite of their theoretical efficiency, the main drawback of these algorithms is that they require to generate and to store in memory the whole labeled transition systems to be compared or minimized. Therefore, the size of the systems which can be handled in practice remains limited. We propose here another approach, allowing to combine the generation and the verification phases, which is based on two algorithms respectively devoted to the comparison ("on the fly" comparison) and the minimization (minimal model generation) of labeled transition systems. Then, we present the results obtained when implementing some of these algorithms within the tool Aldebaran.

20 pages

PDF

PostScript