Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

CHAPTER 5

Introducing Petri Nets

5.1 ABOUT PETRI NETS

Petri nets play an important role in the modeling, analysis, and verification of parallel systems. They are more powerful than finite state machines (automata); in particular, they provide for an efficient representation of concurrent processes. In this chapter we summarize the basic concepts concerning Petri nets. In the sequel we wish to use Petri nets as an alternative way of modeling systems and circuits.

Petri nets are a graphical as well as an algebraic modeling tool, applicable to a large variety of information processing systems. In particular, Petri nets are suitable for modeling and analyzing discrete systems, which involve a high degree of parallelism.

Most introductions to Petri nets rely on graphical representations. In this text we use both graphical as well as textual representations, making extensive use of the helpful tool PETRIFY, which will be introduced in the sequel.

5.1.1 Petri Graphs and Petri Nets

A Petri net PN consists of a Petri graph PG, together with a marking M. A Petri graph is a directed graph with two kinds of nodes (i.e., a “bipartite” graph), called places and transitions. Arcs are either from places to transitions or from transitions to places. In the graphical representation, places are shown as circles and transitions are shown as squares or as bars. A marking M assigns to each place p a nonnegative integer M(p). In the graphical representation, we place M(p) black dots (known as “tokens”) ...