The equivalence checking problem consists in verifying that a system (e.g., a
) matches its abstract specification (e.g., a
) by comparing their Labeled Transition Systems (
s) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking:
verification requires to construct the two
s before comparison, whereas
) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.