=Paper=
{{Paper
|id=Vol-2115/ATAED2018-75-90
|storemode=property
|title=Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems
|pdfUrl=https://ceur-ws.org/Vol-2115/ATAED2018-75-90.pdf
|volume=Vol-2115
|authors=Raymond Devillers,Evgeny Erofeev,Thomas Hujsa
|dblpUrl=https://dblp.org/rec/conf/apn/DevillersEH18
}}
==Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems==
https://ceur-ws.org/Vol-2115/ATAED2018-75-90.pdf
Synthesis of Weighted Marked Graphs from
Constrained Labelled Transition Systems
Raymond Devillers1 , Evgeny Erofeev?2 , and Thomas Hujsa( )3
1
Département d’Informatique, Université Libre de Bruxelles,
B-1050 Brussels, Belgium (rdevil@ulb.ac.be)
2
Department of Computing Science, Carl von Ossietzky Universität Oldenburg,
D-26111 Oldenburg, Germany (evgeny.erofeev@uni-oldenburg.de)
3
ONERA/DTIS & Université Fédérale Toulouse Midi-Pyrénées,
F-31055 Toulouse, France (thomas.hujsa@onera.fr)
Abstract. Recent studies investigated the problems of analyzing Petri
nets and synthesizing them from labelled transition systems (LTS) with
two letters (transitions) only. In this paper, we extend these works by
providing new characterizations for the synthesis of two- and three-letter
Weighted Marked Graphs (WMGs), a well-known and useful class of
weighted Petri nets in which each place has at most one input and one
output. In this study, we focus mainly on LTS forming a single circuit.
Also, we develop a sufficient condition of WMG-solvability for an arbi-
trary number of letters. Finally, we show that this sufficient condition is
not necessary in the case of LTS forming a single circuit with five letters.
Keywords: Weighted Petri net, marked graph, synthesis, labelled transition
system, cycles, cyclic words, circular solvability.
1 Introduction
Petri nets form a highly expressive and intuitive operational model of discrete
event systems, capturing the mechanisms of synchronization, conflict and concur-
rency. Many of their fundamental behavioral properties are decidable, allowing
to model and analyze numerous artificial and natural systems. However, most
interesting model checking problems are intractable, and the efficiency of synthe-
sis algorithms varies widely depending on the constraints imposed on the desired
solution. In this study, we focus on the Petri net synthesis problem from a la-
belled transition system (LTS), which consists in determining the existence of a
Petri net whose reachability graph is isomorphic to the given LTS, and building
such a Petri net solution when it exists.
In previous studies on analysis or synthesis, structural restrictions on nets en-
compassed plain nets (each weight equals 1; also called ordinary nets) [19], ho-
mogeneous nets (meaning that for each place p, all the output weights of p are
?
Supported by DFG through grant Be 1267/16-1 ASYST
75
equal) [22, 18], free-choice nets (the net is homogeneous, and any two transitions
sharing an input place have the same set of input places) [9, 22], choice-free nets
(each place has at most one output transition) [21, 16], marked graphs (each
place has at most one output transition and one input transition) [6, 20, 5, 12],
join-free nets (each transition has at most one input place) [22, 8, 17, 18], etc.
More recently, another kind of restriction has been considered, limiting the num-
ber of different transition labels of the LTS [1, 2, 13, 14].
In this paper, we combine this restriction on the number of labels with the
weighted marked graph (WMG) constraint. Moreover, we focus mainly on finite
circular LTS, meaning strongly connected LTS that contain a unique cycle 4 .
In this context, we investigate the cyclic solvability of a word w, meaning the
existence of a Petri net solution to the finite circular LTS induced by the infinite
cyclic word w∞ .
An important purpose of studying such constrained LTS is to better understand
the relationship between LTS decompositions and their solvability by Petri nets.
Indeed, the unsolvability of simple subgraphs of the given LTS, typically ele-
mentary paths (i.e. not containing any node twice) and cycles (i.e. closed paths,
whose start and end states are equal), often induces simple conditions of un-
solvability for the entire LTS, as highlighted in other works [1, 13, 3]. Moreover,
cycles appear systematically in the reachability graph of live and/or reversible
Petri nets [21], which are used to model various real-world applications, such as
embedded systems [15].
Contributions. In this work, we study further the links between simple LTS
structures and the reachability graph of WMG, as follows.
First, we provide a characterization of the 2-letter (i.e. binary) cyclic words solv-
able by a WMG (i.e. WMG-solvable), and extend the analysis to finite cyclic
LTS. We also tackle the case of infinite cyclic LTS with 2 letters. Then, we provide
a general sufficient condition for the WMG-solvability of a cyclic word with an
arbitrary number of letters, using a decomposition into specific WMG-solvable
binary cyclic subwords. We prove that the same sufficient condition becomes a
characterization of WMG-solvability for a subclass of the 3-letter cyclic words.
Finally, we show, with the help of a counter-example, that this sufficient condi-
tion is not necessary for cyclic words with 5 letters.
Organization of the paper. After recalling classical definitions, notations and
properties in Section 2, we present the results of WMG-solvability for 2-letter
words in Section 3. Then, in Section 4, we focus on circular LTS: we develop the
4
A set A of k arcs in a LTS G defines a cycle of G if the elements of A can be ordered
as a sequence a1 . . . ak such that, for each i ∈ {1, . . . , k}, ai = (ni , `i , ni+1 ) and
nk+1 = n1 , i.e. the i-th arc ai goes from node ni to node ni+1 until the first node
n1 is reached, closing the path. Cycles are also called circuits, circles and oriented
cycles.
76
general sufficient condition of WMG-solvability for any number of letters; in the
case of 3 letters, we provide the characterization for a subset of the circular LTS;
and we exhibit the counter-example for 5 letters. Finally, Section 5 presents our
conclusions and perspectives.
2 Classical Definitions, Notations and Properties
LTS, sequences and reachability. A labelled transition system with initial
state, abbreviated LTS, is a quadruple TS = (S, →, T, ι) where S is the set of
states, T is the set of labels, → ⊆ (S × T × S) is the transition relation, and ι ∈ S
is the initial state.
A label t is enabled at s ∈ S, written s[ti, if ∃s0 ∈ S : (s, t, s0 ) ∈→, in which case
s0 is said to be reachable from s by the firing of t, and we write s[tis0 . Generaliz-
ing to any (firing) sequences σ ∈ T ∗ , s[εi and s[εis are always true; and s[σtis0 ,
i.e. σt is enabled from state s and leads to s0 , if there is some s00 with s[σis00 and
s00 [tis0 . A state s0 is reachable from state s if ∃σ ∈ T ∗ : s[σis0 . The set of states
reachable from s is denoted by [si.
Petri nets, reachability and languages . A (finite, place-transition) weighted
Petri net, or weighted net, is a tuple N = (P, T, W ) where P is a finite set of
places, T is a finite set of transitions, with P ∩ T = ∅ and W is a weight function
W : ((P ×T )∪(T ×P )) → N giving the weight of each arc. A Petri net system, or
system, is a tuple S = (N, M0 ) where N is a net and M0 is the initial marking,
which is a mapping M0 : P → N (hence a member of NP ) indicating the initial
number of tokens in each place. The incidence matrix C of the net is the integer
P × T -matrix with components C(p, t) = W (t, p) − W (p, t).
A place p ∈ P is enabled by a marking M if M (p) ≥ W (p, t) for every output
transition t of p. A transition t ∈ T is enabled by a marking M , denoted by
M [ti, if for all places p ∈ P , M (p) ≥ W (p, t). If t is enabled at M , then t can
occur (or fire) in M , leading to the marking M 0 defined by M 0 (p) = M (p) −
W (p, t) + W (t, p); we note M [tiM 0 . A marking M 0 is reachable from M if there
is a sequence of firings leading from M to M 0 . The set of markings reachable
from M is denoted by [M i. The reachability graph of S is the labelled transition
system RG(S) with the set of vertices [M0 i, the set of labels T , initial state M0
and transitions {(M, t, M 0 ) | M, M 0 ∈ [M0 i ∧ M [tiM 0 }. A system S is bounded
if RG(S) is finite.
The language of a Petri net system S is the set L(S) = {σ ∈ T ∗ | M0 [σi}. These
languages are prefix-closed, i.e., if σ = σ 0 σ 00 ∈ L(S), then σ 0 ∈ L(S). For any
language L ⊆ T ∗ , we denote by P REF (L) the language formed by its prefixes.
Vectors. The support of a vector is the set of the indices of its non-null compo-
nents. Consider any net N = (P, T, W ) with its incidence matrix C. A T-vector
is an element of NT ; it is called prime if the greatest common divisor of its com-
77
ponents is one (i.e. its components do not have a common non-unit factor). A
T-semiflow ν of the net is a non-null T-vector such that C · ν = 0. A T-semiflow
is called minimal when it is prime and its support is not a proper superset of
the support of any other T-semiflow [21].
The Parikh vector P(σ) of a finite sequence σ of transitions is a T-vector count-
ing the number of occurrences of each transition in σ, and the support of σ is the
support of its Parikh vector, i.e. supp(σ) = supp(P(σ)) = {t ∈ T | P(σ)(t) > 0}.
Strong connectedness and cycles in LTS. The LTS is said reversible if,
∀s ∈ [ιi, we have ι ∈ [si, i.e., it is always possible to go back to the initial state;
reversibility implies the strong connectedness of the LTS.
A sequence s[σis0 is called a cycle, or more precisely a cycle at (or around)
state s, if s = s0 . A non-empty cycle s[σis is called small if there is no non-
empty cycle s0 [σ 0 is0 in TS with P(σ 0 ) P(σ) (the definition of Parikh vectors
extending readily to sequences over the set of labels T of the LTS).
A circular LTS is a finite, strongly connected LTS that contains a unique cycle;
hence, it has the shape of an oriented circle. The circular LTS induced by a word
w = w1 . . . wk is the LTS with initial state s0 defined as s0 [w1 is1 [w2 is2 . . . [wk is0 .
All notions defined for labelled transition systems apply to Petri nets through
their reachability graphs.
Petri net subclasses. A net N is plain if no arc weight exceeds 1; pure if
∀p ∈ P : (p• ∩• p) = ∅, where p• = {t ∈ T | W (p, t)>0} and • p = {t ∈ T |
W (t, p)>0}; CF (choice-free [7, 21]) or ON (place-output-nonbranching [3]) if
∀p ∈ P : |p• | ≤ 1; a WMG (weighted marked graph [20]) if |p• | ≤ 1 and |• p| ≤ 1
for all places p ∈ P . The latter form a subclass of the choice-free nets; other
subclasses are marked graphs [6], which are plain with |p• | = 1 and |• p| = 1 for
each place p ∈ P , and T-systems [9], which are plain with |p• | ≤ 1 and |• p| ≤ 1
for each place p ∈ P .
Isomorphism and solvability. Two LTS TS 1 = (S1 , →1 , T, s01 ) and TS 2 =
(S2 , →2 , T, s02 ) are isomorphic if there is a bijection ζ : S1 → S2 with ζ(s01 ) =
s02 and (s, t, s0 ) ∈→1 ⇔ (ζ(s), t, ζ(s0 )) ∈→2 , for all s, s0 ∈ S1 .
If an LTS TS is isomorphic to RG(S) where S is a system, we say that S solves
TS . Solving a word w = `1 . . . `k amounts to solve the acyclic LTS defined by the
single path ι[`1 is1 . . . [`k isk . A finite word w is cyclically solvable if the circular
LTS induced by w is solvable. A LTS is WMG-solvable if a WMG solves it.
Other classical notions. An LTS TS = (S, →, T, ι) is fully reachable if S = [ιi.
It is forward deterministic if s[tis0 ∧s[tis00 ⇒ s0 = s00 , and backward deterministic
if s0 [tis ∧ s00 [tis ⇒ s0 = s00 .
A system S is forward persistent if, for any reachable markings M, M1 , M2 ,
(M [aiM1 ∧ M [biM2 ∧ a 6= b) ⇒ M1 [biM 0 ∧ M2 [aiM 0 for a reachable mark-
ing M 0 ; it is backward persistent if, for any reachable markings M, M1 , M2 ,
78
(M1 [aiM ∧M2 [biM ∧a 6= b) ⇒ M 0 [biM1 ∧M 0 [aiM2 for a reachable marking M 0 .
Next, we recall classical properties of Petri net reachability graphs.
Proposition 1 (Classical Petri net properties). If S is a Petri net system:
− RG(S) is a fully reachable LTS.
− RG(S) is forward deterministic and backward deterministic.
For the subclass of WMGs, we have the following dedicated properties, extracted
from Proposition 4, Lemma 1, Theorem 2 and Lemma 2 in [12].
Proposition 2 (Properties of WMG). If S = (N, M0 ) is a WMG system:
− It is forward persistent and backward persistent.
− If N is connected and has a T-semiflow ν, then there is a unique minimal one
π, with support T , and ν = k · π for some positive integer k. Moreover, if there
is a non-empty cycle in RG(S), there is one with Parikh vector π in RG(S)
around each reachable marking and RG(S) is reversible. If there is no cycle, all
the paths starting from some state s and reaching some state s0 have the same
Parikh vector.
To simplify our reasoning in the sequel, we introduce the following notation,
which captures some of the behavioral properties satisfied by WMG (Proposi-
tions 1 and 2). We denote by
• b the set of properties: forward and backward deterministic, forward and
backward persistent, totally reachable;
• c the property: there is a small cycle whose Parikh vector is prime with
support T .
A synthesis procedure does not necessarily lead to a connected solution. However,
the technique of decomposition into prime factors described in [10, 11] can always
be applied first, so as to handle connected partial solutions and recombine them
afterwards. Hence, in the following, we focus on connected WMG, without loss
of generality. In the next section, we consider the synthesis problem of WMG
with exactly two different labels.
3 Cyclic binary WMG Synthesis
In this section, we provide conditions for the WMG-solvability of 2-letters cyclic
LTS. In Subsection 3.1, we investigate the WMG-solvability of a finite cyclic LTS,
first when it is circular, then when it contains at least one cycle, which is the
more general cyclic case. In Subsection 3.2, we investigate the WMG-solvability
of an infinite cyclic binary LTS.
79
3.1 WMG-solvable finite cyclic binary systems
In this subsection, we first consider any circular LTS with only two different
labels. Each such LTS is defined by a word w ∈ {a, b}∗ , corresponding to the
labels encountered by firing the circuit once from ι, leading back to ι. Changing
the initial state in this LTS amounts to rotate w. Clearly, each such LTS satisfies
property b, but is not always WMG (or even Petri net) solvable.
The next results consider circuit Petri nets as represented in Figure 1, where
places are named following the direction of the arcs, e.g. pa,b is the output place
of a and the input place of b.
i
m n
pa,b
a b
pb,a
m n
j
Fig. 1. A generic WMG solving a finite circular LTS induced by a word w over the
alphabet {a, b}, whose initial marking (i, j) depends on the given solvable LTS. We
assume that P(w) = (n, m) is prime.
Theorem 1 (Cyclically solvable binary words). Consider a finite binary
word w over5 the alphabet {a, b}, with (n, m) = P(w) and n ≤ m (the case
m ≤ n is handled symmetrically). Then, w is cyclically solvable if and only if
gcd(n, m) = 1 and w is a rotation of the word w0 = abm0 . . . abmn−1 , where the
sequence m0 , . . . , mn−1 is the sequence of quotients in the following system of
equalities, with r0 = 0:
r0 + m = m0 .n + r1 , where 0 ≤ r1 < n
r1 + m = m1 .n + r2 , where 0 ≤ r2 < n
...
rn−1 + m = mn−1 .n.
Moreover, let N = (P, T, W ) be a circuit net as in Figure 1 with P = {pa,b , pb,a },
T = {a, b}, W (pb,a , a) = W (a, pa,b ) = m, and W (pa,b , b) = W (b, pb,a ) = n.
Then, the system S = (N, M0 ) with M0 (pa,b ) = 0 and M0 (pb,a ) = m + n − 1,
solves w cyclically.
Proof. From Proposition 2, for a connected WMG solution to exist, the Parikh
vector of the word must be the minimal T-semiflow µ = (n, m) with support
T = {a, b}, which is prime by definition, thus gcd(m, n) = 1.
5
We consider only words that contain each letter of the alphabet.
80
A variant of this problem has been studied in [4] (section 6). Basing on this
study, we derive the following. If a solution exists, then:
- there is a WMG solution as in Figure 1, implying that the sum Ms (pa,b ) +
Ms (pb,a ), where Ms (p) denotes the marking of place p when reaching state s, is
the same for all states (since each firing preserves the number of tokens);
- all the markings reached in pa,b before reaching the initial state again are dif-
ferent, and similarly for pb,a , since otherwise, two identical markings are reached
at two different states, implying unsolvability (more precisely, the “separation
property”, which is necessary for synthesis, is not satisfied);
- w.l.o.g., there is a state s where Ms (pa,b ) = 0, and similarly for pb,a (otherwise,
since the solution is pure, useless tokens can be removed);
- Ms (pa,b )+Ms (pb,a ) = m+n−1. Indeed, with more tokens, a reachable marking
enables both a and b, which is not allowed by the given LTS; with fewer tokens,
a deadlock is reached, i.e. a marking in which no transition is enabled;
- for each i, mi ∈ {bm/nc, dm/ne}, there are (m mod n) b-blocks of size (bm/nc+
1), the other ones have size bm/nc.
Let us start from the state s such that Ms (pa,b ) = 0 and Ms (pb,a ) = m + n − 1,
with r0 = 0. We denote by ri the number of tokens in pa,b at the i + 1-th visited
state that enables a. The value m0 is the maximal number of b’s that can be fired
after the first a, and then r1 tokens remain in pa,b ; hence, there are m+n−1−r1
tokens in pb,a (which is at least m) before the second a. After the second a, we
have m + r1 tokens in pa,b and we fire m1 b’s. We iterate the process until the
initial state is reached.
In the state enabling the (i + 1)-th a, there are (i · m) mod n tokens in pa,b ,
implying that rn is again 0 when the initial state is reached. In between, we
visited all the values from 0 to n−1 for the ri ’s: indeed, if (i·m) mod n = (j ·m)
mod n for 0 ≤ i < j < n, we have ((j − i) · m) mod n = 0, or ((j − i) · m = k · n
for some k; but then n must divide j − i since m and n are relatively prime,
which is only possible if i = j.
Finally, an adequate rotation of w0 leads to w and to the corresponding value of
r0 . t
u
An example is given in Figure 2, where the elements of the sequence m0 , . . . , mn−1
are put in bold in the system on the left.
Complexity. The number of operations to determine the sequence of mi ’s is
linear in the smallest weight n, i.e. also in the minimal number of occurrences of
a letter. In comparison, the previous algorithm of [4] checks a quadratic number
of subwords.
In Theorem 1, we provided a criterion for the cyclic solvability of a given word.
In the next theorem, we abstract the word by a Parikh vector, which provides
less accurate information on the behavior of the process. This result investigates
the possible WMG-solvable LTS for this vector.
81
0 + 21 = 2.8 + 5 21 8
5 + 21 = 3.8 + 2 p2
2 + 21 = 2.8 + 7
7 + 21 = 3.8 + 4 a b
4 + 21 = 3.8 + 1 p1
1 + 21 = 2.8 + 6 21 28 8
6 + 21 = 3.8 + 3
3 + 21 = 3.8 + 0.
Fig. 2. This system solves the word w = ab2 ab3 ab2 ab3 ab3 ab2 ab3 ab3 cyclically.
Theorem 2 (WMG-solvable cyclic binary systems). Let us consider µ =
(n, m) ≥ 1 such that gcd(n, m) = 1. Up to isomorphism and the choice of
the initial state, there is a single finite WMG-solvable LTS (S, →, {a, b}, ι) that
satisfies b, c and |S| ≥ n+m and that contains a small cycle whose Parikh vector
is µ. No such WMG-solvable LTS exists when |S| < n + m. If S = {0, 1, . . . , k},
we have (up to isomorphism) →= {(i, a, i+m)|i, i+m ∈ S}∪{(i, b, i−n)|i, i−n ∈
S}.
Proof. If there is a solution, it has the form illustrated in Figure 1. From the
weights, it is clear that i + j is invariant during the evolutions. Moreover, if the
system is cyclic, by dropping the useless tokens and choosing adequately the
initial state, we may assume i = 0 and j = M0 . From the previous results of
this section, we know that, if M0 = n + m − 1, this generates a circular RG with
n + m states (all the values for i between 0 and n + m − 1 are reached in some
order); moreover, if we identify the states to i, i.e., the marking of pa,b , the arcs
are {(i, a, i + m)|0 ≤ i, i + m < n + m ∈ S} ∪ {(i, b, i − n)|0 ≤ i, i − n < n + m}.
As a consequence, if |S| < n + m, there aren’t enough states to close the circuit,
and there is no solution. If on the contrary we have M0 > n + m − 1, we have in
particular the cycle mentioned above, and since we reach in particular state 1,
from there we may generate the same cycle (shifted), reaching state n + m and
state 2. We then iterate the process until we reach all the markings not greater
than M0 in pa,b . Hence the claim. t
u
3.2 WMG-solvability of infinite cyclic binary LTS
Let us now consider an infinite LTS satisfying b and c with only two different
labels. From the discussion in the previous section, it cannot correspond to a
net of the kind illustrated in Figure 1 since i + j remains constant, hence yields
finitely many states. On the other hand, a net of the kind illustrated in Fig-
ure 3 (or the variant obtained by switching the roles of a and b) yields infinitely
many occurrences of transition a, leading to infinitely many different reachable
markings. Besides, from any state, there may only be finitely many consecutive
b’s. Moreover, this is the only way to obtain infinitely many cycles with Parikh
vector (n, m).
82
m n
a i b
pa,b
Fig. 3. A WMG solution for the infinite cyclic case.
If n = 1, i is the maximum number of consecutive executions of b from ι; we can
then verify if the given LTS corresponds to the constructed net. Otherwise, let k
and l be the Bezout coefficients corresponding to the relatively prime numbers
m and n, so that k · m + l · n = 1. If l ≥ 0 ≥ k, i is the maximum number of
times we may execute a−k bl consecutively from ι, and we can check again if the
given LTS corresponds to the constructed net (this is a direct generalization of
the case n = 1). Otherwise, since −n · m + m · n = 0, by adding this relation
enough times to the previous one, we get k 0 · m + l0 · n = 1 with l0 ≥ 0 ≥ k 0 , and
we apply the same idea.
4 Finite words being cyclically solvable with a WMG
In this section, we provide several conditions of WMG-solvability for LTS formed
of a single circuit, based on the WMG-solvability of specific binary subwords.
We consider first the case of an arbitrary number of letters, providing a general
sufficient condition of solvability by decomposition. Then, we develop a charac-
terization of WMG-solvability for a subclass of the cyclic 3-letter words. Finally,
a counter-example to this characterization is obtained for 5 letters.
4.1 Sufficient condition for the solvability of cyclic words
The next theorem provides a sufficient condition for cyclic solvability of k-ary
words, for any positive integer k. This condition uses binary subwords obtained
by projection6 and containing occurrences of two different labels that are con-
tiguous in the k-ary word. The other binary subwords are not needed since they
lack this contiguity and do not capture the direct causality.
Theorem 3. Consider any word w over7 any finite alphabet T such that P(w) is
prime. Suppose the following: ∀u = w t1 t2 (i.e., the projection of w on {t1 , t2 })
for some t1 , t2 such that t1 6= t2 ∈ T , and w = (w1 t1 t2 w2 ) or w = (t2 w3 t1 ),
u = v ` for some positive integer `, P(v) is prime, and v is cyclically solvable by
a circuit. Then, w is cyclically solvable with a WMG.
6
The projection of a word w ∈ A∗ on a set A0 ⊆ A of letters is the maximum subword
of w whose letters belong to A0 , noted w A0 . For example, the projection of the word
w = `1 `2 `3 `2 on the set {`1 , `2 } is the word `1 `2 `2 .
7
We consider only words that contain each letter of the alphabet.
83
Proof. Consider, for every such pair (ti , tj ), ti 6= tj , a circuit solution Ci,j of v
for the subword v l = ui,j = w ti tj , obtained as in the construction of Theorem
1. Assuming all these nets are place-disjoint, consider the transition-merging8
of all these marked circuits C = {C1 , . . . Cq }, Ci = ((Pi , Ti , Wi ), Mi ) for i =
1 . . . q, through a WMG S 0 , i.e. S 0 = (N 0 , M00 ) such that N 0 = (P 0 , T, W 0 ) with
P 0 = ]i=1...q Pi , T = ∪i=1...q Ti , W 0 = ∪i=1...q Wi , and M00 is the concatenation
M1 . . . Mq .
Let w be of the form aw0 . We prove that a is the only transition enabled in S 0 .
All the subwords of the form w a,t necessarily start with a. All the input places
of the transition a belong to the binary circuits defined by these subwords. Since
these subwords are solvable by marked circuits which we merged together, all
the input places of a are initially enabled. Now, let us suppose that another
transition d is also initially enabled in S 0 . Since d is not the first letter of w,
another letter q appears in w just before the first occurrence of d. In the solution
of w d,q , d is not initially enabled since q must occur before; hence it is not
enabled in the merging either. We deduce that a is the only transition that is
enabled in S 0 .
Now, the same arguments apply to w00 = w0 a whose relevant subwords are
solvable by the circuits in the same way, and we deduce that the WMG S 0 has
the language P REF (w∗ ).
Note that we did not use explicitely above the special form of u. Simply, the
latter is necessary to build a circuit system Ci,j with the language P REF (u∗ ) =
P REF (v ∗ ). Ci,j is a circular solution for v, but not for u unless ` = 1. The
fact that the merging S 0 of all the Ci,j ’s yields not only a system with the
adequate language P REF (w∗ ) but a circular solution of w arises from the fact
that P(w) is prime (by Proposition 2). We thus deduce that the WMG S 0 solves
w cyclically. t
u
4.2 WMG-solvability for a subclass of ternary cyclic words
Next, we prove the other direction of Theorem 3, leading to a characterization
of WMG-solvability for a special subclass of the ternary cyclic words.
The proof exploits a WMG with 3 transitions and 6 places, connecting 2 places
to each pair of transitions, as illustrated in Figure 4. In some cases, a smaller
number of places can solve the same LTS, but we do not aim here at minimizing
the number of nodes in a solution.
Theorem 4 (Cyclic solvability of ternary words). Consider a ternary word
w over9 the alphabet T with Parikh vector (x, x, y) such that gcd(x, y) = 1.
Then, w is cyclically solvable with a WMG if and only if ∀u = w t1 t2 such that
8
Also called sometimes the synchronization on transitions.
9
We consider only words that contain each letter of the alphabet.
84
a
y
y
pa,b ? ? pc,a
? pb,a pa,c ?
x
pc,b x
y x
b ? c
y x
?
pb,c
Fig. 4. A WMG with three transitions (letters), with minimal T-semiflow (x, x, y) and
gcd(x, y) = 1.
t1 6= t2 ∈ T , and w = (w1 t1 t2 w2 ) or w = (t2 w3 t1 ), u = v ` for some positive
integer `, P(v) is prime, and v is cyclically solvable by a circuit 10 .
Proof. The right-to-left direction of the equivalence, assuming the properties on
the projections, is true by Theorem 3, for the particular case that |T | = 3. We
thus deduce the cyclic solvability.
In the rest of this proof, we consider the other direction, assuming circular solv-
ability. If x = y = 1, the claim is trivially obtained. Let us assume that x 6= y.
Let us write T = {a, b, c}. The general form of a solution has 3 transitions
and 6 places (one for each ordered pair of transitions). Additional places are
never necessary in the presence of a T-semiflow. Indeed, let pu,v be a place
between transitions u and v, Wu the weight on the arc to this place and Wv
the one from this place. Due to the presence of the T-semiflow P(w), we have
P(w)(u) · Wu = P(w)(v) · Wv , and we may choose Wu = P(w)(v) as well as
Wv = P(w)(u). We may also divide the weights around each place by their gcd.
In our case, this leads to the configuration illustrated by Figure 4. We denote
by RG the reachability graph of a solution based on this net.
We show first that the projection w ab of w on {a, b} is of the form (ab)k or (ba)k
for some positive integer k.
There is no pattern aab in w2 (which allows to consider sequences on the border
of two consecutive w’s) because, if M1 [aiM2 [aiM3 [bi, M1 (pc,b ) = M2 (pc,b ) =
M3 (pc,b ) ≥ y and M2 (pa,b ) ≥ 1, which would also allow to perform b after the
first a and RG is not circular.
10
also called circular Petri net.
85
If there is a pattern aac and M1 [aiM2 [aiM3 [ciM4 , M2 (pa,c ) ≥ y and M1 (pb,c ) =
M2 (pb,c ) = M3 (pb,c ) ≥ x, hence y < x otherwise M2 already enables c and RG
is not circular. Then M4 (pa,b ) ≥ 2, M4 (pc,b ) ≥ x > y and M4 (pc,a ) ≥ x > y, so
that M4 [bi; hence M4 (pb,a ) = 0 since otherwise we also have M4 [ai and RG is
not circular. We thus have M4 [baiM5 for some marking M5 , with M5 (pb,a ) = 0,
so that M5 does not enable a; M5 does not enable b either since otherwise we
could also do M4 [bbi and again RG is not circular. Thus, we have M4 [baci, and
then we are in a situation similar to the one after the first c. As a consequence,
we must have a sequence M1 [aa(cba)ω i, and RG is not circular.
Hence, in w2 we cannot have a sequence aa, nor bb by symmetry.
Let us now assume that a pattern ack a exists in w2 for some k ≥ 1. Since the
first firing of a puts a token in pa,b and the next firing of c does not enable b,
we must have x < y. Let us assume in the circular RG that M1 [ack aiM2 [σiM1 .
σ is not empty since it must contain x times b. It cannot end with an a, since
otherwise we have a sequence aa, which we already excluded. It cannot end
with a b either, since M1 (pb,a ) ≥ 2 (in order to fire a twice without a b in
between), so that if M3 [biM1 [ai, M3 (pb,a ) ≥ 1, we must also have M3 [ai, and
RG is not circular. Hence, σ ends with a c and for some markings M20 , M3 we
have M3 [ciM1 [ack iM20 [aiM2 .
We deduce that M20 (pa,b ) ≥ 1, M20 (pc,b ) ≥ (k + 1) · x; hence (k + 1) · x < y
otherwise M20 also enables b and RG is not circular. Also, M3 (pb,a ) ≥ 2 and
M3 (pc,a ) ≥ 2 · y − (k + 1) · x > y, so that M3 also enables a and again RG
is not circular. As a consequence, we cannot have a pattern ack a, nor bck b by
symmetry, and w ab = (ab)k or w ab = (ba)k for the positive integer k = x. With
v = ab or v = ba, we have the adequate solvability property for w ab , and we
can assume in the following that the sum of the tokens present in places pa,b and
pb,a is 1 for all reachable markings.
Let us now suppose that we have a WMG S solving w cyclically, whose under-
lying net is pictured in Figure 4. From the previous results, we can assume that
M0 (pa,b ) + M0 (pb,a ) = 1 in S, this equality being preserved by all reachable
markings. To show that u = w ac has the adequate form (the case for w bc is
symmetrical), let us consider the circuit Cac , restriction of S to pa,c , c, pc,a , a.
Let us assume in the following that u cannot be written under the form u = v `
for some positive integer `, where P(v) is prime and cyclically solvable. Since
gcd(x, y) = gcd(P(w)(a), P(w)(c)) = gcd(P(u)(a), P(u)(c)) = 1, P(u) is prime
and u = v with ` = 1, hence u is not cyclically solvable. For the net N consid-
ered, this implies the existence of some prefix σac of u such that, for every initial
marking of Cac that enables the sequence u in this circuit, the marking reached
by firing σac necessarily enables both places pa,c and pc,a . Indeed, Theorem 1
specifies the finite set of all possible minimal markings that allow cyclic solv-
ability, and each such marking enables exactly one place of the circuit. Every
other non-circular reachability graph is defined by some larger initial marking
and contains a marking that enables both places.
Thus, for any initial marking M0 that makes the system S = (N, M0 ) solve w
86
cyclically, the smallest prefix of w whose projection on {a, c} equals σac leads to
a marking M in the WMG that enables pa,c and pc,a .
Hereafter, we consider all the cases in which either a or c is enabled from M .
In each case, we describe the shape of the LTS and deduce from it a reachable
marking that enables two transitions, hence a contradiction.
Case x > y: In this case, in S, we cannot have two consecutive c’s.
− Subcase in which M enables the place pa,c as well as the transition a in the
WMG, hence its input places pb,a and pc,a . Since M [ai, transition c is not enabled
at M , implying that pb,c is not enabled by M . We deduce: M (pa,c ) > M (pb,c ).
Since pa,c is enabled by M , the last occurrence of a transition before the next
firing of c is necessarily b, implying: M [(ab)k ciM1 for some integer k ≥ 1 and
some marking M1 . The inequality mentioned above is still valid at M1 , i.e.
M1 (pa,c ) > M1 (pb,c ), and we iterate the same arguments from M1 to deduce
that
P the rotation wM of w starting at M is of the form (ab) c . . . (ab) c with
k1 ky
i=1..y ki = x and each ki is positive.
− Subcase in which M enables the place pc,a as well as the transition c in the
WMG, hence its input places pa,c and pb,c . Thus, the firing of c from M cannot
enable a, implying that M (pc,b ) < M (pc,a ) and that M [c(ba)k ciM1 for some
positive integer k and a marking M1 . The inequality is still valid at M1 , i.e.
M1 (pc,b ) < M1 (pc,a ), from which we deduce Pthat the rotation wM of w starting
at M is of the form c(ba)k1 . . . c(ba)ky with i=1..y ki = x and each ki is positive.
Case x ≤ y:
− Subcase in which M enables the place pa,c as well as the transition a in
the WMG, hence its input places pc,a and pb,a . Thus, the firing of a from M
cannot enable c, implying that M (pb,c ) < M (pa,c ) and that M [abck iM1 for some
positive integer k and a marking M1 , at which the same inequality is still valid.
We deduce
P that the rotation wM of w starting at M is of the form abck1 . . . abckx
with i=1..x ki = y and each ki is positive.
− Subcase in which M enables the place pc,a as well as the transition c in the
WMG, hence its input places pa,c and pb,c . Thus, firing one or several c’s from M
does not enable a, and M (pc,b ) < M (pc,a ), implying that M [ck baiM1 for some
positive integer k and a marking M1 , at which the same inequality is still valid.
We deduce
P that the rotation wM of w starting at M is of the form ck1 ba . . . ckx ba
with i=1..x ki = y and each ki is positive.
In each of the four cases developed above, we observe that each sequence of ab
or ba could be seen as an atomic firing, and wM b,c is obtained from wM a,c by
renaming each a into one b. This implies that the deletion of the initial useless
tokens (also known as frozen tokens, i.e. never used by any firing) yields a system
in which some reachable marking distributes the tokens in the same way in the
places between c and a as in the places between c and b. This is for example the
case of the marking M if it does not contain useless tokens.
We deduce that M (with or without useless tokens) enables all four places pa,c ,
pc,a , pb,c and pc,b , thus enabling two transitions of the WMG at least. This
87
contradicts the cyclic solvability of w, implying that v = u is cyclically solvable
by a circuit. Hence the claim. t
u
4.3 A counter-example for 5 letters
In Theorem 4, we provided a characterization of cyclic WMG-solvability for
ternary words w such that P(w) is prime and has only two values. However, this
results does not apply to words w over 5 letters such that P(w) is prime and has
only two values, as pictured in Figure 5. This WMG cyclically solves the word
w = aacbbeabd with P(w) = (3, 3, 1, 1, 1), which is prime, while its projection
u = aabbab on {a, b} leads to v = u, and P(v) = (3, 3) is not prime, hence is not
cyclically solvable by a WMG.
a
3 3 c
a
3 3
3 3 b
c d e a
3 3 b
3 3
3 3 d
e
b
b a
Fig. 5. aacbbeabd is cyclically WMG-solvable.
5 Conclusions and Perspectives
In this work, we generalized previous methods dedicated to the analysis and syn-
thesis of weighted marked graphs, a well-known and useful subclass of weighted
Petri nets allowing to model various real-world applications.
By restricting the size of the alphabet to 2 letters, we provided a characterization
of the WMG-solvable labelled transition systems formed of a single circuit. We
also extended this investigation to infinite LTS.
88
For the case of an LTS formed of a single circuit with an arbitrary number of
letters, we proposed a sufficient condition of WMG-solvability.
Then, for the case of an LTS formed of a single circuit with 3 letters, we obtained
a characterization of WMG-solvability for a subset of the possible Parikh vectors.
Finally, we proved that this condition for 3 letters does not extend to circular
LTS using a 5-letter alphabet.
A general perspective is to characterize all the WMG-solvable LTS, which are
not necessarily formed of a single circuit. To this end, developing new conditions
based on decompositions into subwords, by weakening the results presented in
this paper, would be worth investigating.
Acknowledgements
We would like to thank the anonymous referees for their useful suggestions.
References
1. Barylska, K., Best, E., Erofeev, E., Mikulski, L., Piatkowski, M.: On binary words
being Petri net solvable. In: Proceedings of the International Workshop on Algo-
rithms & Theories for the Analysis of Event Data, ATAED 2015, Brussels, Belgium.
pp. 1–15 (2015), http://ceur-ws.org/Vol-1371/paper01.pdf
2. Barylska, K., Best, E., Erofeev, E., Mikulski, L., Piatkowski, M.: Conditions for
Petri net solvable binary words. T. Petri Nets and Other Models of Concurrency
11, 137–159 (2016)
3. Best, E., Devillers, R.: Synthesis and reengineering of persistent systems. Acta Inf.
52(1), 35–60 (2015), http://dx.doi.org/10.1007/s00236-014-0209-7
4. Best, E., Erofeev, E., Schlachter, U., Wimmel, H.: Characterising petri net solvable
binary words. In: Kordon, F., Moldt, D. (eds.) Application and Theory of Petri
Nets and Concurrency. pp. 39–58. Springer International Publishing, Cham (2016)
5. Best, E., Hujsa, T., Wimmel, H.: Sufficient conditions for the marked graph re-
alisability of labelled transition systems. Theoretical Computer Science (2017),
http://www.sciencedirect.com/science/article/pii/S0304397517307181
6. Commoner, F., Holt, A., Even, S., Pnueli, A.: Marked directed graphs. J. Comput.
Syst. Sci 5(5), 511–523 (1971), https://doi.org/10.1016/S0022-0000(71)80013-2
7. Crespi-Reghizzi, S., Mandrioli, D.: A decidability theorem for a class
of vector-addition systems. Inf. Process. Lett. 3(3), 78–80 (1975),
http://dx.doi.org/10.1016/0020-0190(75)90020-4
8. Delosme, J.M., Hujsa, T., Munier-Kordon, A.: Polynomial sufficient conditions of
well-behavedness for weighted join-free and choice-free systems. In: 13th Interna-
tional Conference on Application of Concurrency to System Design. pp. 90–99
(July 2013)
9. Desel, J., Esparza, J.: Free Choice Petri Nets, Cambridge Tracts in Theoretical
Computer Science, vol. 40. Cambridge University Press, New York, USA (1995)
89
10. Devillers, R.: Products of Transition Systems and Additions of Petri Nets. In:
Proc. 16th International Conference on Application of Concurrency to Sys-
tem Design (ACSD 2016) J. Desel and A. Yakovlev (eds). pp. 65–73 (2016),
https://doi.org/10.1109/ACSD.2016.10
11. Devillers, R.: Factorisation of transition systems. Acta Informatica (2017),
https://doi.org/10.1007/s00236-017-0300-y
12. Devillers, R., Hujsa, T.: Analysis and synthesis of weighted marked graph Petri
nets. In: Khomenko, V., Roux, O.H. (eds.) Application and Theory of Petri Nets
and Concurrency: 39th International Conference, PETRI NETS 2018, Bratislava,
Slovakia, 2018, Proceedings. pp. 1–21. Springer International Publishing (2018)
13. Erofeev, E., Barylska, K., Mikulski, L., Piatkowski, M.: Generating all min-
imal Petri net unsolvable binary words. In: Proceedings of the Prague
Stringology Conference 2016, Prague, Czech Republic. pp. 33–46 (2016),
http://www.stringology.org/event/2016/p04.html
14. Erofeev, E., Wimmel, H.: Reachability graphs of two-transition Petri nets. In: Pro-
ceedings of the International Workshop on Algorithms & Theories for the Analysis
of Event Data 2017, Zaragoza, Spain. pp. 39–54 (2017), http://ceur-ws.org/Vol-
1847/paper03.pdf
15. Hujsa, T.: Contribution to the study of weighted Petri nets. Ph.D. thesis, Pierre and
Marie Curie University, Paris, France (2014), https://tel.archives-ouvertes.fr/tel-
01127406
16. Hujsa, T., Delosme, J.M., Munier-Kordon, A.: On the reversibility of well-behaved
weighted choice-free systems. In: Ciardo, G., Kindler, E. (eds.) Application and
Theory of Petri Nets and Concurrency. pp. 334–353. Springer International Pub-
lishing, Cham (2014)
17. Hujsa, T., Delosme, J.M., Munier-Kordon, A.: Polynomial sufficient condi-
tions of well-behavedness and home markings in subclasses of weighted Petri
nets. ACM Trans. Embed. Comput. Syst. 13(4s), 141:1–141:25 (Jul 2014),
http://doi.acm.org/10.1145/2627349
18. Hujsa, T., Devillers, R.: On liveness and deadlockability in subclasses of weighted
Petri nets. In: van der Aalst, W., Best, E. (eds.) Application and Theory of
Petri Nets and Concurrency: 38th International Conference, PETRI NETS 2017,
Zaragoza, Spain, June 25–30, 2017, Proceedings. pp. 267–287. Springer Interna-
tional Publishing, Cham (2017), https://doi.org/10.1007/978-3-319-57861-3_16
19. Murata, T.: Petri nets: properties, analysis and applications. Proceedings of the
IEEE 77(4), 541–580 (April 1989)
20. Teruel, E., Chrzastowski-Wachtel, P., Colom, J.M., Silva, M.: On weighted T-
systems. In: Jensen, K. (ed.) 13th International Conference on Application and
Theory of Petri Nets and Concurrency (ICATPN), LNCS. vol. 616, pp. 348–367.
Springer, Berlin, Heidelberg (1992), https://doi.org//10.1007/3-540-55676-1_20
21. Teruel, E., Colom, J.M., Silva, M.: Choice-Free Petri Nets: a Model for De-
terministic Concurrent Systems with Bulk Services and Arrivals. IEEE Trans-
actions on Systems, Man, and Cybernetics, Part A 27(1), 73–83 (1997),
http://dx.doi.org/10.1109/3468.553226
22. Teruel, E., Silva, M.: Structure theory of Equal Conflict systems. Theoreti-
cal Computer Science 153(1&2), 271–300 (1996), https://doi.org/10.1016/0304-
3975(95)00124-7
90