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) [19], homogeneous nets (meaning that for each place p, all the output weights of p are Supported by DFG through grant Be 1267/16-1 ASYST 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 number 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 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 [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].
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 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. 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, M 0 ) where N is a net and M 0 is the initial marking, which is a mapping M 0 : P → N (hence a member of N P ) 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 [t , 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 defined by M (p) = M (p) − W (p, t) + W (t, p); we note M [t M . A marking M is reachable from M if there is a sequence of firings leading from M to M . The set of markings reachable from M is denoted by [M . The reachability graph of S is the labelled transition system RG(S) with the set of vertices [M 0 , the set of labels T , initial state M 0 and transitions
The language of a Petri net system S is the set L(S) = {σ ∈ T * | M 0 [σ }. These languages are prefix-closed, i.e., if σ = σ σ ∈ L(S), then σ ∈ 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 N T ; it is called prime if the greatest common divisor of its com-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 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}. [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 .
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 ι
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, M 0 ) 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 s 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 (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 [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.
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.
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. p a,b is the output place of a and the input place of b. 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 w = ab m0 . . . ab mn−1 , where the sequence m 0 , . . . , m n−1 is the sequence of quotients in the following system of equalities, with r 0 = 0:
Moreover, let N = (P, T, W ) be a circuit net as in Figure 1 with 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 M s (p a,b ) + M s (p b,a ), where M s (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 p a,b before reaching the initial state again are different, and similarly for p b,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 M s (p a,b ) = 0, and similarly for p b,a (otherwise, since the solution is pure, useless tokens can be removed); -M s (p a,b )+M s (p b,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. In the state enabling the (i + 1)-th a, there are (i • m) mod n tokens in p a,b , implying that r n is again 0 when the initial state is reached. In between, we visited all the values from 0 to n−1 for the r i '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 w leads to w and to the corresponding value of r 0 .
An example is given in Figure 2, where the elements of the sequence m 0 , . . . , m n−1 are put in bold in the system on the left.
Complexity. The number of operations to determine the sequence of m i '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. 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 = M 0 . From the previous results of this section, we know that, if M 0 = 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 p a,b , the arcs are
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 M 0 > 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 M 0 in p a,b . Hence the claim.
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). 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
is the maximum number of times we may execute a −k b l 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 • m + l • n = 1 with l ≥ 0 ≥ k , and we apply the same idea.
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.
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 projection 6 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 {t 1 , t 2 }) for some t 1 , t 2 such that t 1 = t 2 ∈ T , and w = (w 1 t 1 t 2 w 2 ) or w = (t 2 w 3 t 1 ), 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.
Proof. Consider, for every such pair (t i , t j ), t i = t j , a circuit solution C i,j of v for the subword v l = u i,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 = {C 1 , . . . C q }, C i = ((P i , T i , W i ), M i ) for i = 1 . . . q, through a WMG S , i.e. S = (N , M 0 ) such that N = (P , T, W ) with P = i=1...q P i , T = ∪ i=1...q T i , W = ∪ i=1...q W i , and M 0 is the concatenation M 1 . . . M q .
Let w be of the form aw . We prove that a is the only transition enabled in S .
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 . 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 . Now, the same arguments apply to w = w a whose relevant subwords are solvable by the circuits in the same way, and we deduce that the WMG S 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 C i,j with the language P REF (u * ) = P REF (v * ). C i,j is a circular solution for v, but not for u unless = 1. The fact that the merging S of all the C i,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 solves w cyclically.
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 t1t2 such that t 1 = t 2 ∈ T , and w = (w 1 t 1 t 2 w 2 ) or w = (t 2 w 3 t 1 ), 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 = 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 p u,v be a place between transitions u and v, W u the weight on the arc to this place and W v the one from this place. Due to the presence of the T-semiflow P(w), we have P(w)(u) • W u = P(w)(v) • W v , and we may choose W u = P(w)(v) as well as W v = 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 w 2 (which allows to consider sequences on the border of two consecutive w
We deduce that 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 M 0 (p a,b ) + M 0 (p b,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 C ac , restriction of S to p a,c , c, p c,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 C ac that enables the sequence u in this circuit, the marking reached by firing σ ac necessarily enables both places p a,c and p c,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 M 0 that makes the system S = (N, M 0 ) 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 p a,c and p c,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. − Subcase in which M enables the place p a,c as well as the transition a in the WMG, hence its input places p c,a and p b,a . Thus, the firing of a from M cannot enable c, implying that M (p b,c ) < M (p a,c ) and that M [abc k M 1 for some positive integer k and a marking M 1 , at which the same inequality is still valid. We deduce that the rotation w M of w starting at M is of the form abc k1 . . . abc kx with i=1..x k i = y and each k i is positive.
− Subcase in which M enables the place p c,a as well as the transition c in the WMG, hence its input places p a,c and p b,c . Thus, firing one or several c's from M does not enable a, and M (p c,b ) < M (p c,a ), implying that M [c k ba M 1 for some positive integer k and a marking M 1 , at which the same inequality is still valid. We deduce that the rotation w M of w starting at M is of the form c k1 ba . . . c kx ba with i=1..x k i = y and each k i 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 w M b,c is obtained from w M 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 p a,c , p c,a , p b,c and p c,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.
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.
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.
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.