Verifying Bisimulations ``On the Fly''

Jean-Claude Fernandez and Laurent Mounier

Proceedings of the 3rd International Conference on Formal Description Techniques FORTE'90 (Madrid, Spain), November 1990

Abstract:

This paper describes a decision procedure for bisimulation-based equivalence relations between Labelled Transition Systems (LTSs). 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 LTSs. 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 Aldebaran and has been used in the framework of verification of Lotos specifications.

16 pages

PDF

PostScript