Throughout the rest of the book we study the properties of live and bounded free-choice systems. In this chapter, we prove the S-coverability Theorem and the T-coverability Theorem, which state that well-formed free-choice nets can be decomposed in two different ways into simpler nets. Together with Commoner's Theorem, the Coverability Theorems are part of what can be called classical free-choice net theory, developed in the early seventies.

The S-coverability Theorem

Figure 5.1 shows a live and bounded (even 1-bounded) free-choice system that we shall frequently use to illustrate the results of this and the next chapters. Its underlying well-formed free-choice net can be decomposed into the two S-nets shown at the bottom of the figure. Observe that they are connected to the rest of the net only through transitions. We prove in this section that every well-formed free-choice net can be decomposed in this way.

Definition 5.1S-components

Let N′ be the subnet of a net N generated by a nonempty set X of nodes. N′ is an S-component of N if

• •s ∪ s• ⊆ X for every place s of X, and

• N′ is a strongly connected S-net.

The two nets at the bottom of Figure 5.1 are S-components of the net at the top. The subnet generated by {s1, t1,s3, t3,s7,t7} is not an S-component; it satisfies the second condition of Definition 5.1, but not the first.

This chapter presents the main results of the theory of S-systems and T-systems. It is divided into two sections of similar structure, one for each of these two classes. The main results of each section are a Liveness Theorem, which characterizes liveness, a Boundedness Theorem, which characterizes b-boundedness of live systems, and a Reachability Theorem, which characterizes the set of reachable markings of live systems. Additionally, both sections contain a Shortest Sequence Theorem, which states that every reachable marking can be reached by an occurrence sequence whose length is bounded by a small polynomial in the number of transitions of the net (linear in the case of S-systems and quadratic for T-systems).

S-systems

Recall from the Introduction that S-systems are systems whose transitions have exactly one input place and one output place.

Definition 3.1S-nets, S-systems

A net is an S-net if |•t| = 1 = |t•| for every transition t.

A system (N, M0) is an S-system if N is an S-net.

The fundamental property of S-systems is that all reachable markings contain exactly the same number of tokens. In other words, the total number of tokens of the system remains invariant under the occurrence of transitions.

Proposition 3.2Fundamental property of S-systems

Let (N, M0) be an S-system. If M is a reachable marking, then M0(S) = M(S), where S is the set of places of N.

A home marking of a system is a marking which is reachable from every reachable marking; in other words, a marking to which the system may always return. The identification of home markings is an interesting issue in system analysis. A concurrent interactive system performs some initial behaviour and then settles in its ultimate cyclic (repetitive) mode of operation. A typical example of such a design is an operating system which, at boot time, carries out a set of initializations and then cyclically waits for, and produces, a variety of input/output operations. The states that belong to the ultimate cyclic behavioural component determine the central function of this type of system. The markings modelling such states are the home markings.

In Section 8.1 we show that live and bounded free-choice systems have home markings. In Section 8.2 we prove a stronger result: the home markings are the reachable markings which mark all the proper traps of the net.

Existence of home markings

Definition 8.1Home marking

Let (N, M0) be a system. A marking M of the net N is a, home marking of (N, M0) if it is reachable from every marking of [M0〉.

We say that (N, M0) has a home marking if some reachable marking is a home marking.

Using the results of Chapter 3, we can easily prove the following proposition.

Proposition 8.2Home markings of live S- and T-systems

Every reachable marking of a live S-system or a live T-system is a home marking.

This book developed out of lecture courses in Uncertain Reasoning given at the University of Manchester in 1989 and 1991 as part of the Master of Science degree in Mathematical Logic and is aimed at readers with some mathematical background who wish to understand the mathematical foundations of the subject. Thus the emphasis is on providing mathematical formulations, analyses and justifications of what I see as some of the major questions and assumptions underlying present day theories of Uncertain Reasoning whilst avoiding, as far as possible, lengthy philosophical discussions on the one hand and precise computer algorithms on the other. Much of the material presented appears already, in some form or other, in published papers, so that my main contribution is the assembling and presenting of it within a unified framework.

My hope is that by doing so I might encourage more ‘mathematicians’ to take an active interest in the subject whilst at the same time offering to those currently working on practical applications in the field easy access to some of the mathematics underlying their assumptions. In short it is the sort of book which I wish had been available to me when I first entered the area.

The subject of Uncertain Reasoning (also referred to as Approximate Reasoning and Reasoning under Uncertainty) dates back to Plato, if not beyond, but has seen an exponential expansion in the last decade with the drive towards intelligent computers, especially so called expert systems.

Petri nets are one of the most popular formal models of concurrent systems, used by both theoreticians and practitioners. The latest compilation of the scientific literature related to Petri nets, dating from 1991, contains 4099 entries, which belong to such different areas of research as databases, computer architecture, semantics of programming languages, artificial intelligence, software engineering and complexity theory. There are also several introductory texts to the theory and applications of Petri nets (see the bibliographic notes).

The problem of how to analyze Petri nets – i.e., given a Petri net and a property, how to decide if the Petri net satisfies it or not – has been intensely studied since the early seventies. The results of this research point out a very clear trade-off between expressive power and analyzability. Even though most interesting properties are decidable for arbitrary Petri nets, the decision algorithms are extremely inefficient. In this situation it is important to explore the analyzability border, i.e., to identify a class of Petri nets, as large as possible, for which strong theoretical results and efficient analysis algorithms exist.

It is now accepted that this border can be drawn very close to the class of free-choice Petri nets. Eike Best coined the term ‘free-choice hiatus’ in 1986 to express that, whereas there exists a rich and elegant theory for free-choice Petri nets, few of its results can be extended to larger classes. Since 1986, further developments have deepened this hiatus, and reinforced its relevance in Petri net theory.