5 - The Coverability Theorems

Summary

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 {s₁, t₁,s₃, t₃,s₇,t₇} is not an S-component; it satisfies the second condition of Definition 5.1, but not the first.