Verifying Bisimulations On the Fly
Jean-Claude Fernandez, Laurent Mounier · 1990
This paper describes a decision procedure for bisimulation-based equivalence relations between labeled transition systems. The algorithm usually performed in order to verify bisimulation consists in refining some initial equivalence relation until it becomes compatible with the transition relation under consideration. However, this method requires to store the transition relation explicitly, which limits it to medium-sized labeled transition systems. The algorithm proposed here does not need to previously construct the two transition systems: the verification can be performed during their generation. Thus, the amount of memory required can be significantly reduced, and verification of larger size systems becomes possible. This algorithm has been implemented in the tool Ald' ebaran and has been used in the framework of verification of Lotos specifications. 1 Introduction One of the successful approaches used for the verification of systems of communicating processes is provided by beha...