Symbolic Verification with Periodic Sets

Symbolic approaches attack the state explosion problem by introducing
implicit representations that allow the simultaneous manipulation of
large sets of states. The most commonly used representation in this
context is the Binary Decision Diagram (BDD). This paper takes the
point of view that other structures than BDD's can be useful for
representing sets of values, and that combining implicit and explicit
representations can be fruitful. It introduces a representation
of complex periodic sets of integer values, shows how this
representation can be manipulated, and describes its application to the
state-space exploration of protocols. Preliminary experimental results
indicate that the method can dramatically reduce the resources
required for state-space exploration.