Open Access Article:

The Multi-Paradigm Modeling for Cyber-Physical Systems (MPM4CPS) initiative published a book on the “Foundations of MPM4CPS”. My colleagues and I contributed to the book by writing a chapter about Petri Nets and their use in the verification of non-deterministic systems. The work reviews some basics on Petri Nets and describes the state-of-the-art of current research. I think we did a good job of briefly capturing the essentials of the field.


The study of concurrent and parallel systems has been a challenging research domain within cyber-physical systems community. This chapter provides a pragmatic introduction to the creation and analysis of such system models using the popular Petri nets formalism. Petri nets is a formalism that convinces through its simplicity and applicability.We offer an overview of the most important Petri nets concepts, analysis techniques and model checking approaches. Finally, we show the use of so-called High-level Petri nets for the representation of complex data structures and functionality and present a novel research approach that allows the use of Petri nets inside Functional Mock-up Units and cyber-physical system models.