Introduction

Petri nets are a very elegant framework to expose the problems of concurrent systems. They allow to define problems in a comprehensible way and to focus on important issues like liveness or boundedness of a given state. Some of the problems concerning liveness and boundedness are counterintuitive. They offer deep didactic value to look for something that appears impossible at the first glance. Solving such problems gives the students much satisfaction. The questionnaires filled anonymously after each course give no doubt about it. But it also demonstrates good understanding of the subject, so such homework can replace the final exam, if the originality of the solution leaves no doubt about the authorship. We will demonstrate solutions for four problems:

1. Find a net and two markings: 𝑀 and 𝑀 ′ such that • 𝑀 is live • 𝑀 ′ ≥ 𝑀 • 𝑀 ′ is not live 2. Find a net and two markings: 𝑀 and 𝑀 ′ such that • 𝑀 is live and bounded • 𝑀 ′ ≥ 𝑀 • 𝑀 ′ is live and not bounded 3. Find a net and initial marking M such that • 𝑀 is live and bounded • the reachability graph of 𝑀 has two finals (two maximal strongly connected components).

Find a net and initial marking M such that

• 𝑀 is live • there exist two places 𝑝 1 , 𝑝 2 , such that they are both unbounded, but not simultaneously.

Definitions

Petri nets are triples ⟨𝑃, 𝑇, 𝐹 ⟩, where 𝑃 and 𝑇 are finite, nonempty and disjoint sets of places and transitions respectively, while 𝐹 : 𝑃 × 𝑇 ∪ 𝑇 × 𝑃 → N is a function definining the structure of a Petri net graph. We assume that if 𝐹 (𝑥, 𝑦) = 0, then there is no edge in the graph between nodes 𝑥 and 𝑦. A positive value means that the edge connecting 𝑥 and 𝑦 exists and denotes the capacity of the edge, so the number of tokens that will be passing along this arc and the direction of token flow. If for all 𝑥, 𝑦 : 𝐹 (𝑥, 𝑦) ≤ 1, we call such a net simple.

A net is a P-system if the numbers of incoming and outgoing edges of any transition do not exceed one. A net is a T-system if the numbers of incoming and outgoing edges of any place do not exceed one.

Let's fix a net 𝒩 = ⟨𝑃, 𝑇, 𝐹 ⟩. A marking is a mapping from 𝑃 to N. A transition 𝑡 ∈ 𝑇 is enabled at marking 𝑀 , if for all 𝑝 ∈ 𝑃 : 𝑀 (𝑝) ≥ 𝐹 (𝑝, 𝑡). An enabled transition at a given marking 𝑀 can fire changing 𝑀 into 𝑀 ′ according to the rule: for all 𝑝 ∈ 𝑃 : 𝑀 ′ (𝑝) = 𝑀 (𝑝) − 𝐹 (𝑝, 𝑡) + 𝐹 (𝑡, 𝑝). Firing a transition 𝑡 at 𝑀 changing it to 𝑀 ′ is denoted by 𝑀 [𝑡⟩𝑀 ′ . The reachability set of 𝑀 is the smallest set of markings [𝑀 ] satisfying two conditions:

• 𝑀 ∈ [𝑀 ] • if 𝑀 ′ ∈ [𝑀 ] and ∃𝑡 ∈ 𝑇 and 𝑀 ′′ such that 𝑀 ′ [𝑡⟩𝑀 ′′ then 𝑀 ′′ ∈ [𝑀 ].

The reachability graph 𝐺(𝑀 ) of a marking M is a graph ⟨𝑉, 𝐸⟩, where 𝑉 = [𝑀 ] and 𝐸 = {(𝑀 ′ , 𝑀 ′′ ) : ∃𝑡 ∈ 𝑇 : 𝑀 ′ [𝑡⟩𝑀 ′′ }; in this case we presume that the edge between 𝑀 ′ and 𝑀 ′′ is labeled by

𝑡. A subgraph (𝑉 ′ , 𝐸 ′ ) is called a final of (𝑉, 𝐸) iff 𝑉 ′ ⊆ 𝑉, 𝐸 ′ = 𝐸 ∩ (𝑉 ′ × 𝑉 ′

) is a maximal strongly connected component, so any two nodes of 𝑉 ′ are connected by a path in 𝐺(𝑀 ). If the set [𝑀 ] is finite, then finals represent possible ultimate behaviors of a net after making possibly irreversible decisions, during resolving conflicts with transition firings.

A place 𝑝 at marking 𝑀 is bounded, if there exists 𝑘 ∈ N such that ∀𝑀 ′ ∈ [𝑀 ] : 𝑀 ′ (𝑝) ≤ 𝑘. Otherwise we call such a place unbounded at 𝑀 . A marking 𝑀 is bounded if all places are bounded at 𝑀 (or, equivalently, the set

[𝑀 ] is finite). Marking 𝑀 is live if ∀𝑡 ∈ 𝑇 : ∀𝑀 ′ ∈ [𝑀 ] : ∃𝑀 ′′ ∈ [𝑀 ′ ] : 𝑡 is enabled at 𝑀 ′′ . A marking 𝑀 is dead if no transition is enabled at 𝑀 .

A net is well formed, if there exists a live and bounded marking in it. A net is structurally bounded if all markings are bounded. When a net is unbounded, we construct coverability graph following the idea of Karp and Miller [KM69]. Whenever during the construction of the coverability graph a marking bigger than some previously considered node on a path from 𝑀 is created, we replace all the coordinates, which are greater, by a symbol 𝜔 to indicate the possibility of generating arbitrarily many tokens. Additionaly we introduce 𝜔 𝑜 indicating the possibility of generating any odd number of tokens, and 𝜔 𝑒 indicating the possibility of generating any even number of tokens.

For two markings 𝑀, 𝑀 ′ we say that 𝑀 ≤ 𝑀 ′ iff ∀𝑝 ∈ 𝑃 : 𝑀 (𝑝) ≤ 𝑀 ′ (𝑝). We call a property monotonic, if is is preserved under increasing a marking. Otherwise it is called non-monotonic.

We present now four problems with (subjectively) increasing difficulty. All of them seem at the first glance to have no solution, but solutions indeed exist.

Non-monotonicity of liveness

Find a net and two markings: 𝑀 and 𝑀 ′ such that

• 𝑀 is live • 𝑀 ′ ≥ 𝑀 • 𝑀 ′ is not live

This is an old problem, proposed by the first author in the [PNB13] long ago, solved by many, including [WR85]. Here we present the most compact solution consisting of a net with just two transitions and one place. The marking of Figure 1 is live: invariantly the number of tokens on place 𝑝 is odd, so one can always increase the number of them by firing 𝑡 1 , but if we increase the number of tokens in the initial marking to 2, the marking is not live: we can fire 𝑡 2 making a marking dead.

This problem has some important moral: When something goes well, adding some extra goods can destroy wellness. Like it happens in real life, for instance with people who win a fortune on a lottery give up their good jobs, lose friends and end up in disaster. Or in economics, when too much money can trigger unnecessary investments, killing some well working parts of a system.

Non-monotonicity of boundedness for live nets

Find a net and two markings: 𝑀 and 𝑀 ′ such that

• 𝑀 is live and bounded • 𝑀 ′ ≥ 𝑀 • 𝑀 ′ is live and not bounded

This problem is much harder. In fact the first author has been puzzled with this problem by Teruel [ET92], while working together on T-systems and P-systems in 1992. The hypothesis of Teruel was that well-formed P-systems are struturally bounded, which would exclude the example satisfying these requirements. Surprisingly, one of the solutions for this problem is a P-system, which makes the hypothesis false.

The first author proposes this problem to the students, as stated, without a requirement that the net should be a P-system. Maybe this makes the problem even harder. Anyway, the example presented here on Figure 2 with only two places and four transitions is easily verifiable, as can be seen on the coverability graphs. Notice that every transition can be rollbacked with an opposite transition. To be precise, after firing 𝑡 1 the net will restore its marking by firing 𝑡 4 , and after firing 𝑡 2 , the net will restore its marking by firing 𝑡 3 and vice versa. This means that every marking that can activate 𝑡 1 and 𝑡 2 or 𝑡 3 and 𝑡 4 is live. This is because, after applying transitions in some order from such marking, you can always return to the original marking by applying the corresponding opposite transitions in the reverse order. This way, the net will restore a marking, from which it was possible to activate all the transitions at some point. Notice that marking (0, 5) on Figure 2 can activate both 𝑡 3 and 𝑡 4 , so the net with unbounded marking is live. Mind that such an example cannot be found for free-choice nets (a consequence of the rank theorem) [DE94].

Let us present another net on Figure 3 and Figure 4, which was discovered by the second author and will serve as a basis of the solution of the next problem.

𝑝 1 𝑝 2 𝑡 1 𝑡 2 𝑡 3 𝑡 4 2 3 3 4 4 3 3 2 (2, 1) (0, 4) 𝑡 1 (3, 0) 𝑡 3 𝑡 2 (1, 3) 𝑡 4 𝑡 4 𝑡 1

Figure 2: A bounded marking of a P-System net solving the "Non-monotonicity of boundedness for live nets" problem, coverability graphs for bounded and unbounded markings

𝑝 1 𝑝 2 𝑝 3 𝑝 4 𝑝 5 𝑝 6 𝑝 7 𝑡 1 𝑡 2 𝑡 3 𝑡 4 10|0|10|10 01|1|10|10 𝑡 1 01|0|01|01 𝑡 3 10|1|01|01 𝑡 2 𝑡 4

Figure 3: A bounded marking of a net solving the "Non-monotonicity of boundedness for live nets" problem, proposed by second author.

10|0|20|10 01|1|20|10 𝑡 1 01|0|11|01 𝑡 3 10|1|11|01 𝑡 2 01|𝜔 𝑒 |11|01 𝑡 1 10|𝜔 𝑜 |11|01 𝑡 2 10|𝜔 𝑒 |20|10 𝑡 4 01|𝜔 𝑜 |20|10 𝑡 1 𝑡 4 𝑡 1 𝑡 3 𝑡 3 𝑡 4 𝑡 *

Two finals

Find a net and initial marking M such that

• 𝑀 is live and bounded • the coverability graph of 𝑀 has two finals.

To find a net, whose coverability graph has two finals is a very easy task. But adding the requirement of liveness can make the problem pretty hard.

Recently the first author communicated Devillers, who mentioned that the problem was first solved probably by Best and Voss in [BV84].

The solution presented here was proposed by the second author. Mind that the initial marking is live and bounded, and depending on the choice of the first transition to fire, we fall into two different finals, which of course do not share any single marking. The presented reachablility graph leaves no doubt that the problem is solved indeed: after the choice of the first transition to fire, the net falls into disjoint cycles.

To approach this problem, one can start with a net that is modeling the flow of two processes rivaling for an access to a critical section in a concurrent environment. One can add an additional restriction to ensure liveness and eliminate starvation by enforcing on the processes to enter the critical section in an interleaving sequence -one after the other. This scenario can be represented by the net in Figure 5 without the place 𝑎. Tokens in places 𝑖 1 , 𝑖 2 mean accordingly that the process is idle. Place 𝑚 is representing the binary semaphore. Tokens in 𝑐𝑠 1 and 𝑐𝑠 2 mean, that a specific process is in critical section. Token in 𝑒 means that one of the processes just released the semaphore and wants to become idle.

With such a net, we can just add an asymmetry to the net with place 𝑎, which solves the given problem. The solution can be seen on Figure 5.

Asynchronous unboundedness

Find a net and initial marking M such that • 𝑀 is live • there exist two places 𝑝 1 , 𝑝 2 , such that they are both unbounded, but not simultaneously. In other words: for every 𝑘 ∈ N there exists a marking 𝑀 1 ∈ [𝑀 ] with 𝑀 1 (𝑝 1 ) > 𝑘, and there exists a marking 𝑀 2 ∈ [𝑀 ] with 𝑀 2 (𝑝 2 ) > 𝑘, but there exists a constant 𝑚 such that for every

𝑀 ′ ∈ [𝑀 ] either 𝑀 ′ (𝑝 1 ) < 𝑚 or 𝑀 ′ (𝑝 2 ) < 𝑚

The solution for this problem is presented on Figure 6. The net is composed of one net that was used for solving the "Two Finals" problem and two nets that were created by the second author for the "Non-monotonicity of boundedness for live nets" problem. By choosing non-deterministicly the first transition 𝑡 1 or 𝑡 2 , the net will put two tokens either on 𝑎 1 or on 𝑎 2 accordingly, but it will be not possible to achieve two tokens on both these places simultaneaously. As we showed earlier the upper nets with their 𝑎 𝑖 being marked with two tokens are unbounded causing the place 𝑝 𝑖 to achieve any number of tokens. All the three nets are live and taking/adding tokens from places 𝑎 𝑖 by other nets won't affect their liveness in a long run. As a result we've received a live net with places 𝑝 1 and 𝑝 2 that fit the requirements of the problem.

Conclusions

All the presented solutions expose some interesting aspects of net behaviors. Having learned such examples enriches understanding of different non-intuitive properties and interrelations between them. Here the solution of the last example was merely a combination of two previous solutions. Usually students find the last problem being the most difficult.

It is also nice to see that some standard problems from the concurrency theory, like mutex, give an insight to non-trivial solutions of the presented Petri net problems.