Petri Nets 2012 & ACSD 2012
Hamburg, Germany, June 25–29, 2012
Thomas Chatain, Stefan Haar, Victor Khomenko, G. Michele Pinna
Petri net unfoldings is a prominent formalism for the description and analysis of concurrent systems. On the theoretical side, it provides powerful and aesthetically appealing true concurrency semantics of concurrent models. On the practical side, unfoldings of highly concurrent systems are often much smaller than their reachability graphs, and so alleviate the state space explosion problem. Hence, unfoldings have become the basis of numerous methods and tools for formal verification.
During the two decades that have passed since its introduction by McMillan in 1992, the unfolding technique has been considerably improved, parallelised for shared memory and distributed architectures, and extended from checking reachability properties to ones expressible in Linear Temporal Logic (LTL-X); it has also been extended from "plain" Petri nets to high-level ones, Petri nets with read arcs, time Petri nets, process algebras and many other formalisms. Furthermore, unfoldings have become the inspiration for more sophisticated and compact representations of the set of reachable states of a model, in particular symbolic prefixes and merged processes.
This course will provide a general introduction into unfoldings, unfolding based formal verification and applications of unfoldings. These will be combined with demonstration of some practical unfolding-based tools. Moreover, a number of recent ideas will be considered in more detail, including the reveals relation, symbolic prefixes, and merged processes and related models.
