A compositional transformation for formal verification

The conditions under which a conjunction of two relations aR ₁b and bR₂c with existential abstraction of b can be transformed into an implication aR₁b→bR₂ c with universal abstraction of b are determined. In algorithmic design verification based on tautology checking and automata equivalence this transformation allows one to derive new verification algorithms, and to show under which conditions the breadth-first symbolic reachability algorithm used in proving automata equivalence can be applied when the automata are nondeterministic. Boolean characteristic functions of relations that have efficient representation using binary decision diagrams are used in the derivations