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