2 - Analysis techniques for Petri nets

Summary

This chapter introduces elementary definitions, concepts and results concerning arbitrary Petri nets. We start with a short section on mathematical notation. Section 2.2 is devoted to the definition and properties of nets, markings, the occurrence rule and incidence matrices. Section 2.3 defines net systems as nets with a distinguished initial marking. We give formal definitions of some behavioural properties of systems: liveness, deadlock-freedom, place-liveness, boundedness. Section 2.4 introduces S- and T-invariants, an analysis technique used throughout the book. The relationship between these invariants and the behavioural properties of Section 2.3 is discussed.

The chapter includes six simple but important results, which are very often used in later chapters. They are the Monotonicity, Marking Equation, Exchange, Boundedness, and Reproduction Lemma, and the Strong Connectedness Theorem. We encourage the reader to become familiar with them before moving to the next chapters.

Mathematical preliminaries

We use the standard definitions on sets, numbers, relations, sequences, vectors and matrices. The purpose of this section is to fix some additional notations.

Notation 2.1Sets, numbers, relations

Let X and Y be sets. We write X ⊆ Y if X is a subset of Y, including the case X = Y. X ⊂ Y denotes that X is a proper subset of Y, i.e., X ⊆ Y and X ≠ Y. X\Y denotes the set of elements of X that do not belong to Y. |X| denotes the cardinality of X.