MAT-74506 Model Checking and Petri Nets

- A state space tool for concurrent system models expressed in C++ (A. Valmari 2015)
- Introduction to the ASSET tool.
- An Investigation of the Therac-25 Accidents (N. Leveson & C.S. Turner 1993)
- A HTML version of the famous analysis of the famous series of accidents.
- Anatomy of the Pentium Bug (V. Pratt 1995)
- The Pentium bug cost Intel $475,000,000.
- Can Stubborn Sets Be Optimal? (A. Valmari & H. Hansen 2011)
- Recommended reading on partial-order methods.
*O*(*m*log*n*) Time Algorithms for DFA Minimization and More (A. Valmari 2010)- Slides on block and cord splitting algorithms. The publication “Fast Brief Practical DFA Minimization” is recommended, but unfortunately it is not open access. The DFA minimizer program written in C++ that it describes is available here. The extension to bisimulation minimization is here. Efficient Minimization of DFAs with Partial Transition Functions (A. Valmari, P. Lehtinen 2008) is out of date, but its description on the partition refinement data structure is still relevant, and it is open access.
- Old and New Algorithms for Minimal Coverability Sets (A. Valmari & H. Hansen 2014)
- Recommended reading on minimal coverability sets.
- Petri Nets (J. Esparza 2006)
- A series of slides on Petri nets (focusing on place/transition nets).
- Place/Transition Petri Nets (J. Desel & W. Reisig 1998)
- An extensive introduction to the most common class of Petri nets.
- Rinnakkaisjärjestelmien algoritminen verifiointi (A. Valmari 2007)
- A non-technical non-extensive introduction to verification of concurrent systems and to methods alleviating the state explosion problem. In Finnish.
- The State Explosion Problem (A. Valmari 1998)
- While primarily a survey on methods for alleviating the state explosion problem, it also discusses many issues on model checking. Although it is partially out of date and lacks some important issues, it is a good starting point.
- Visual Verification of Safety and Liveness (A. Valmari & M. Setälä 1996)
- Using Peterson's mutual exclusion algorithm as an example, discusses an approach that uses process-algebraic model checking techniques without the necessity to start by writing a requirements specification.
- What really happened on Mars? (M.B. Jones ↠ G.E. Reeves 1997)
- The Mars Pathfinder started to suffer from repeated system resets. This web page and its sub-pages tell what went wrong and how it was fixed. Be sure to click and read “this detailed first-hand account”.
- What the Small Rubik's Cube Taught Me about Data Structures, Information Theory and Randomisation (A. Valmari 2006)
- Discusses various data structures for storing the reachable states of the cube, aiming more on insight than on technicalities.

More to be added …