Tuesday, October 08, 3:30 p.m.- 5:00 p.m.
Where: 7220 Wean Hall
Gianfranco Ciardo, Professor of Computer Science, College of William and Mary
Symbolic algorithms based on binary-decision diagrams (BDDs) have enabled
the exhaustive logic verification of enormous discrete-state systems.
In state-space generation, the focus of our talk, the currently-known set of
reachable states and the next-state function are compactly encoded using BDDs.
Then, a fixed-point iteration explores the entire state space in as many
steps as the maximum distance of any state from the initial state. However,
the time and (peak) memory requirements can still be excessive for large
We present a novel approach to target systems with globally-asynchronous
locally-synchronous behavior, such as protocols, Petri nets, or concurrent
software. We employ a boolean Kronecker encoding of the next-state function
(an idea originally developed for the exact solution of large Markov chains)
paired with multi-valued decision diagrams (MDDs) to store the state space.
We introduce several improvements made possible by the use of structural
information automatically extracted from the model, such as taking into
account the locality of effect for an event, the symmetry and monotonicity
properties inherent in our MDD manipulations, and, above all, the use
of ``saturation'', a completely different style of fixed-point iteration.
Since these ideas complement each others, the overall effect is cumulative,
and our implementation shows orders of magnitude improvements in both memory
and time over state-of-the-art symbolic tools.