Petri Net Analysis Using Decision Diagrams

This tutorial provides an introduction to the most important classes of decision diagrams and their applications in the area of verification and stochastic or timed modeling. In particular, we show how structured representations can greatly reduce the memory and time required for state-space generation, CTL model checking, numerical solution of Markov chains, and reachability analysis of nondeterministic integer-timed models. We use Petri nets (PNs) as the high-level model specification language, but the algorithms and data-structures presented are widely applicable to many other formalisms commonly used to describe discrete-state systems.