Structured Symbolic Model Checking of Asynchronous Systems

Model checking is a popular technology for assessing the correctness
of discrete-state systems.  Its success, particularly in the hardware
industry, has been made possible by the discovery of Binary Decision
Diagrams (BDDs) as a suitable data structure for compactly storing the
huge state spaces described by synchronous digital circuits.  However,
BDD-based model checking does not scale when analysing asynchronous
systems, such as Petri nets, protocols and concurrent software.

This talk presents a novel algorithm for generating and analysing the
state spaces of asynchronous systems, which employs Multi-valued
Decision Diagrams and Kronecker-based data structures.  These permit
the systematic exploitation of structural information of asynchronous
system models, such as taking into account the locality of effect for
an event, and the use of a new strategy for computing fixed points.
Experimental studies show huge improvements in both memory and time
efficiency when compared to state-of-the-art model checkers.  The talk
concludes by briefly describing recent efforts in parallelising this
particular algorithm and in benchmarking model-checking algorithms in
general.