Symbolic Equivalence Checking

Abstract. We describe the implementation, within ALDEBARAN of an algorithmic method allowing the generation of a minimal labeled transition rom 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.

• Type: Conference
• Year: 1993
• Where: CAV
• Authors: Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier
• Keywords: CAV 1993, Equivalence Relation, Hardware, Labeled Transition System, Minimal Labeled Transition