Symbolic Equivalence Checking

Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier

Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece), June 1993

Abstract:

We describe the implementation within Aldebaran of an algorithmic method allowing the generation of a minimal labeled transition system from an abstract model ; this minimality is relative to an equivalence relation. The method relies on a symbolic representation of the state space. We compute the minimal labeled transition system using the Binary Decision Diagram structures to represent the set of equivalence classes. Some experiments are presented, using a model obtained from LOTOS specifications.

12 pages

PDF

PostScript