Vol-3170/short1
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | |
| id | Vol-3170/short1 |
| wikidataid | →Q117351473 |
| title | The Chameleon Game |
| pdfUrl | https://ceur-ws.org/Vol-3170/short1.pdf |
| dblpUrl | https://dblp.org/rec/conf/apn/Desel22 |
| volume | Vol-3170→Vol-3170 |
| session | → |
The Chameleon Game
The Chameleon Game
Jörg Desel
FernUniversität in Hagen, Germany
Abstract
A little puzzle is presented, together with a corresponding Petri net model. Conditions for deadlock-
freedom and for the termination property are proven necessary and sufficient. This example might be
helpful for education issues w.r.t. modeling of systems, modeling of properties, techniques for decid-
ing deadlock-freedom and for termination such as siphons and invariants and, more generally, proof
techniques.
Keywords
Petri Net Examples, Education, Deadlock-Freedom, Termination, Proof Techniques, Chameleons
1. Introduction
A usual way to teach programming is to explain the programming language syntax, a number of
example programs, and its runs, and then expect that students can construct their own programs
independently for a given requirement. The same holds respectively for teaching modeling
and for teaching model analysis. In fact, good students survive this impertinence, but many
other students do not get the feeling of how to model, analyze, or prove properly. In particular,
they might be able to reproduce very small and trivial examples but fail to make the transfer
to application. This is not surprising: Imagine that in music classes students would first learn
the syntax for the language of music, i.e., the interpretation of notes, clefs, keys etc. Later
they hear concerts from Mozart and Beethoven and then are expected to be able to compose
their own music. Instead, what is absolutely necessary for learning music, programming, or
modeling is training by examples of different, increasing complexity and size, where training
means independent work on related tasks.
This article presents an example that is claimed to be useful for learning modeling with
Petri nets, model analysis, and proofs based on models. In fact, existing textbook literature on
modeling intentionally starts with very simple examples, because students are not supposed to
spend time on understanding the example, but on the concepts being taught. More application
oriented literature uses more complex models, but often the emphasis or the learning goal
is within the application domain and not on modeling. However, some good examples of
medium sized modeling tasks and sample solutions can be found. Yet, to the best of my
knowledge, there is no systematic collection of them. One exception is the collection of example
in Wolfgang Reisig’s book on distributed algorithms [1], which provides lots of modeling and
PNSE’22, International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022
" joerg.desel@fernuni-hagen.de (J. Desel)
~ https://www.fernuni-hagen.de/sttp/team/joerg.desel.shtml (J. Desel)
© 2022 Copyright for this paper by its author. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
202
�Jörg Desel CEUR Workshop Proceedings 202–210
model analysis examples for high-level Petri nets, but I doubt that many students would be
ready to independently create models on that level.
This short paper just provides a modeling example on a much lower level, suitable for
beginners like graduates of the Petri Net Course of the annual Petri Net Conference or of the
Petri Net Advanced Course series. It only applies elementary concepts of low-level Petri nets,
but also typical proof techniques, recognizing that simple application of invariants, siphons,
and such things are not sufficient in most application examples.
My personal motivation for this work is that I found the task statement completely inde-
pendent from the typical Petri net modeling world, that the problems mentioned are neither
completely trivial nor unsolvable, and that this example is beautiful in two ways: it is a beautiful
problem, and Petri nets can provide a beautiful solution.
2. The Chameleon Game
I recently found the following puzzle in the German online magazin SPIEGEL online [2], based
on [3]:
Some chameleons live quite happily in a large terrarium. There are six in all:
four red, two blue, and a green one. These chameleons have a strange property:
whenever two chameleons of different colors meet, both take on the third color.
For example, when a blue and a green chameleon meet, they both turn red. And
when a red and a green chameleon meet, they both turn blue.
Question: Can it happen that at some point in time all the chameleons have the
same color?
Additional questions: What is the answer if at the beginning five chameleons are
red, two are blue and one is green? What if six chameleons are red, two are blue
and one is green?
The solutions to two of the questions are given and proven without any formal model in
[2]. In this contribution, we aim to show that the puzzle is very well suited to train Petri net
modeling, and that the above questions, as well as related questions, can be solved using Petri
net methods.
It is easily seen that the property “all chameleons have the same color" of this example
coincides with the deadlock property of a Petri net model, as long as only the behavior mentioned
above is modeled. Generally, a deadlock is a state in which no (further) action is possible – in
Petri net models it is a marking which enables no transition. A system or an initially marked
Petri net is said to be deadlock-free, if no reachable state or marking is a deadlock.
So, for a Petri net model of the Chameleon game, the above questions translate to the questions
whether the net with respective initial markings is deadlock-free or not.
Figure 1 shows a Petri net model of the chameleon game, which we shall call chameleon net
in this paper (for educational issues, students should be asked to provide the model!).
The initial marking of the chameleon net depends on the initial numbers of chameleons and
their colors. The figure shows the initial situation with four red chameleons, two blue ones,
and one green one, as in the first question above.
203
�Jörg Desel CEUR Workshop Proceedings 202–210
bgr
2
red
2 2
Figure 1: Petri net model of the Chameleon Game
In this contribution, we will only consider this chameleon Petri net and will use the following
notations: The initial marking 𝑚0 of the net will be denoted by (𝑟0 , 𝑏0 , 𝑔0 ) where 𝑟0 = 𝑚0 (𝑟𝑒𝑑),
𝑏0 = 𝑚0 (𝑏𝑙𝑢𝑒), and 𝑔0 = 𝑚0 (𝑔𝑟𝑒𝑒𝑛). Similarly, we describe general markings 𝑚 by (𝑟, 𝑏, 𝑔).
We assume that the readers know the concepts of occurrence rule for Petri nets (with arc
weights) and occurrence sequences (finite and infinite ones). Moreover, we assume the incidence
matrix of a net to be known. We will also mention marking graphs, place invariants and siphons.
For definitions, see any textbook on Petri nets like [4] or see [5].
The following section presents a deadlock-freedom analysis of the chameleon net, providing
answers to the above questions. We will characterize deadlock-free initial markings, i.e., initial
markings that make the marked chameleon net deadlock-free. For initial markings which are
not deadlock-free we will provide a strategy how to fire transitions in such a way that a deadlock
will be reached eventually.
Section four considers a similar, but different question: Will the chameleon net inevitably
reach a deadlock, provided that in each non-deadlocked marking a transition occurs? We call
this property termination property and say that the net with a given initial marking satisfying
the termination property terminates. If a net does not terminate, then it is possible to keep on
firing transitions forever, which means that infinite occurrence sequences exist. Note that a
non-terminating net may run into a deadlock, but does not necessarily do so. We will analyze
the chameleon net w.r.t. termination and provide a sufficient and necessary condition for this
property in terms of the initial marking. We will provide a strategy how to avoid deadlocks for
non-terminating initial markings of the chameleon net.
3. Deadlock-Freedom
As long as there are chameleons with different colors, they might meet and change colors. That
is, a transition can occur in the chameleon net. When, conversely, all chameleons are of the
same color, nothing can happen anymore and the corresponding marking of the Petri net does
204
�Jörg Desel CEUR Workshop Proceedings 202–210
not enable any transition and therefore is a deadlock. We consider the following three questions:
1. Is there a finite occurrence sequence from marking (4, 2, 1) to a deadlock?
2. Is there a finite occurrence sequence from marking (5, 2, 1) to a deadlock?
3. Is there a finite occurrence sequence from marking (6, 2, 1) to a deadlock?
In the positive case, the answer is simple: a suitable occurrence sequence leading to a deadlock
is a sufficient answer. In the negative case, however, we are looking for a proof that no such
occurrence sequence exists.
Question 1 is easily answered by
𝑟𝑏𝑔 𝑔𝑟𝑏 𝑔𝑟𝑏 𝑔𝑟𝑏
(4, 2, 1) −−→ (3, 1, 3) −−→ (2, 3, 2) −−→ (1, 5, 1) −−→ (0, 7, 0)
and Question 2 by
𝑔𝑟𝑏 𝑟𝑏𝑔 𝑟𝑏𝑔 𝑟𝑏𝑔 𝑟𝑏𝑔
(5, 2, 1) −−→ (4, 4, 0) −−→ (3, 3, 2) −−→ (2, 2, 4) −−→ (1, 1, 6) −−→ (0, 0, 8).
The reader is invited to find a respective occurrence sequence that leads to a deadlock for
Question 3 ... but will inevitably fail because no such sequence exists. To prove this fact, the
simplest way is to construct the marking graph of the net and verify that each of its nodes has
at least one successor and therefore does not represent a deadlock. But imagine that the initial
marking was (1006, 1002, 1001) – then this procedure was no longer feasible. Instead, both [2]
and [3] present a proof that, for this particular initial marking, no reachable deadlock exists. In
the sequel, we will translate this proof into Petri net jargon.
For analysis of the chameleon net we consider its incidence matrix
⎛ ⎞
2 −1 −1
A = ⎝ −1 2 −1 ⎠
−1 −1 2
where the rows corresponds to the places 𝑟𝑒𝑑, 𝑏𝑙𝑢𝑒 and 𝑔𝑟𝑒𝑒𝑛 and the columns to the transitions
𝑏𝑔𝑟, 𝑔𝑟𝑏 and 𝑟𝑏𝑔. It is well known that, if a transition occurs at marking 𝑚 and leads to marking
𝑚′ , then 𝑚′ is obtained by adding the corresponding column of the incidence matrix to 𝑚. A
place invariant is a vector 𝑖 satisfying 𝑖 · A = (0, 0, 0). The most important property of a place
invariant 𝑖 is that each reachable marking 𝑚 satisfies 𝑖 · 𝑚 = 𝑖 · 𝑚0 . In the chameleon example,
there is only one relevant place invariant, namely (1, 1, 1) (and its multiples), which states that
the overall number of tokens (chameleons) never changes.
The concept of place invariants was generalized in [6] to modulo-invariants. A vector 𝑖 is a
modulo-𝑛-invariant, if 𝑖 · A ≡ 0 (mod 𝑛), i.e., if all entries of 𝑖 · A are multiples of 𝑛. Similar
to place invariants, we have for a modulo-𝑛-invariant 𝑖 that 𝑖 · 𝑚 ≡ 𝑖 · 𝑚0 (mod 𝑛) for each
marking 𝑚 reachable from 𝑚0 , i.e., 𝑖 · 𝑚 − 𝑖 · 𝑚0 is a multiple of 𝑛.
Modulo-3-invariants of the chameleon net will be used in the proof of the following lemma.
The net has the modulo-3-invariants (1, −1, 0), (1, 0, −1), (0, 1, −1) and (1, 1, 1) (every place
invariant is also a modulo-𝑛-invariant for every 𝑛), as well as sums and differences of these
vectors. For example, (1, −1, 0) states that the difference between the respective numbers of red
205
�Jörg Desel CEUR Workshop Proceedings 202–210
and blue chameleons will always differ from the initial difference by a multiple of 3. In the exam-
ple shown in Figure 1, for every reachable marking 𝑚 we have 𝑟 − 𝑏 ∈ {. . . , −4, −1, 2, 5, . . .}
because 𝑟0 − 𝑏0 = 2.
The following lemma considers the case that a deadlock is reachable where all chameleons
are red. The other two options of deadlocks (all chameleons blue or all chameleons green) are
similar. For technical reasons, the case that there are no chameleons at all is excluded.
Lemma 1. Assume 𝑟0 + 𝑏0 + 𝑔0 > 0.
The marking (𝑟0 + 𝑏0 + 𝑔0 , 0, 0) is reachable from 𝑚0 if and only if
𝑏0 ≡ 𝑔0 (mod 3) and 𝑟0 + 𝑏0 > 0 and 𝑟0 + 𝑔0 > 0.
Proof.
=⇒
Assume that (𝑟0 + 𝑏0 + 𝑔0 , 0, 0) is reachable from (𝑟0 , 𝑏0 , 𝑔0 ).
𝑏0 ≡ 𝑔0 (mod 3) follows by the mod-3 invariant (0, 1, −1) and because 0 = 𝑏 = 𝑔 = 0 ≡
0 (mod 3) .
𝑟0 +𝑏0 > 0 since otherwise the initial marking is a deadlock (0, 0, 𝑔0 ) with 𝑔0 = 𝑟0 +𝑏0 +𝑔0 > 0,
contradicting reachability of (𝑟0 + 𝑏0 + 𝑔0 , 0, 0).
Similarly, 𝑟0 + 𝑔0 > 0 since otherwise the initial marking is a deadlock (0, 𝑏0 , 0) with 𝑏0 > 0.
⇐=
Assume 𝑏0 ≡ 𝑔0 (mod 3), 𝑟0 + 𝑏0 > 0, 𝑟0 + 𝑔0 > 0. We proceed by induction on max(𝑏0 , 𝑔0 ).
Base. If max(𝑏0 , 𝑔0 ) = 0 then 𝑚0 = (𝑟0 , 0, 0) and we are finished.
Step. Assume that max(𝑏0 , 𝑔0 ) > 0. We show that we can reach a marking (𝑟, 𝑏, 𝑔) from
(𝑟0 , 𝑏0 , 𝑔0 ) such that
𝑏 ≡ 𝑔 (mod 3), 𝑟 + 𝑏 > 0, 𝑟 + 𝑔 > 0, max(𝑏, 𝑔) < max(𝑏0 , 𝑔0 ).
Then, by the induction hypothesis, (𝑟0 + 𝑏0 + 𝑔0 , 0, 0) can be reached from (𝑟, 𝑏, 𝑔) and thus
from (𝑟0 , 𝑏0 , 𝑔0 ), too.
In the cases considered below we use (𝑏−𝑔) ≡ (𝑏0 −𝑔0 ) ≡ 0 (mod 3). This is because (0, 1, −1)
is a modulo-3-invariant of the chameleon net. Moreover, we have 𝑟 + 𝑏 + 𝑔 = 𝑟0 + 𝑏0 + 𝑔0
because (1, 1, 1) is a place invariant.
If 𝑏0 > 0 and 𝑔0 > 0, then we fire 𝑏𝑔𝑟, yielding the marking (𝑟 = 𝑟0 + 2, 𝑏 = 𝑏0 − 1, 𝑔 = 𝑔0 − 1).
Then 𝑟 + 𝑏 = 𝑟0 + 𝑏0 + 1 > 1, 𝑟 + 𝑔 = 𝑟0 + 𝑔0 + 1 > 1 and max(𝑏, 𝑔) = max(𝑏0 , 𝑔0 ) − 1.
If 𝑏0 = 0 then, by assumptions, 𝑟0 > 0 and 𝑔0 > 0. Since 𝑏0 ≡ 𝑔0 (mod 3) we obtain 𝑔0 ≥ 3. We
fire 𝑔𝑟𝑏. Then 𝑟 = 𝑟0 − 1, 𝑏 = 2, 𝑔 = 𝑔0 − 1 ≥ 2. So max(𝑏, 𝑔) = 𝑔 = 𝑔0 − 1 = max(𝑏0 , 𝑔0 ) − 1.
Since 𝑏 = 2 and 𝑔 ≥ 2 we have 𝑟 + 𝑏 > 0 and 𝑟 + 𝑔 > 0.
The case 𝑔0 = 0 is similar by symmetry; we fire 𝑟𝑏𝑔.
206
�Jörg Desel CEUR Workshop Proceedings 202–210
Corollary 1. A deadlock is reachable if and only if
𝑏0 ≡ 𝑔0 (mod 3) or 𝑔0 ≡ 𝑟0 (mod 3) or 𝑟0 ≡ 𝑏0 (mod 3).
In other words, no deadlock is reachable if and only if
{(𝑏0 − 𝑔0 ), (𝑔0 − 𝑟0 ), (𝑟0 − 𝑏0 )} ≡ {0, 1, 2} (mod 3)
where equivalence modulo 𝑛 is defined on sets elementwise.
Proof. The only possible reachable deadlocks are (𝑟0 + 𝑏0 + 𝑔0 , 0, 0), (0, 𝑟0 + 𝑏0 + 𝑔0 , 0) and
(0, 0, 𝑟0 + 𝑏0 + 𝑔0 ). In the first case, 𝑏 = 𝑔 and therefore, by the modulo-3-invariant (0, 1, −1)
we have 𝑏0 ≡ 𝑔0 (mod 3). For the other two cases, the same argument applies to the respective
other pairs of places.
Conversely, assume that one of the conditions, say 𝑏0 ≡ 𝑔0 (mod 3) holds true. If 𝑟0 + 𝑏0 >
0 and 𝑟0 + 𝑔0 > 0, then the result follows from Lemma 1. Otherwise, either 𝑟0 = 𝑏0 = 0 or
𝑟0 = 𝑔0 = 0 and thus the initial marking is already a deadlock. This is in particular the case if
all places are initially unmarked.
By symmetry, Lemma 1 can be applied for the other conditions in the same way.
The proof of Lemma 1 also shows a strategy to reach a deadlock, if possible. When we assume
that 𝑥0 ≡ 𝑦0 ≡ 0 (mod 3) (𝑥 ̸= 𝑦), which has to be the case for some places 𝑥 and 𝑦 by the
lemma, then we give priority to the transition which has both 𝑥 and 𝑦 in its pre-set, until one (or
both) of these places are unmarked. In case both are unmarked, a deadlock is reached. In case
only one of these places is unmarked, we fire the transition that adds two tokens to this place
(and takes away a token from the other place) and then continue with the prioritized transition.
Now let‘s come back to the three questions asked initially regarding three particular ini-
tial markings of the chameleon net. From the initial marking (4, 2, 1) a deadlock can be
reached because 4 ≡ 1 (mod 3). From the marking (5, 2, 1) a deadlock can be reached
because 5 ≡ 2 (mod 3). From the marking (6, 2, 1) no deadlock can be reached because
{6, 2, 1} ≡ {0, 1, 2} (mod 3), i.e., the numbers 6, 2 and 1 represent all three equivalence classes
modulo 3.
4. Termination
In the previous section we aimed at characterizing initial markings of the chameleon net with
the property that a deadlock is reachable. Moreover, we provided a strategy to reach a deadlock,
if possible.
Now we take the opposite view and try to avoid deadlocks. So our first question is whether
the net with a given initial marking necessarily reaches a deadlock eventually or if the initial
marking enables an infinite occurrence sequence. Again, we aim at a characterization of those
initial markings that allow for infinite occurrence sequences, and in turn of initial markings
that make the net terminating eventually.
As seen in the previous section, deadlock states of the chameleon game are easily characterized:
A state of the chameleon game is a deadlock if and only if all chameleons have the same color
207
�Jörg Desel CEUR Workshop Proceedings 202–210
and hence no color change is possible any more. In terms of markings of the chameleon net, a
marking is a deadlock marking, if and only if (at least) two of the places 𝑟𝑒𝑑, 𝑏𝑙𝑢𝑒 and 𝑔𝑟𝑒𝑒𝑛
are unmarked. So the question from above translates to the question whether it is possible to
fire transitions in such a way that always at most one place is unmarked.
An analysis of the chameleon net shows that the net has three minimal siphons: {𝑟𝑒𝑑, 𝑏𝑙𝑢𝑒},
{𝑏𝑙𝑢𝑒, 𝑔𝑟𝑒𝑒𝑛} and {𝑔𝑟𝑒𝑒𝑛, 𝑟𝑒𝑑}. So the deadlocks are exactly those markings where a siphon
is unmarked. Remember that, in general, whenever a marking is a deadlock, some siphon is
unmarked. In our example net, the converse holds as well.
If the initial marking is already a deadlock, then the answer to the above question is simple and
negative. Otherwise we look at the last marking before reaching a deadlock. It is easily seen that
at this marking two places must carry exactly one token each, and that the transition removing
these two tokens leads to the deadlock. So we can avoid reaching a deadlock immediately if
at least one of the input places of the according transition carries at least two tokens. The
following lemma states that this condition is also sufficient for non-termination, i.e., for the
existence of an infinite occurrence sequence.
Lemma 2. The chameleon has an infinite occurrence sequence if and only if initially one of its
places carries at least two tokens and another place carries at least one token.
Proof. Assume that 𝑚0 (𝑥) ≥ 2 and 𝑚0 (𝑦) ≥ 1, where 𝑥 and 𝑦 are distinct places (and 𝑧 is the
remaining place). Then the transition in the pre-set of 𝑧 is enabled. Its occurrence leads to a
marking 𝑚 with 𝑚(𝑧) = 𝑚0 (𝑧) + 2 ≥ 2 and 𝑚(𝑥) = 𝑚0 (𝑥) − 1 ≥ 1. So we have the same
situation as initially: one place carries at least two tokens (now it is 𝑧) and a distinct place (now
𝑥) carries at least one token. This argument can be repeated arbitrarily, and a deadlock is never
reached. In other words: Applying this strategy, the condition is invariant.
Conversely, assume that there is an infinite occurrence sequence from the initial marking
(𝑟0 , 𝑏0 , 𝑔0 ). Consider the first two transition occurrences 𝑢 and 𝑣 in this sequence, i.e., the
sequence starts with 𝑢 𝑣. If 𝑢 = 𝑣, then both places in the pre-set of this transition carry initially
at least two tokens. If 𝑢 ̸= 𝑣 then the place which is neither in the post-set of 𝑢 nor in the
post-set of 𝑣 is in both pre-sets. Hence it initially carries at least two tokens, because 𝑢 𝑣 is
enabled at 𝑚0 . The other place in the pre-set of 𝑢 carries initially at least one token, because 𝑢
is enabled at 𝑚0 .
In terms of chameleons, Lemma 2 states that the game does not terminate if and only if
at least two chameleons have the same color and two chameleons have different color. The
following corollary provides a characterization of the negated property:
Corollary 2. The chameleon game terminates if and only if at least one of the following conditions
holds:
1. Two places are unmarked (all chameleons have the same color)
2. The overall number of tokens is less than three (there are less than three chameleons)
3. All three places carry exactly one token initially (there is one red, one blue and one green
chameleon)
208
�Jörg Desel CEUR Workshop Proceedings 202–210
It might be worth mentioning that for four or more chameleons, the net inevitably terminates
if and only if the initial marking is already a deadlock, because otherwise at least one of the
three colors must appear twice and also different colors appear. For three chameleons, the net
moreover terminates if all chameleons have different colors, because after one (arbitrary) step,
they all will have the same color. For two chameleons, either the initial marking is a deadlock
(same color) or a deadlock is reached after one step (different color), whereas one chameleon
will stay lonely forever anyway and zero chameleons do not have to be considered.
5. Conclusion
We have presented a puzzle, translated it into Petri nets and used Petri net analysis techniques
for finding answers to the puzzle and other relevant information. None of this constitutes
results to scientific problems nor to real world applications. However, the chameleon net
presented in this paper can be used in many ways to explain how to model systems with Petri
nets (in the small) and how to provide answers to questions about a system using Petri net
techniques. The chameleon example can be used for motivation and explanation of Petri net
analysis techniques as well as for various student exercises, where students are asked to find
solutions based on learned Petri net techniques and general proof techniques. For example, the
example can be used as a motivating example for the introduction of modulo-invariants. In this
case, students are asked to find the particular invariant property that holds for this net, and
then modulo-invariants are introduced as a general concept that formalizes this invariant. If
modulo-invariants are already known, then the example can be used as an exercise of finding
an appropriate modulo-invariant.
A particular importance of examples like this one is that students get a feeling for when
which modeling construct and which analysis method can be used and/or is promising, also in
a bigger setting.
The Petri net community lacks a systematic collection of nontrivial examples, although small
examples can be found in many scientific papers and textbooks on Petri nets. For explaining a
new technique, the examples are just big enough to understand the new idea, but often the same
results could easily be obtained without the technique. On the other hand, industrial examples
are here and there published, but in general they can hardly be used for educational purpose –
too many aspects are relevant in practice, the examples are too large to be used in classes, and
students can only take the role of recipients, where no active engagement is possible.
I hope that this and existing or new examples of medium complexity and difficulty will be
collected in future to serve as an example collection for the community, as a pool for educational
purposes, but also as a source to test new techniques and compare with existing ones.
References
[1] W. Reisig, Elements of distributed algorithms: modeling and analysis with Petri nets,
Springer, 1998.
[2] H. Dambeck, M. Niestedt, Verwirrspiel im Terrarium, https://www.spiegel.de/karriere/
209
�Jörg Desel CEUR Workshop Proceedings 202–210
verwirrspiel-im-terrarium-raetsel-der-woche-a-404e0560-ca83-418c-a5f3-8acfa3167d3d,
2021. Accessed: 2022-03-01.
[3] A. Beutelspacher, Das Geheimnis der zwölften Münze: Neue mathematische Knobeleien,
C.H.Beck, 2021.
[4] W. Reisig, Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical
Computer Science, Springer, 1985.
[5] J. Desel, J. Esparza, Free Choice Petri Nets, Cambridge University Press, USA, 1995.
[6] J. Desel, K.-P. Neuendorf, M.-D. Radola, Proving nonreachability by modulo-invariants,
Theoretical Computer Science 153 (1996) 49–64.
210
�