A Tool Set for deciding Behavioral Equivalences

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...

• Type: Conference
• Year: 1991
• Where: CONCUR
• Authors: Jean-Claude Fernandez, Laurent Mounier
• Keywords: CONCUR 1991, Distributed And Parallel Computing, Equivalence Relations, Simulation-based Equivalence Relations, Transition Systems