Modeling is used to analyze complex systems, and computer simulation of the systems is many decades old now. The model has to be computation-friendly in order to carry out the simulations. The book describes Petri nets, the computation-friendly models. It prepares readers for the theory side of Petri nets. The basics, properties, and major application of program verification are discussed. Its textbook format consists of the gradual unfolding of the theory of Petri nets, with exercises at the end of each chapter. Undergraduate/graduate-level semester courses can use it as a textbook.

Chapter 1 provides basic definitions related to Petri nets. It shows how they can be expressed using tables and diagrams. The concepts of places, transitions, firing of transitions, and so on are included in the basics. The last chapter (21) is on higher-level Petri nets. Chapter 2 is on the formal languages recognized by Petri nets. Regular languages (extensively used by compiler-like applications for tokenizing texts) are recognized by Petri nets. The chapter reveals that more languages are recognized by Petri nets than regular languages. Chapter 3 discusses reachability of states with respect to Petri nets and their initializations. It also gives the related covering trees/graphs and properties, which can be proved. Chapter 9 continues with unfolding, that is, reachability with similar properties. A discussion on decidability of the reachability problem can be found in chapters 17 and 18.

Readers interested in developing software packages of Petri nets will like the connection of Petri nets with matrices, which are shown in chapters 4 through 6. The chapters discuss classes of nets such as S-nets, T-nets, and free-choice nets, along with their good properties. Chapter 7 looks at a verification technique using the theories developed in earlier chapters. Chapter 8 is on fairness properties of Petri net simulations. In the system under consideration, fairness refers to the fair distribution of scarce resources. The chapter defines mathematically various levels of fairness in the nets. Chapter 10 explores the computability of Petri nets if they are perceived as computers.

Chapters 11 through 16 are on Petri net synthesis. The design of a net based on given specifications is called synthesis. The specification can be in labeled transition systems/persistence labeled transition systems. The algorithm for synthesis appears in chapter 14. The theorems needed are proved earlier. The method and details are explained through examples. Chapter 16 is about model checking of synthesized Petri nets. A logic language, S4, is formally defined using syntax and semantics.

A programming language having explicit constructs for concurrency are typically process algebra based. The semantics of such languages can be given using Petri nets. Chapters 19 and 20 provide the techniques for writing such semantics. The chapters show how to handle some of the most commonly used programming constructs.