<?xml version="1.0"?>
<feed xmlns="http://www.w3.org/2005/Atom" xml:lang="en">
	<id>http://ceur-ws.bitplan.com/index.php?action=history&amp;feed=atom&amp;title=Vol-3170%2Fshort1</id>
	<title>Vol-3170/short1 - Revision history</title>
	<link rel="self" type="application/atom+xml" href="http://ceur-ws.bitplan.com/index.php?action=history&amp;feed=atom&amp;title=Vol-3170%2Fshort1"/>
	<link rel="alternate" type="text/html" href="http://ceur-ws.bitplan.com/index.php?title=Vol-3170/short1&amp;action=history"/>
	<updated>2026-04-04T08:01:29Z</updated>
	<subtitle>Revision history for this page on the wiki</subtitle>
	<generator>MediaWiki 1.35.5</generator>
	<entry>
		<id>http://ceur-ws.bitplan.com/index.php?title=Vol-3170/short1&amp;diff=1764&amp;oldid=prev</id>
		<title>Wf: edited by wikiedit</title>
		<link rel="alternate" type="text/html" href="http://ceur-ws.bitplan.com/index.php?title=Vol-3170/short1&amp;diff=1764&amp;oldid=prev"/>
		<updated>2023-03-31T11:14:53Z</updated>

		<summary type="html">&lt;p&gt;edited by wikiedit&lt;/p&gt;
&lt;table class=&quot;diff diff-contentalign-left diff-editfont-monospace&quot; data-mw=&quot;interface&quot;&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;tr class=&quot;diff-title&quot; lang=&quot;en&quot;&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;← Older revision&lt;/td&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;Revision as of 11:14, 31 March 2023&lt;/td&gt;
				&lt;/tr&gt;&lt;tr&gt;&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot; id=&quot;mw-diff-left-l8&quot; &gt;Line 8:&lt;/td&gt;
&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot;&gt;Line 8:&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|authors=Jörg Desel&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|authors=Jörg Desel&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|dblpUrl=https://dblp.org/rec/conf/apn/Desel22&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;|dblpUrl=https://dblp.org/rec/conf/apn/Desel22&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td colspan=&quot;2&quot;&gt; &lt;/td&gt;&lt;td class='diff-marker'&gt;+&lt;/td&gt;&lt;td style=&quot;color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;&lt;ins style=&quot;font-weight: bold; text-decoration: none;&quot;&gt;|wikidataid=Q117351473&lt;/ins&gt;&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;}}&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;}}&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;==The Chameleon Game==&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;==The Chameleon Game==&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;/table&gt;</summary>
		<author><name>Wf</name></author>
	</entry>
	<entry>
		<id>http://ceur-ws.bitplan.com/index.php?title=Vol-3170/short1&amp;diff=1763&amp;oldid=prev</id>
		<title>Wf: modified through wikirestore by wf</title>
		<link rel="alternate" type="text/html" href="http://ceur-ws.bitplan.com/index.php?title=Vol-3170/short1&amp;diff=1763&amp;oldid=prev"/>
		<updated>2023-03-31T11:14:46Z</updated>

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