Exploiting cofactoring for efficient FSM symbolic traversal based on the transition relation

Symbolic state space traversal techniques are one of the most notable achievements in the fields of formal verification and of automated synthesis. Transition functions and transition relations are two alternative approaches. In terms of efficiency, transition functions have proven to be superior, although the transition relation is much more expressive. The paper brings the transition relation back to a new life, profiting from recent advancements in the fields of Boolean function representation, simplification, and image computation represented by BDDs and by the generalized cofactor operator. A theoretical result allows us to considerably simplify both the process of building the transition relation and of traversing the state space. Experimental results show that performances similar to those of the transition function are obtained