Verifying Bisimulations "On the Fly"

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

• Type: Conference
• Year: 1990
• Where: FORTE
• Authors: Jean-Claude Fernandez, Laurent Mounier
• Keywords: Equivalence Relation, FORTE 1990, FORTE 2007, Transition Relation, Transition Systems