Symbolic equivalence checking

Abstract

We describe the implementation, within Aldébaran 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.