A small high-level Petri net describing the behavior of a simple algorithm with one loop is presented and discussed. The net can run into a deadlock if and only if the algorithm terminates. The behavior of the net is surprisingly complex, so that we provide a tool to visualize possible runs. We ofer the reader a puzzle, ask for a termination proof - and of course provide a solution.
Very often, Petri nets and other formal modeling languages are taught independently of application domains such as software engineering. In addition, the methods used in formal techniques difer significantly from methods in other fields, although both are based on mathematics. Due to the usual study structure in separate modules, taught by diferent professors, students find it dificult to recognize connections and integrate their knowledge.
Since Petri nets have a particularly wide range of uses, it makes sense to use them as a comprehensive bridge in studies. This traditionally happens in some places, for example in the old textbook [1] of Rüdiger Valk and Eike Jessen, which is both a book on Petri nets and on applications in computing systems.
The primary modeling aspect of Petri nets is concurrency. However, many concepts developed for Petri nets are likewise applicable to sequential systems, which can be viewed as a special case of concurrent systems.
This short article presents an example – actually a puzzle or a challenging exercise for students – which integrates three areas of knowledge: programming practice, programming theory and Petri net modeling. The question to be answered is to find a descending measure for a loop, proving that a given algorithm terminates. The algorithm is presented as a Petri net, so that the termination proof is at the same time a termination proof for the Petri net behavior. Since the behavior of the algorithm under consideration turns out to be surprisingly complex, we provide as a web-based educational resource a Python program. This program can be modified by the user and contributes to understanding the behavior of the algorithm. This understanding is essential for finding the required termination argument.
We found the algorithm under consideration by chance. The question in this article meets the two most important beauty criteria: The algorithm itself is very simple and immediately understandable, whereas the question to the students is surprisingly dificult but solvable. Let us end this introduction by providing the algorithm in natural language:
Given two nonzero integers, repeat the following until one of the numbers is zero: If the numbers have diferent signs, add the second number to the first; otherwise, subtract the first from the second.
So, starting e.g. with the pair (
(
Instead of starting with a textual representation of the algorithm, we formalize it by means of the following high-level Petri net (for the ocurrence rule of high-level Petri nets see [2] or [3]). Notice that the initial values of the two tokens and in the two places represent the initial values of the two integers.
This Petri net corresponds to the following algorithm without INPUT and OUTPUT operations, when 0 is the input value for the variable and 0 is the input value for the variable .
INPUT , ∈ Z WHILE · ̸= 0
IF · < 0 THEN
← + ELSE
← −
OUTPUT ,
Actually, repeated calculation of the product · is not the most eficient way to evaluate the conditions after WHILE and IF. Instead, a real implementation would rather check ̸= 0 and ̸= 0 instead of · ̸= 0 and > 0 xor > 0 instead of · < 0.
This example departs from common applications of Petri nets. It deals with integers, a scenario somewhat atypical in the Petri net world, since token numbers on places (token counts) can never be negative. Consequently, these integers are not represented as markings of places but rather as high-level tokens.
Let us start with some observations: • There is an obvious invariant stating that, for each reachable marking, both places carry one token representing an integer each. Therefore, for any reachable marking , we can write () = instead of () = {}, and the same applies to the place . • A transition is only enabled at a marking satisfying () ̸= 0 and () ̸= 0. Since each transition occurrence changes only one of the two tokens, we have () ̸= 0 or () ̸= 0 after any transition occurrence. Consequently, the marking satisfying () = () = 0 can only be reached if this is the initial marking. • Taking the transition guards into account, each reachable marking enables at most one of the two transitions. It enables no transition if and only if one of the two tokens represents the value 0.
Therefore, the behavior is deterministic for each initial marking.
We are interested in termination of the algorithm: Does it terminate for arbitrary input values 0 and 0, or only for some and, if so, for which ones? In terms of Petri nets, we address the question of whether the Petri net can reach a deadlock and, if so, from which initial markings a deadlock can be reached. Given that the behavior of the net is neither concurrent nor nondeterministic, such a deadlock would inevitably be eventually reached – if it is reachable at all.
This question is naturally a task for you, the reader, or for your students.
How would you approach finding an answer? Naturally, you would first test the algorithm with diferent input values 0 and 0 and find that during the process the numbers sometimes become positive, sometimes negative, and also vary in their magnitude . . . and that, ultimately, regardless of the initial values of the variables, one of the two - and thus the product - inevitably turns to zero. The remaining number is then always the greatest common divisor of the initial values, or its negative value, if this concept is generalized from natural numbers to integers.
To prove termination of the algorithm, it is very helpful to find a descending measure, that is, a function Z × Z → N that allocates a natural number to each assignment of the variables and . This number should decrease by at least one with every loop iteration (see e.g. [4] for this and more general termination criteria). In Petri net language, the function, applied to () and (), decreases with every transition occurrence. Once a suitable descending measure is found, (0, 0) indicates for initial values and how many times the transitions can fire at most. That, is, after a finite number of loop iterations there can eventually be no more iterations of the loop, or in Petri net terminology, a deadlock is reached. In our example, this happens precisely when () = 0 or () = 0.
Before we present a solution, a bit more about the genesis of this puzzle. It was planned as a regular exercise for our students and meant to be quite harmless, in the expectation that the algorithm either does not terminate or that a suitable decreasing measure is easy to find. But neither is the case! Since after many experiments it seemed unlikely that the algorithm would not terminate for any initial marking, we concentrated on the search for a descending measure, proving termination generally.
When looking for a descending measure, it helps to look at the algorithm in more detail. For this purpose, it has proven useful to note the respective values of and in a coordinate system, with the -axis representing and the -axis representing . Then arrows represent the changes caused by a loop execution, i.e., if the values and are changed to ′ and ′, then there is an arrow from the point (, ) to the point (′, ′). That is exactly what we have done for several example values in Figure 2. Yellow (horizontal) arrows represent occurrences of transition and blue (vertical) arrows represent occurrences of transition .
And because it’s so easy to make a mistake, we implemented the algorithm and the visualization mentioned above. So you don’t have to repeat this efort. We are happy to provide the tool, which is accessible via https://kalliope1907.github.io/jupyter/notebooks/index.html?path=visualisierung_algorithmus. ipynb. The tool allows to play with the algorithm. It visualizes the live of both variables for arbitrary initial values. Since it can be freely modified by the user – provided she has some practice in Python programming – not only the initial values but also the algorithm itself can be changed. And finally, the tool draws surpringly nice pictures, see the screenshot in Figure 3 for an example.
Before we developed this tool we gave the task to 600 students at the FernUniversität in Hagen in the "Software Engineering" module as an assignment and actually received three responses. The solution we’re about to present is actually a combination of two proposals from students – our previous solution turned out to be less elegant.
We are looking for a mapping : Z × Z → N such that
• (, ) decreases for any loop execution, i.e.,
• If (, ) = 0 then the loop terminates, i.e.,
· < 0 =⇒ ( + , ) < (, )
· > 0 =⇒ (, − ) < (, )
(, ) = 0 =⇒ · = 0
(
The formal definition of our descending measure turns out to be somewhat tedious. It is better understood when you consider the following eight areas of the coordinate system.
We define a mapping : Z ×
Z → N and distinguish ten (!) cases: A more compact version of the definition might be nicer, although less understandable: || · · > || · · || · · < || · · || · · = || · · ̸= 0 || · · = || · · = 0 As one of our students found out, 2 · max(||, ||) can be equivalently replaced by | + | + | − |.
This definition clearly satisfies the second requirement: (, ) = 0 implies · = 0. In fact, since and are integers, we have (, ) ≥ 1 for all other cases.
Why is this function truly a descending measure, i.e., why does its value always decrease? We shall now prove that with each move from values and to values ′ and ′ we get (, ) > (′, ′). For this proof, we restrict our considerations to the special case > 0 and > 0, i.e., to the first quadrant of the coordinate system. It is easy to see that by rotation symmetry the same arguments apply to the other three cases. Note that for = 0 or = 0 nothing has to be shown, because in both cases · = 0 and therefore the loop stops.
Since we assume > 0 and > 0 we obtain · > 0. Therefore ′ = and ′ = − . We thus have to prove (, − ) < (, ).
We distinguish five cases (see the five downward-pointing blue arrows in the coordination system of Figure 2): Case 1: > 2 · .
Then − > . We get (, − ) = 2( − ) − 1 < 2 − 1 = (, ) since > 0. Case 2: = 2 · .
Then − = . We get (, − ) = 1 < 2 − 1 = (, ) since = 2 ≥ 2.
Case 3: 2 · > > .
Then − < . We get (, − ) = 2 < 2 − 1 = (, ) since < .
Case 4: = .
Then − = 0. We get (, − ) = 0 < 1 = (, ) since , > 0.
Case 5: < .
Then − < − < 0. We get (, − ) = 2 − 1 < 2 = (, ).
So in all of these five cases the inequality holds, and it holds in each case for a diferent reason. This completes the proof (we would in fact have 20 diferent cases if we would consider all four quadrants explicitly).
We presented an algorithm and its Petri net representation and proved that this algorithm terminates for all initial values, or, equivalently, that the Petri net terminates for every initial marking.
This exercise links program analysis and Petri net analysis and demonstrates how Petri nets can be used as a (programming) language independent means for the representation of algorithms. In addition, a connection to programming practice is made, as it can be helpful for students to create or use and modify an illustrative tool to understand the behavior of the algorithm.
As Petri nets are particularly useful for modeling the concurrent behavior of systems, they represent distributed algorithm in a natural way. Therefore, Petri net analysis techniques can be applied to analyse termination and other behavioral properties of distributed algorithm, as shown in many examples in [5], for another example see [6].