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 arbitrary 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.
Petri nets form a highly expressive and intuitive operational model of discrete event systems, capturing the mechanisms of synchronization, conflict and concurrency. 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 synthesis 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 labelled 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
encompassed plain nets (each weight equals 1; also called ordinary nets) [
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 cycle4. 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
elementary 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
unsolvability for the entire LTS, as highlighted in other works [
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 solvable 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 condition 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. 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
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. Generalizing 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 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 [M0i, the set of labels T , initial state M0 and transitions {(M, t, M 0) | M, M 0 ∈ [M0i ∧ 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
components. 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
components 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 [
The Parikh vector P(σ) of a finite sequence σ of transitions is a T-vector counting 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}.
∀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 nonempty cycle s0[σ0is0 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[w1is1[w2is2 . . . [wkis0. 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 [
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 ι[`1is1 . . . [`kisk. 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 marking M 0; it is backward persistent if, for any reachable markings M, M1, M2, 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 [
To simplify our reasoning in the sequel, we introduce the following notation, which captures some of the behavioral properties satisfied by WMG (Propositions 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 [
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. 3.1
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.
a m m
i pa,b pb,a j n n b
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.
A variant of this problem has been studied in [
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. tu 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 [
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. a 21 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. tu 3.2
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 Figure 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). pa,b n
b
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−kbl 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 k0 · m + l0 · n = 1 with l0 ≥ 0 ≥ k0, and we apply the same idea. 4
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 characterization 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
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 contiguous 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 t1t2 (i.e., the projection of w on {t1, t2}) for some t1, t2 such that t1 6= t2 ∈ T , and w = (w1t1t2w2) or w = (t2w3t1), 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. Proof. Consider, for every such pair (ti, tj ), ti 6= tj , a circuit solution Ci,j of v for the subword vl = ui,j = w titj , 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 S0, i.e. S0 = (N 0, M00 ) such that N 0 = (P 0, T, W 0) with P 0 = ]i=1...qPi, T = ∪i=1...qTi, W 0 = ∪i=1...qWi, and M00 is the concatenation M1 . . . Mq.
Let w be of the form aw0. We prove that a is the only transition enabled in S0. 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 S0. 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 S0.
Now, the same arguments apply to w00 = w0a whose relevant subwords are solvable by the circuits in the same way, and we deduce that the WMG S0 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 S0 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 S0 solves w cyclically. tu 4.2
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.
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 t1t2 such that 8 Also called sometimes the synchronization on transitions. 9 We consider only words that contain each letter of the alphabet. pb,c y pa,c ?
x x x ? pc,a c x 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 = (w1t1t2w2) or w = (t2w3t1), 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 solvability. 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. 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 acka 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[ackaiM2[σ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[ackiM20 [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 acka, nor bckb 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 underlying 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 considered, 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 solvability, 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 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)kciM1 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 the rotation wM of w starting at M is of the form (ab)k1 c . . . (ab)ky c with Pi=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)kciM1 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 that the rotation wM of w starting at M is of the form c(ba)k1 . . . c(ba)ky with Pi=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 [abckiM1 for some positive integer k and a marking M1, at which the same inequality is still valid. We deduce that the rotation wM of w starting at M is of the form abck1 . . . abckx with Pi=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 [ckbaiM1 for some positive integer k and a marking M1, at which the same inequality is still valid. We deduce that the rotation wM of w starting at M is of the form ck1 ba . . . ckx ba with Pi=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 contradicts the cyclic solvability of w, implying that v = u is cyclically solvable by a circuit. Hence the claim. 4.3
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. b e tu b c 3 3 3 3 3 3 a d b 3 3
In this work, we generalized previous methods dedicated to the analysis and synthesis 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.
3 3 3 3
e 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.
We would like to thank the anonymous referees for their useful suggestions.