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.

Free-choice Petri nets have been around for more than twenty years, and are a successful branch of net theory. Nearly all the introductory texts on Petri nets devote some pages to them. This book is intended for those who wish to go further. It brings together the classical theorems of free-choice theory obtained by Commoner and Hack in the seventies, and a selection of new results, like the Rank Theorem, which were so far scattered among papers, reports and theses, some of them difficult to access.

Much of the recent research which found its way into the book was funded by the ESPRIT II BRA Action DEMON, and the ESPRIT III Working Group CALIBAN. The book is self-contained, in the sense that no previous knowledge of Petri nets is required. We assume that the reader is familiar with naïve set theory and with some elementary notions of graph theory (e.g. path, circuit, strong connectedness) and linear algebra (e.g. linear independence, rank of a matrix). One result of Chapter 4 requires some knowledge of the theory of NP-completeness.

The book can be the subject of an undergraduate course of one semester if the proofs of the most difficult theorems are omitted. If they are included, we suggest the course be restricted to Chapters 1 through 5, which contain most of the classical results on S- and T-systems and free-choice Petri nets. A postgraduate course could cover the whole book.

All chapters are accompanied by a list of exercises.

This part, which consists of two chapters, gives the basic material.

Chapter 1 is a brief discussion of the required background from (modal-free) propositional logic. There should be nothing in this chapter which you don't know already, although perhaps the style of presentation will be new to you. The variety of modal languages are described in Chapter 2. The polymodal versions are introduced right from the beginning and this brings a greater cohesion to the subject.

Introduction

The propositional modal language is an extension of the pure propositional language formed by adding a battery of new 1-ary connectives (known informally as box connectives). Originally there was just one new connective □, however for many purposes it is necessary to add several (possibly infinitely many) such connectives [i], one for each element i of an index set I. Thus there are many possible modal languages, one for each index set I. The syntax, semantics, and proof systems associated with modal languages are designed to subsume those of the proposition language, in fact, propositional logic can be regarded as the extreme version of modal logic where I = ∅.

The element i of I are called labels and I itself is called the signature of the modal language. Thus two languages are identical precisely when they have the same signature. (We are never going to consider how one language may be be translated into another, so we need not worry about comparison of signatures.)

Unlike the propositional connectives ¬, →, ∧, ∨, ⊤, and ⊥, the box connectives [i] do not have a fixed interpretation. For each formula φ (of the modal language) we may use [i] to obtain a new formula

[i]φ

This may be read in several ways, and different readings suggest different semantics and proof systems.

This book is an introduction to modal logic, more precisely, to classically based propositional modal logic. There are few books on this subject and even fewer books worth looking at. None of these give an acceptable mathematically correct account of the subject. This book is a first attempt to fill that gap.

Apart from its mathematical clarity, some other features of the book are:

• The central concept of the book is that of a labelled transition structure, and polymodal languages are used from the beginning.

• Modal languages are viewed as a tool for analysing the properties of transition structures, not the other way round.

• There is not an overemphasis on syntactic (proof theoretic) matters.

• Nevertheless, a detailed explanation is given of the differences between the weak completeness and Kripke completeness of formal systems.

• Correspondence properties (the expressibility properties of modal languages) are stressed as an important tool.

• Bisimulations are used as a method of comparing transition structures.

• Each chapter has a decent selection of exercises and over one sixth of the book consists of a comprehensive set of solutions to these exercises.

The book is aimed primarily at a computer science readership. However there is no computer science in the book and very little material which is directly attributable to a computer science motivation. Thus the reader of the book may be interested in modal logic in its own right or because of one or several of its applications in computer science.

Introduction

This chapter is one of the first parts of this book that you should read. You might think this is a little strange since it is also one of the last things in the book. However, all of the material in this chapter should appear somewhere, and I believe that it is better if it is all in one place rather than scattered throughout the book. This position is as good as any.

Beginning

Put yourself in the position of a complete beginner to modal logic; someone who already knows the basics of propositional and predicate logic and who now wants to learn something of modal logic. (You may actually be such a person.) There are many reasons why you may want to do this, from mere curiosity to an eventual use in a particular application. What should you do to acquire this knowledge?

One thing you could do is attend a course on modal logic, but let us assume that this is not an option. The other thing to do is read various text books on the subject. Which ones? There are, in fact, only a few possibilities.

The first possibility is [29] by Hughes and Cress well, first published in 1968. This, at the time it was written, was the most comprehensive and accessible introduction to the subject. It contains descriptions of many of the systems that were, and to some extent still are, of interest.