The Power of QDDs

Queue-content Decision Diagrams (QDDs) are finite-automaton based
data structures for representing (possibly infinite) sets of contents
of a finite collection of unbounded FIFO queues. Their intended use is
to serve as a symbolic representation of the possible queue contents
that can occur in the state space of a protocol modeled by
finite-state machines communicating through unbounded queues. This is
done with the help of a loop-first search, a state-space exploration
technique that attempts whenever possible to compute symbolically the
effect of repeatedly executing a loop any number of times, making it
possible to analyze protocols with infinite state spaces though
without the guarantee of termination. This paper first solves a key
problem concerning the use of QDDs in this context: it precisely
characterizes when, and shows how, the operations required by a
loop-first search can be applied to QDDs. Then, it addresses the
problem of exploiting QDDs and loop-first searches to broaden the
range of properties that can be checked from simple state reachability
to temporal logic. Finally, a sufficient criterion for the
termination of a loop-first search using QDDs is given.