``On the Fly'' Verification of Behavioural Equivalences and Preorder
Jean-Claude Fernandez and Laurent Mounier
Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), July 1991
This paper describes decision procedures for bisimulation and simulation relations between two transition systems. The algorithms proposed here do not need to previously construct transition systems: the verification can be performed during their generation. In addition, diagnosis features are computed when the two transitions systems are not equivalent.