Author: Prof. Gianfranco Ciardo
Department of Computer Science and Engineering, University of California, Riverside, USA, ciardo@cs.ucr.edu

Abstract: Motivated by the need to analyze Petri nets, timed Petri nets, and stochastic Petri nets with very large reachability graphs, this tutorial provides an introduction to several important classes of decision diagrams, going well beyond the well-known BDDs, as well as the algorithms to manipulate them. The considered applications include reachability-set generation, CTL model checking, and p-semiflow analysis for ordinary Petri nets, numerical solution of stochastic Petri nets describing an underlying Markov chain, and reachability analysis for integer-timed Petri nets.

Tutorial Outline: The study of complex discrete-state systems often requires the analysis and manipulation of very large data structures such as sets and relations, or vector and matrices. Recent advances in the area of decision diagrams have made possible the analysis of truly enormous systems, thanks to their ability to compactly encode the required structures in many cases. This full-day tutorial covers these advances in so-called symbolic methods and their impact on the analysis of various classes of Petri nets. Of course, many high-level formalisms commonly used to model discrete systems can also benefit from using decision diagrams.

1. Reachability set generation for Petri nets
• Petri nets: Definition. Enabling and firing rule. Explicit reachability-set generation.
• Binary decision diagrams and their operations: Definition. The set encoded by a BDD. Reduction rule and canonicity. Algorithms for union, intersection, and relational product.
• Symbolic reachability-set for safe Petri nets: Encoding sets of states and the transition relation using BDDs. Partitioned transition relation. A breadth-first algorithm.
• Multiway decision diagrams: The set encoded by an MDD. General reduction rules for MDDs.
• Symbolic reachability-set generation of extended classes of Petri nets: Exploiting asynchronous behavior and loc nhjth unknown variable ranges.
• Accelerated fixpoint computation: Chaining. Saturation.
2. CTL model checking of Petri nets
• Explicit CTL model checking: Definition and explicit algorithms for the EX, EU, and EG operators.
• Symbolic CTL model checking: Encoding the inverse transition relation. Breadth-first symbolic algorithms for the EX, EU, and EG operators. A constrained saturation algorithm for the EU operator. Building the reachability relation to compute the EG operator and consider fairness.
• Integer-valued decision diagrams: Multi-terminal MDDs. Additive edge-valued MDDs. Algorithms for sum, product, and minimum. An algorithm to compute a shortest EF witness.
3. Numerical analysis of Stochastic Petri nets
• Generalized Stochastic Petri nets: Definition of Markov chains. Steady-state and transient solution algorithms for Markov chains. The process underlying a GSPN.
• Real-valued decision diagrams: Multi-terminal MDDs. Multiplicative edge-valued MDDs.
• Numerical solution of Markov chains encoded using decision diagrams: A hybrid-symbolic approach for the exact solution of Markov chains. An approximate solution algorithm for steady-state analysis of Markov chains.
4. Reachability problems in integer-timed Petri nets
• Timed Petri nets: Definition and behavior. The integer-timed case.
• Timed reachability: Definition. A symbolic algorithm using MDDs.
• Earliest reachability: Definition. A symbolic algorithm using additive edge-valued MDDs.
5. Invariant analysis of Petri nets
• P-semiflows: Definition and meaning. Farkas' algorithm.
• A fully symbolic algorithm for p-semiflow computation: Definition of ZBDDs. An extension, zero-suppressed integer-range MDDs.
6. Software support
• A brief survey of existing software analysis tools that use decision diagram technologies, and of existing decision diagram libraries.

Intended audience: The proposed tutorial is targeted at Petri net researchers and practitioners who have an interest in the analysis of very large and complex discrete systems. While a minimal familiarity with basic concepts of Petri net analysis is assumed, all required Petri net definitions, properties, and algorithms will be briefly summarized. Researchers with knowledge of BDDs and their use for symbolic verification (but not of more advanced decision diagram variants and algorithms) may find this tutorial particularly stimulating.

Previous venues: Courses and tutorials on decision diagrams were delivered at 2005 Bertinoro ISS, Decision diagrams and their applications (15 hours, 3 hours per day for 5 days); QEST 2005, Decision diagrams for logic and stochastic modeling (3 hours); SIGMETRICS 2006, Symbolic encodings for stochastic processes (3 hours), and QEST 2009, Petri net analysis using decision diagrams (3 hours). The main difference with respect to the above courses, except the 3-hour QEST 2009 tutorial, is the much stronger emphasis on Petri nets. This emphasis is due to several factors:

• The audience, being already familiar with basic Petri net concepts, will be better equipped to assimilate the new concepts (how to use decision diagrams for various types of analysis).
• Petri nets present some peculiar advantages (e.g., easy symbolic representation of the change of marking due to the firing of a transition) but also some peculiar challenges (e.g., unknown bounds for the marking of each place).
• Much of Ciardo's recent work on advanced use of decision diagrams has been strictly connected to Petri nets, such as symbolic computation of p-semiflows (which was presented at PETRI NETS 2009), or study of timed and earliest reachability on integer-timed Petri nets (which was presented at SOFSEM 2009). Many of these challenging problems can greatly benefit from the use of decision diagrams and, at the same time, motivated the development of new variants of decision diagrams and new manipulation algorithms.

Another difference from past tutorials is the intention to completely drop the topic of Kronecker encodings which, while related and historically relevant, have now been completely subsumed by more elegant and powerful decision diagram encodings. This will leave more time for the core concepts.

Speaker's biography:
Gianfranco Ciardo is a Professor in the Department of Computer Science and Engineering at the University of California, Riverside. He holds a PhD in Computer Science from Duke University and a Laurea in Scienze dell' Informazione from the University of Torino. He has been Visiting Faculty at HP Labs, University of Torino, TU Berlin, ICASE, and National Institute of Aerospace. Prior to joining academia, he worked at Software Productivity Consortium, and CSELT. His interests are logic verification and stochastic modeling, performance and reliability evaluation of hardware/software systems, symbolic model checking, Markov models, discrete-event simulation, and Petri nets. He has published more than 100 papers in journals and conferences, has been on the editorial board of IEEE Transactions on Software Engineering, and is on the editorial board of Transactions on Petri Nets and Other Models of Concurrency. He was a keynote speaker at PNPM 2001, Petri Nets 2004, EPEW/WS-FM 2005, and PDMC 2009.