When: Tuesday, October 08, 3:30 p.m.- 5:00 p.m.

Where: 7220Wean Hall

Gianfranco Ciardo, Professor of Computer Science, College of William and Mary

Special Presentation

Abstract:
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 models. 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.

<< Back