Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach

Abstract

Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new conditions for the synthesis of 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.

Some of these new conditions do not restrict the number of labels; the other ones consider up to 3 labels. Additional constraints are investigated: when the LTS is either finite or infinite, and either cyclic or acyclic. We show that one of these conditions, developed for 3 labels, does not extend to 4 nor to 5 labels. Also, we tackle geometrically the WMG-solvability of finite, acyclic LTS with any number of labels.

E. Erofeev—Supported by DFG through grant Be 1267/16-1 ASYST.

T. Hujsa—Supported by the STAE foundation/project DAEDALUS, Toulouse, France.

1 Introduction

Petri nets form a highly expressive and intuitive operational model of discrete event systems, capturing the mechanisms of synchronisation, conflict and concurrency. Many of their fundamental behavioural properties are decidable, allowing to model and analyse 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 the analysis or synthesis of Petri nets, structural restrictions encompassed plain nets (each weight equals 1; also called ordinary nets) [1], homogeneous nets (meaning that for each place p, all the output weights of p are equal) [2, 3], free-choice nets (the net is homogeneous, and any two transitions sharing an input place have the same set of input places) [2, 4], choice-free nets (each place has at most one output transition) [5, 6], marked graphs (each place has at most one output transition and one input transition) [7,8,9,10], join-free nets (each transition has at most one input place) [2, 3, 11, 12], etc.

More recently, another kind of restriction has been considered, limiting the number of different transition labels of the LTS in combination with restrictions on the LTS structure: for the binary case, feasibility of net synthesis from finite linear LTS and LTS with cycles¹ has been characterised by rates of labels in the transition system [13, 14] and by pseudo-regular expressions [15], giving rise to fast specialised synthesis algorithms; moreover, a complete enumeration of the shapes of synthesisable transition systems is presented in [16].

In this paper, we combine the restriction on the number of labels with the weighted marked graph (WMG) constraint. In addition, we study constraints on the existence of cycles in the LTS: when the LTS is acyclic, i.e. it does not contain any cycle, and when it is cyclic, i.e. it contains at least one cycle. In the latter case, we also study the finite circular LTS, meaning strongly connected LTSs that contain a unique cycle: 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^\infty$.

An important purpose of studying such constrained LTSs 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 [13, 15, 17]. Moreover, cycles appear systematically in the reachability graph of live and/or reversible Petri nets [5, 18], which are used to model various real-world applications, such as embedded systems [19].

Contributions. In this work, we study further the links between simple LTS structures and the reachability graph of WMGs, as follows.

First, we provide a characterisation of the 2-label (i.e. binary) words being cyclically solvable by a WMG (i.e. WMG-solvable), and extend the analysis to finite cyclic LTSs. We also tackle the case of infinite cyclic LTSs with 2 labels.

Then, when the number of labels is arbitrary, we provide a geometric characterisation of the finite, acyclic, WMG-solvable LTS, as well as a general sufficient condition of WMG-solvability for a cyclic word, using a decomposition into specific cyclically WMG-solvable binary subwords. We prove that this sufficient condition becomes a characterisation of cyclic WMG-solvability for a subclass of the 3-label words. Furthermore, we show, with the help of two counter-examples, that this characterisation does not hold for words with four or five labels.

Comparing with [20], we refine the results and explanations on WMG-solvable, finite, cyclic, binary LTSs by introducing Lemma 1 and upgrading Theorem 2, in Subsect. 3.1. We also provide the new geometric characterisation of WMG-solvability for acyclic LTS with any number of labels, and we sharpen the counter-examples to the characterisation of cyclically solvable ternary words in the cases of four and five labels.

Organisation of the Paper. After recalling classical definitions, notations and properties in Sect. 2, we present the results of WMG-solvability for 2-label words in Sect. 3. Then, in Sect. 4, we propose the geometric characterisation of WMG-solvability for an acyclic LTS with any number of labels. In Sect. 5, we develop the general sufficient condition of circular WMG-solvability for any number of labels. In Sect. 6, we tackle the ternary case and exhibit counter-examples for 4 and 5 labels. Finally, Sect. 7 presents our conclusions and perspectives.

2 Classical Definitions, Notations and Properties

LTSs, Sequences and Reachability. A labelled transition system with initial state, abbreviated LTS, is a quadruple $TS =(S,\rightarrow ,T,\iota )$ where S is the set of states, T is the set of labels, $\rightarrow \,\subseteq (S\times T\times S)$ is the labelled transition relation, and $\iota \in S$ is the initial state.

A label t is enabled at $s\in S$, written $s[t\rangle$, if $\exists s'\in S:(s,t,s')\in \rightarrow$, in which case $s'$ is said to be reachable from s by the firing of t, and we write $s[t\rangle s'$. Generalising to any (firing) sequences $\sigma \in T^*$, $s[\varepsilon \rangle$ and $s[\varepsilon \rangle s$ are always true; and $s[\sigma t\rangle s'$, i.e. $\sigma t$ is enabled from state s and leads to $s'$, if there is some $s''$ with $s[\sigma \rangle s''$ and $s''[t\rangle s'$. A state $s'$ is reachable from state s if $\exists \sigma \in T^*:s[\sigma \rangle s'$. The set of states reachable from s is denoted by $[s\rangle$.

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\cap T=\emptyset$, and $W:((P\times T)\cup (T\times P))\rightarrow \mathbb {N}$ is a weight function giving the weight of each arc. A Petri net system, or system, is a tuple $\mathcal S=(N,M_0)$ where N is a net and $M_0$ is the initial marking, which is a mapping $M_0:P\rightarrow \mathbb {N}$ (hence a member of $\mathbb {N}^P$) indicating the initial number of tokens in each place. If $W(x,y)>0$, y is said to be an output of x, and x is said to be an input of y. The incidence matrix C of the net is the integer $P\times T$-matrix with components $C(p,t)=W(t,p)-W(p,t)$.

A transition $t\in T$ is enabled by a marking M, denoted by $M[t\rangle$, if for all places $p\in P$, $M(p)\ge W(p,t)$. A place $p \in P$ is enabled by a marking M if $M(p) \ge W(p,t)$ for every output transition t of p, meaning that it is not an obstacle to enabling transitions. 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\rangle M'$. A marking $M'$ is reachable from M if there is a sequence of firings leading from M to $M'$; if this sequence of firings defines a sequence of transitions $\sigma \in T^*$, we note $M[\sigma \rangle M'$. The set of markings reachable from M is denoted by $[M\rangle$. The reachability graph of $\mathcal S$ is the labelled transition system $RG (\mathcal S)$ with the set of vertices $[M_0\rangle$, the set of labels T, initial state $M_0$ and transitions $\{(M,t,M')\mid M,M'\in [M_0\rangle \wedge M[t\rangle M'\}$. A system $\mathcal S$ is bounded if $RG (\mathcal S)$ is finite.

The language of a Petri net system $\mathcal S$ is the set ${\mathcal L}(\mathcal S)=\{\sigma \in T^*\mid M_0[\sigma \rangle \}$. These languages are prefix-closed, i.e., if $\sigma =\sigma '\sigma ''\in {\mathcal L}(\mathcal S)$, then $\sigma '\in {\mathcal L}(\mathcal S)$. For any language $L\subseteq T^*$, we denote by ${ {PREF}}(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 $\mathbb {N}^{T}$; 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 $\nu$ of the net is a non-null T-vector such that . 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 [5].

The Parikh vector ${\mathbf P}(\sigma )$ of a finite sequence $\sigma$ of transitions is a T-vector counting the number of occurrences of each transition in $\sigma$, and the support of $\sigma$ is the support of its Parikh vector, i.e. $supp (\sigma )= supp ({\mathbf P}(\sigma ))=\{t\in T\mid {\mathbf P}(\sigma )(t)>0\}$.

Strong Connectedness and Cycles in an LTS. The LTS $(S,\rightarrow ,T,\iota )$ is said reversible if, $\forall s\in [\iota \rangle$, we have $\iota \in [s\rangle$, i.e., it is always possible to go back to the initial state; reversibility implies the strong connectedness of the LTS.

A sequence $s[\sigma \rangle s'$ is called a cycle, or more precisely a cycle at (or around) state s, if $s=s'$. A non-empty cycle $s[\sigma \rangle s$ is called small if there is no non-empty cycle $s'[\sigma '\rangle s'$ in $TS$ with ${\mathbf P}(\sigma ') \lneqq {\mathbf P}(\sigma )$, meaning that no component of the left vector is greater than the corresponding component of the right vector, and at least one is smaller (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\!=\!w_1\ldots w_k$ is the LTS with initial state $s_0$ defined as $s_0[w_1\rangle s_1 [w_2\rangle s_2 \ldots [w_k\rangle s_0$.

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 $\forall p\in P:(p^\bullet {\cap }{}^\bullet p)=\emptyset$, where $p^\bullet =\{t\in T\mid W(p,t)>0\}$ and ${}^\bullet p=\{t\in T\mid W(t,p){>}0\}$; CF (choice-free [5, 21]) or ON (place-output-nonbranching [17]) if $\forall p\in P:|p^\bullet |\le 1$; a WMG (weighted marked graph [8]) if $|p^\bullet |\le 1$ and $|{}^\bullet p|\le 1$ for all places $p\in P$. The latter form a subclass of the choice-free nets; other subclasses are marked graphs [7], which are plain with $|p^\bullet |=1$ and $|{}^\bullet p|=1$ for each place $p\in P$, and T-systems [4], which are plain with $|p^\bullet |\le 1$ and $|{}^\bullet p|\le 1$ for each place $p\in P$.

Isomorphism and Solvability. Two LTS $TS _1=(S_1,\rightarrow _1,T,s_{01})$ and $TS _2=(S_2,\rightarrow _2,T,s_{02})$ are isomorphic if there is a bijection $\zeta :S_1\rightarrow S_2$ with $\zeta (s_{01})=s_{02}$ and $(s,t,s')\in \rightarrow _1\,\Leftrightarrow (\zeta (s),t,\zeta (s'))\in \rightarrow _2$, for all $s,s'\in S_1$.

If an LTS $TS$ is isomorphic to $RG (\mathcal S)$ where $\mathcal S$ is a system, we say that $\mathcal S$ solves $TS$. Solving a word $w=\ell _1 \ldots \ell _k$ amounts to solve the acyclic LTS defined by the single path $\iota [\ell _1\rangle s_1 \ldots [\ell _k\rangle s_k$. 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,\rightarrow , T,\iota )$ is fully reachable if $S=[\iota \rangle$. It is forward deterministic if $s[t\rangle s'\wedge s[t\rangle s''\Rightarrow s'=s''$, and backward deterministic if $s'[t\rangle s\wedge s''[t\rangle s\Rightarrow s'=s''$.

A system $\mathcal S$ is forward persistent if, for any reachable markings $M,M_1,M_2$, $(M[a\rangle M_1 \wedge M[b\rangle M_2 \wedge a\ne b) \Rightarrow M_1[b\rangle M' \wedge M_2[a\rangle M'$ for a reachable marking $M'$; it is backward persistent if, for any reachable markings $M,M_1,M_2$, $(M_1[a\rangle M \wedge M_2[b\rangle M \wedge a\ne b) \Rightarrow M'[b\rangle M_1 \wedge M'[a\rangle M_2$ for a reachable marking $M'$.

Next, we recall classical properties of Petri net reachability graphs.

Proposition 1 (Classical Petri net properties)

If $\mathcal S$ is a Petri net system:

• $RG (\mathcal S)$ is a fully reachable LTS.

• $RG (\mathcal 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 [10].

Proposition 2 (Properties of WMG)

If $\mathcal S=(N,M_0)$ is a WMG system:

• It is forward persistent and backward persistent.

• If N is connected and has a T-semiflow $\nu$, then there is a unique minimal one $\pi$, with support T, and $\nu = k \cdot \pi$ for some positive integer k. Moreover, if there is a non-empty cycle in $RG (\mathcal S)$, there is one with Parikh vector $\pi$ in $RG (\mathcal S)$ around each reachable marking and $RG (\mathcal 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 behavioural properties satisfied by WMG (Propositions 1 and 2). We denote by

• b (for basic) the set of properties: forward and backward deterministic, forward and backward persistent, totally reachable;

• c (for cyclic) 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 [22, 23] can always be applied first, so as to handle connected partial solutions and recombine them afterwards. Hence, in the following, we focus on connected WMGs, without loss of generality. In the next section, we consider the synthesis problem of WMG with exactly two different labels.

3 Synthesis of a WMG from a Cyclic Binary LTS

In this section, we provide conditions for the WMG-solvability of 2-label cyclic LTS. In Subsect. 3.1, we investigate the WMG-solvability of a finite cyclic LTS: first when it is circular, then without this constraint. In Subsect. 3.2, we investigate the WMG-solvability of an infinite cyclic binary LTS.

3.1 WMG-solvable Finite 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\in \{a,b\}^*$, corresponding to the labels encountered by firing the circuit once from $\iota$, leading back to $\iota$. Changing the initial state in this LTS amounts to rotate w. Clearly, each such LTS satisfies property b, but is not always WMG- (nor even Petri net-) solvable.

The next results consider circuit Petri nets as represented in Fig. 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.

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 ${\mathbf P}(w) = (n,m)$ is prime.

Theorem 1 (Cyclically WMG-solvable binary words)

Consider a finite binary word w over the alphabet $\{a,b\}$, with ${\mathbf P}(w) = (n,m)$ and $n\le m$, the case $m\le n$ being 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^{m_0} \ldots ab^{m_{n-1}}$, where the sequence $m_0, \ldots , m_{n-1}$ is the sequence of quotients in the following system of equalities, with $r_0 = 0$:

$$ \left\{ \begin{array}{l} r_0 + m= m_0 \cdot n + r_1, \text { where } 0 \le r_1< n\\ r_1 + m = m_1 \cdot n+ r_2, \text { where } 0 \le r_2 < n\\ \ldots \\ r_{n-1} + m = m_{n-1} \cdot n. \end{array} \right. $$

Moreover, $m+n-1$ tokens are necessary and sufficient to solve the word cyclically.

Proof

From Proposition 2, for a connected WMG solution to exist, the Parikh vector of the word must be the minimal T-semiflow $\mu =(n,m)$ with support $T=\{a,b\}$, which is prime by definition, thus $gcd(m,n)=1$. A variant of this problem has been studied in [24], Sect. 6. Basing of this previous study, we highlight the following facts, leading to the claim. If a solution exists, then:

• there exists a WMG solution as pictured in Fig. 1, in which each firing preserves the number of tokens; thus, denoting by $M_s(p)$ the marking of place p at state s, the sum $M_s(p_{a,b})+M_s(p_{b,a})$ is the same for all states.

• Consider any two different reachable markings $M'$ and $M''$, then, from the above, $M'(p_{a,b}) \ne M''(p_{a,b})$ and $M'(p_{b,a}) \ne M''(p_{b,a})$.

• $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.e. a marking that enables no transition.

• For each i, $m_i\in \{\lfloor m/n \rfloor ,\lceil m/n\rceil \}$, there are $(m\!\!\!\mod \!n)$ b-blocks of size $(\lfloor m/n \rfloor \!+\!1)$, the other ones have size $\lfloor m/n \rfloor$.

Let us start from the state s such that $M_s(p_{a,b})=0$ and $M_s(p_{b,a})=m\,+\,n-1$, with $r_0=0$. We denote by $r_i$ the number of tokens in $p_{a,b}$ at the $(i\,+\,1)$-th visited state that enables a. The value $m_0$ is the maximal number of b’s that can be fired after the first a, and then $r_1$ tokens remain in $p_{a,b}$; hence, there are $m\,+\,n-1-r_1$ tokens in $p_{b,a}$ (which is at least m) before the second a. After the second a, we have $m+r_1$ tokens in $p_{a,b}$ and we fire $m_1$ b’s. We iterate the process until the initial state is reached.

In the state enabling the $(i+1)$-th a, there are $(i\cdot m)\mod n$ tokens in $p_{a,b}$, implying that $r_n$ equals 0 when the initial state is reached again. In between, we visited all the values from 0 to $n-1$ for the $r_i$’s: indeed, if $(i\cdot m)\mod n=(j\cdot m)\mod n$ for $0\le i<j<n$, we have $((j-i)\cdot m)\mod n=0$, or $(j-i)\cdot m=k\cdot 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, some rotation of $w'$ leads to w and to the associated value of $r_0$.    $\square$

An example is given in Fig. 2, where the elements of the sequence $m_0, \ldots , m_{n-1}$ are put in bold in the system on the left.

Fig. 2.

This system solves the word $w = ab^{2}ab^{3}ab^{2}ab^{3}ab^{3}ab^{2}ab^{3}ab^{3}$ cyclically.

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 label. In comparison, the previous algorithm of [24] checks a quadratic number of subwords.

The next lemma characterises the set of states reachable in any WMG whose underlying net is the one pictured in Fig. 1 and whose initial marking contains at least $n+m-1$ tokens.

Lemma 1 (Reachable states w.r.t. the number of tokens)

Let N be a binary WMG as in Fig. 1, such that with $\gcd (n,m)=1$. Then for each positive integer $k \ge m+n-1$, and each marking $M_0$ for N, the following properties are equivalent:

(1) $M_0$ contains exactly k tokens;

(2) RG$((N,M_0))$ contains exactly $k+1$ states;

(3) the set of states of RG$((N,M_0))$ is $\{(k_{ab}, k_{ba}) \in \mathbb {N}^2 \,|\, k_{ab} + k_{ba} = k\}$.

Proof

We first prove that (1) implies (2) and (3).

The case $k=m+n-1$ follows from the proof of Theorem 1: all the markings of the form $(k_{ab},m+n-1-k_{ab})$ with $k_{ab} \in [0,m+n-1]$ are reachable. By the preservation of the total number of tokens through firings, these markings are distinct and their amount is thus $n+m$, proving the claim for $k=m+n-1$.

In the following, let us denote by $S_\bot$ the set of all these markings (i.e. with exactly $m+n-1$ tokens).

The case $k = \ell \cdot (m+n-1)$ for some positive integer $\ell$ is deduced similarly: denoting $M_0$ as any sum of $\ell$ markings $M_1 \ldots M_\ell$ such that each $M_i$ corresponds to some distribution of k tokens over the two places, firing sequences are allowed in each $(N,M_i)$ that lead to all the markings of $S_\bot$, i.e. $S_\bot$ is the set of states of RG($(N,M_i)$) for each i and all these RG’s differ only by the choice of the initial state. All these sequences, obtained from all $i \in [1,\ell ]$, are allowed independently (sequentially as well as in a shuffle) in $(N,M_0)$. Thus, all the markings of the form $(k_{ab},k-k_{ab})$ with $k_{ab} \in [0,k]$ are mutually reachable, describing $k+1$ distinct markings, which correspond to all the possibilities of distributing k tokens over the two places.

Now, let us consider $k>m+n-1$, denoting the initial marking as $M_0 = (u+u',v+v')$ such that $u+v = \ell \cdot (m+n-1)$, $\ell \in \mathbb {N}_{>0}$, and $u',v'$ are non-negative integers with $m+n-1 > u'+v' \ge 1$. From the above, all the markings of the form $M+(u',v')$, where M belongs to RG(N, (u, v)) are reachable from $M_0$, describing $u+v+1$ distinct markings. Other markings can be reached by firing the tokens of $u'$ and $v'$: for each $x \in [0;u'-1]$ and each $y \in [0;v'-1]$, the markings $(x+n,k-x-n)$ and $(k-y-m,y+m)$ are reachable, from which we may fire b and a, respectively, leading to markings $(x,k-x)$ and $(k-y,y)$, and all these markings are distinct. Thus, we reach at least $u+v+1+u'+v'=k+1$ distinct markings, which describe all the possible distributions of k.

We deduce that (1) implies (2) and (3). Now, assuming (2), and from the reasoning above, $M_0$ cannot have strictly less nor strictly more than k tokens, implying (1). Finally, (3) describes all the $k+1$ distributions of the k tokens over the two places, all of these markings being mutually reachable by reversibility, hence (1) and (2) are obtained.    $\square$

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 behaviour of the process. This result investigates the possible WMG-solvable LTS for this vector.

Theorem 2 (WMG-solvable reversible binary LTS)

Let us consider such that $\gcd (n,m)=1$, and a positive integer k. Up to isomorphism and the choice of the initial state, when $k \ge n+m$, there exists a single finite WMG-solvable LTS $(S,\rightarrow ,\{a,b\},\iota )$ that satisfies b, c and $|S| = k$, and that contains a small cycle whose Parikh vector is $\mu$. No such WMG-solvable LTS exists when $k < n+m$. In the particular case of $S=\{0,1,\ldots ,m+n-1\}$, we have (up to isomorphism) $\rightarrow =\{(i,a,i+m)|i,i+m\in S\}\cup \{(i,b,i-n)|i,i-n\in S\}$.

Proof

If a solution exists, it has the form of Fig. 1. If $k \ge n+m$, there are exactly $k-1$ tokens in the system by Lemma 1 and the reachability graph is unique up to isomorphism. From the previous results of this section, if $M_0=n+m-1$, then the RG is circular and contains exactly $n+m$ distinct 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 $\{(i,a,i+m)|0\le i,i+m<n+m\in S\}\cup \{(i,b,i-n)|0\le i,i-n<n+m \in S\}$. As a consequence, if $|S|<n+m$, there aren’t enough states to close the circuit, and there is no solution. The rest of the claim immediately results from Lemma 1.    $\square$

3.2 WMG-solvable Infinite Cyclic Binary LTS

Let us consider an infinite LTS satisfying b and c with only two different labels. From the previous section, it cannot correspond to a net of the kind illustrated in Fig. 1 since $i+j$ remains constant, hence yields finitely many states. On the other hand, a net of the kind illustrated in Fig. 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).

Fig. 3.

A WMG solution for the infinite cyclic case.

If $n=1$, i is the maximum number of consecutive executions of b from $\iota$; 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\cdot m+l\cdot n=1$. If $l\ge 0\ge k$, i is the maximum number of times we may execute $a^{-k}b^{l}$ consecutively from $\iota$, and we can check again if the given LTS corresponds to the constructed net (this is a direct generalisation of the case $n=1$). Otherwise, since $-n\cdot m+m\cdot n=0$, by adding this relation enough times to the previous one, we get $k'\cdot m+l'\cdot n=1$ with $l'\ge 0\ge k'$, and we apply the same idea.

4 WMG-solvable Acyclic LTS: A Geometric Approach

In what follows, we consider any acyclic LTS satisfying property b. First, in Subsect. 4.1, we give a geometric interpretation of WMG-solvability for acyclic LTS with only two different labels. Then, in Subsect. 4.2, we extend this result to any number of labels.

4.1 Geometric Characterisation for 2 Labels

In the following, we specialise to the WMG case the more general framework considered in [16], Theorem 2, using convex sets of $\mathbb {N}^2$. The standard definition of convex sets of $\mathbb {R}^2$ is given by the segment-inclusion property: a set $C\subseteq \mathbb {R}^2$ is convex if and only if, for any $x,y\in C$, $[x,y]\subseteq C$, where [x, y] is the linear segment with extremities x and y. However, this does not work for $\mathbb {N}^2$ (nor $\mathbb {Z}^2$), as illustrated by Fig. 4: in the set $C=\{x,y,z\}$ with $x=(0,0)$, $y=(1,2)$ and $z=(2,1)$, we have $[x,y]=\{x,y\}$, $[y,z]=\{y,z\}$ and $[z,x]=\{z,x\}$; hence we have the segment-inclusion property; however, clearly, this set should not be considered as convex since the node $X=(1,1)$ is missing.

In [25], two equivalent definitions of convex sets in lattices like $\mathbb {Z}^2$ are provided, which immediately extend to $\mathbb {N}^2$:

• 1. either as the intersection of a convex set of $\mathbb {R}^2$ with $\mathbb {Z}^2$,

• 2. or as the intersection of half planes ${\mathcal L}_i$, with ${\mathcal L}_i=\{(x,y)\in \mathbb {Z}^2|a_i\cdot x+b_i\cdot y\ge c_i \text{ for } \text{ some } a_i,b_i,c_i\in \mathbb {Z}\}$. If the convex set is finite, we can use a finite set of such half-planes, otherwise we may need (countably) infinitely many of them (notice that infinite convex sets exist with a boundary defined by finitely many half-planes).

Fig. 4.

Non-convex set in $\mathbb {Z}^2$ with the segment-inclusion property.

In order to characterise the acyclic LTS that are solvable by WMG nets with two labels, we first identify isomorphically each state s with:

$\varDelta _s=({\text {number of}\, a\text {'s in any path from } \iota \text { to }s}, {\text {number of }b\text {'s in any path from }\iota \text { to }s})$ (this is coherent from Proposition 2), which amounts to consider for S a part of $\mathbb {N}^2$ containing $(0,0) (=\iota )$. From the full reachability, S is connected (there is a directed path from (0, 0) to any $(i,j)\in S$, hence an undirected path between any two states). From Keller’s theorem [26] (due to determinism and persistence), full reachability and Proposition 2, we have that $(i,j){\mathop {\rightarrow }\limits ^{a}}(i',j')\iff i'=i+1\wedge j'=j$ and $(i,j){\mathop {\rightarrow }\limits ^{b}}(i',j')\iff i'=i\wedge j'=j+1$.

Fig. 5.

General places for a WMG synthesis, with initial marking $m_{a,b} = M_0(p_{a,b})$, $m_{a,*} = M_0(p_{a,*})$ and $m_{*,b} = M_0(p_{*,b})$.

If the system is WMG-solvable, it must be defined by a finite set of places of the kind $p_{a,b}$ and $p_{b,a}$ in Fig. 5 (with $\gcd (W_a,W_b)=1$ and $m_{a,b}, m_{b,a}\ge 0$), including the special cases $p_{*,b}$ (with $W_a=0$, $W_b=1$ and $m_{*,b}>0$, the case $m_{*,b}=0$ only serving to make b non-firable but we assumed the system weakly live) or $p_{*,a}$, and $p_{a,*}$ (with $W_b=0$, $W_a=1$ and $m_{*,a}=m_{a,*}=0$) or $p_{b,*}$. For a place $p_{a,b}$, we have for each state $s=(i,j)$ that the corresponding marking is $M_s(p_{a,b})=M_0(p_{a,b})+i\cdot W_a-j\cdot W_b$, and since we must have $M_s(p_{a,b})\ge 0$, this defines a ‘region’, both in the sense of [27] and in an intuitive geometric meaning: $R_{p_{a,b}}=\{(i,j)|M_0(p_{a,b})+W_a\cdot i-W_b\cdot j\ge 0\}$ or, permuting the roles of a and b, $R_{p_{b,a}}=\{(i,j)|M_0(p_{b,a})-W_a\cdot i+W_b\cdot j\ge 0\}$, i.e. in either case the intersection of $\mathbb {N}^2$ with a half plane of $\mathbb {Z}^2$. These regions will be called in the following WMG-regions. Notice that [16] considers additional regions, where $W_a<0$ or $W_b<0$. Each such region is convex, as well as any intersection of such regions.

We deduce the next specialisation of Theorem 2 in [16].

Theorem 3 (WMG-solvable acyclic binary LTS)

An acyclic LTS satisfying property b is WMG-solvable if and only if, when applied on $\mathbb {N}^2$, its set of states S is connected, convex and delimited by (i.e., it is the intersection of) a finite set of WMG-regions. A possible solution is then provided by the places corresponding to these regions.

For any finite LTS, if it is the intersection of WMG-regions, it is the intersection of a finite set of such regions. However, the result may be extended to an infinite LTS, but then it may be necessary to specify that only a finite set of regions is allowed. This is illustrated by Fig. 6.

Fig. 6.

Illustration of Theorem 3.

Fig. 7.

Convex sets defined by WMG-regions may be non-totally reachable in $\mathbb {N}^2$.

Note that total reachability does not arise from WMG-regions alone, as illustrated by Fig. 7: on the left, the points $\iota =(0,0)$, (1, 0) and (2, 1) form a convex set of $\mathbb {N}^2$, intersection of the WMG-regions $i-2\cdot j\ge 0$ and $1-i+j\ge 0$ (plus $j\ge 0$ to certify being in $\mathbb {N}^2$), but (2, 1) is not reachable from $\iota$. These WMG-regions yield the WMG system on the right of the same figure.

A closer look shows that state $\iota$ corresponds to marking (1, 0), state (1, 0) to marking (0, 1) and (2, 1) to marking (0, 0). The latter is not reachable, but is potentially reachable in the sense of [5]. Let us recall that, from the classical state equation $M[\sigma \rangle M'\Rightarrow M'=M+C\cdot {\mathbf P}(\sigma )$ where C is the incidence matrix, and that a marking M is potentially reachable from the initial marking $M_0$ if $M=M_0+C\cdot \alpha$ for some T-vector (non-necessarily the Parikh vector of some firing sequence). Indeed, here $C=\left( \begin{array}{rr} -1&{}1\\ 1&{}-2\end{array}\right)$, and $(0,0)=(1,0)+C\cdot (2,1)$ (caution: here the vectors are to be considered as column vectors).

Another possible interpretation is to consider the net on the right of Fig. 7 as a continuous or fluid one, in the sense of [28]. In those models, a transition may be executed fractionally and reachable markings may be real vectors with no negative component. Thus, in our case, we can have the firing sequence

$$(1,0)[a\rangle (0,1)[b^{1/2}\rangle (1/2,0)[a^{1/2}\rangle (0,1/2)[b^{1/4}\rangle (1/4,0)[a^{1/4}\rangle (0,1/4)[b^{1/8}\rangle (1/8,0)\ldots $$

We cannot finitely reach the marking (0, 0), but if we allow limit-reachability, then the accumulated firings $2\cdot a+b$ finally lead to the marking (0, 0). More generally, the whole interior of the shown convex set becomes reachable.

Next, we generalise these notions and results to any number of labels.

4.2 Geometric Characterisation for Any Number of Labels

Let us consider an acyclic LTS satisfying property b with n labels $t_1,t_2,\ldots ,t_n$. Again, we identify each state s to its distance $\varDelta _s\in \mathbb {N}^n$, giving for each i the number of $t_i$’s in any path from $\iota$ to s. Arcs are defined by the relations $s[t_i\rangle s'$ when $s,s'\in S$, $\varDelta _{s'}(t_i)=\varDelta _{s}(t_i)+1$ and $\varDelta _{s'}(t_j)=\varDelta _{s}(t_j)$ for some i and any $j\ne i$.

We consider special WMG-regions of the kind $k+h\cdot x_i-l\cdot x_j\ge 0$ for some $k,h\ge 0$, $l>0$ and $i\ne j$. In particular, each of them is either parallel to a plane including two axes (if $h>0$), or perpendicular to one axis (if $h=0$). From the specialisation of [16], we deduce the following.

Theorem 4 (WMG-solvable acyclic n-ary systems)

An acyclic LTS satisfying property b with n different labels is WMG-solvable if and only if, when applied on $\mathbb {N}^n$, its set of states S is connected, convex and delimited by (i.e., it is the intersection of) a finite set of WMG-regions. A possible solution is then provided by the places corresponding to these regions.

However, this characterisation is less intuitively (visually) interpretable when $n>2$. Hence it will usually be more efficient to use the general WMG synthesis procedure described in [10].

5 A Sufficient Condition of Circular WMG-solvability for Any Number of Labels

In this section, we provide a general sufficient condition for the cyclic solvability of k-ary words, for any positive integer k. This condition, embodied by the next theorem, uses binary subwords obtained by projection² and containing occurrences of two different labels that are contiguous somewhere 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 5

Consider any word w over any finite alphabet T such that ${\mathbf P}(w)$ is prime. Suppose the following: (i.e., the projection of w on $\{t_1,t_2\}$) for some $t_1,t_2$ such that $t_1 \ne t_2 \in T$, and $w = (w_1 t_1 t_2 w_2)$ or $w = (t_2 w_3 t_1)$, $u = v^\ell$ for some positive integer $\ell$, ${\mathbf P}(v)$ is prime, and v is cyclically solvable by a circuit. Then, w is cyclically solvable with a WMG.

Proof

For every such pair $(t_i,t_j)$, $i< j$, let $C_{i,j}= ((P_{i,j},T_{i,j},W_{i,j}),M_{i,j})$ be a circuit solution of v for the subword , obtained as in the construction of Theorem 1. Assuming all these nets are place-disjoint (which is always possible since the Petri net solutions are considered up to isomorphism), consider the transition-merging³ of all these marked circuits. The result is a WMG $\mathcal S'=(N',M_0')$ such that $N'=(P',T,W')$ with $P' = \cup _{i,j} P_{i,j}$, $T = \cup _{i,j} T_{i,j}$, $W' = \cup _{i,j} W_{i,j}$, and $M'_0 = \cup _{i,j} M_{i,j}$.

Let w be of the form $aw'$. We prove that a is the only transition enabled in $\mathcal S'$.

All the subwords of the form 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 $\mathcal S'$. Since d is not the first label of w, another label q appears in w just before the first occurrence of d. In the solution of , 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 $\mathcal S'$ has the language ${ {PREF}}(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 ${ {PREF}}(u^*)={ {PREF}}(v^*)$. $C_{i,j}$ is a circular solution for v, but not for u unless $\ell =1$. The fact that the merging $\mathcal S'$ of all the $C_{i,j}$’s yields not only a system with the adequate language ${ {PREF}}(w^*)$ but a circular solution of w arises from the fact that ${\mathbf P}(w)$ is prime (by Proposition 2). We thus deduce that the WMG $\mathcal S'$ solves w cyclically.    $\square$

6 Synthesis of WMGs from Live Ternary LTS

In this section, we provide several conditions of WMG-solvability for a ternary LTS. We first develop a characterisation of WMG-solvability for a subclass of the cyclic ternary words in Subsect. 6.1. Then, in Subsect. 6.2, we construct two counter-examples to this condition: one for four labels with three different values in the Parikh vector, and another one for five labels with only two different values.

6.1 WMG-solvability in a Subclass of the Finite Circular Ternary LTS

First, we prove the other direction of Theorem 5, leading to a full characterisation 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 Fig. 8. In some cases, a smaller number of places can solve the same LTS, but we do not aim here at minimising the number of nodes in a solution.

Fig. 8.

A generic WMG with three labels, with minimal T-semiflow (x, x, y) and $\gcd (x,y)=1$.

Theorem 6 (Cyclic solvability of ternary words)

Consider a ternary word w over 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 such that $t_1\ne t_2 \in T$, and $w = (w_1 t_1 t_2 w_2)$ or $w = (t_2 w_3 t_1)$, $u = v^\ell$ for some positive integer $\ell$, ${\mathbf P}(v)$ is prime, and v is cyclically solvable by a circuit (i.e. a circular net).

Proof

The right-to-left direction of the equivalence, assuming the properties on the projections, is true by Theorem 5, 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 since $w=t_1t_2t_3$, up to some permutation, and an easy marked graph solution may be found. Let us thus assume that $x\ne 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 ${\mathbf P}(w)$, we have ${\mathbf P}(w)(u)\cdot W_u={\mathbf P}(w)(v)\cdot W_v$, and we may choose $W_u={\mathbf P}(w)(v)$ as well as $W_v={\mathbf 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 Fig. 8. We denote by RG the reachability graph of a solution based on this net.

We show first that the projection 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’s) because, if $M_1[a\rangle M_2[a\rangle M_3[b\rangle$, $M_1(p_{c,b})=M_2(p_{c,b})=M_3(p_{c,b})\ge y$ and $M_2(p_{a,b})\ge 1$, which would also allow to perform b after the first a and RG is not circular.

If there is a pattern aac and $M_1[a\rangle M_2[a\rangle M_3[c\rangle M_4$, $M_2(p_{a,c})\ge y$ and $M_1(p_{b,c})=M_2(p_{b,c})=M_3(p_{b,c})\ge x$, hence $y<x$ otherwise $M_2$ already enables c and RG is not circular. Then $M_4(p_{a,b})\ge 2$, $M_4(p_{c,b})\ge x>y$ and $M_4(p_{c,a})\ge x> y$, so that $M_4[b\rangle$; hence $M_4(p_{b,a})=0$ since otherwise we also have $M_4[a\rangle$ and RG is not circular. We thus have $M_4[ba\rangle M_5$ for some marking $M_5$, with $M_5(p_{b,a})=0$, so that $M_5$ does not enable a; $M_5$ does not enable b either since otherwise we could also perform $M_4[bb\rangle$ and again RG is not circular. Thus, we have $M_4[bac\rangle$, and then we are in a situation similar to the one after the first c. As a consequence, we must have a sequence $M_1[aa(cba)^\omega \rangle$, and RG is not circular.

Hence, in $w^2$ we cannot have a sequence aa, nor bb by symmetry.

Let us now assume that a pattern $ac^ka$ exists in $w^2$ for some $k\ge 1$. Since the first firing of a puts a token in $p_{a,b}$ and the next firing of c does not enable b, we must have $x < y$. Let us assume in the circular RG that $M_1[ac^ka\rangle M_2[\sigma \rangle M_1$. $\sigma$ 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 $M_1(p_{b,a})\ge 2$ (in order to fire a twice without a b in between), so that if $M_3[b\rangle M_1[a\rangle$, $M_3(p_{b,a})\ge 1$, we must also have $M_3[a\rangle$, and RG is not circular. Hence, $\sigma$ ends with a c and for some reachable markings $M'_2$ and $M_3$ we have $M_3[c\rangle M_1[ac^k\rangle M'_2[a\rangle M_2$.

We deduce that $M'_2(p_{a,b})\ge 1$, $M'_2(p_{c,b})\ge (k+1)\cdot x$; hence $(k+1)\cdot x<y$ otherwise $M'_2$ also enables b and RG is not circular. Also, $M_3(p_{b,a})\ge 2$ and $M_3(p_{c,a})\ge 2\cdot y - (k+1)\cdot x>y$, so that $M_3$ also enables a and again RG is not circular. As a consequence, we cannot have a pattern $ac^ka$, nor $bc^kb$ by symmetry, and or for the positive integer $k=x$. With $v=ab$ or $v=ba$, we have the adequate solvability property for , and we can assume in the following that the sum of the tokens present in places $p_{a,b}$ and $p_{b,a}$ is 1 for all reachable markings.

Let us now suppose that we have a WMG $\mathcal S$ solving w cyclically, whose underlying net is pictured in Fig. 8. From the previous results, we can assume that $M_0(p_{a,b})+M_0(p_{b,a})=1$ in $\mathcal S$, this equality being preserved by all reachable markings. To show that has the adequate form (the case for is symmetrical), let us consider the circuit $C_{ac}$, restriction of $\mathcal 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^\ell$ for some positive integer $\ell$, where ${\mathbf P}(v)$ is prime and v is cyclically solvable. Since $gcd(x,y)=gcd({\mathbf P}(w)(a),{\mathbf P}(w)(c))=gcd({\mathbf P}(u)(a),{\mathbf P}(u)(c))=1$, ${\mathbf P}(u)$ is prime and $u=v$ with $\ell =1$, hence u is not cyclically solvable. For the net N considered, this implies the existence of some prefix $\sigma _{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 $\sigma _{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 $\mathcal S = (N,M_0)$ solve w cyclically, the smallest prefix of w whose projection on $\{a,c\}$ equals $\sigma _{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.

Case $x>y$: In this case, in $\mathcal S$, we cannot have two consecutive c’s.

• Subcase in which M enables the place $p_{a,c}$ as well as the transition a in the WMG, hence its input places $p_{b,a}$ and $p_{c,a}$. Since $M[a\rangle$, transition c is not enabled at M, implying that $p_{b,c}$ is not enabled by M. We deduce: $M(p_{a,c}) > M(p_{b,c})$. Since $p_{a,c}$ is enabled by M, the last occurrence of a transition before the next firing of c is necessarily b, implying: $M[(ab)^kc\rangle M_1$ for some integer $k \ge 1$ and some marking $M_1$. The inequality mentioned above is still valid at $M_1$, i.e. $M_1(p_{a,c}) > M_1(p_{b,c})$, and we iterate the same arguments from $M_1$ to deduce that the rotation $w_M$ of w starting at M is of the form $(ab)^{k_1}c \ldots (ab)^{k_y}c$ with $\sum _{i=1..y} k_i=x$ 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, the firing of c from M cannot enable a, implying that $M(p_{c,b})<M(p_{c,a})$ and that $M[c(ba)^kc\rangle M_1$ for some positive integer k and a marking $M_1$. The inequality is still valid at $M_1$, i.e. $M_1(p_{c,b})<M_1(p_{c,a})$, from which we deduce that the rotation $w_M$ of w starting at M is of the form $c(ba)^{k_1} \ldots c(ba)^{k_y}$ with $\sum _{i=1..y} k_i=x$ and each $k_i$ is positive.

Case $x \le y$:

• 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\rangle 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^{k_1} \ldots abc^{k_x}$ with $\sum _{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^kba\rangle 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^{k_1}ba \ldots c^{k_x}ba$ with $\sum _{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 is obtained from 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.    $\square$

6.2 Counter-Examples for 4 and 5 Labels

In Theorem 6, we provided a characterisation of cyclic WMG-solvability for ternary words w such that ${\mathbf P}(w)$ is prime with two values. However, this result does not apply to words w over 4 labels with 3 values nor 5 labels with 2 values, even if ${\mathbf P}(w)$ is prime. Indeed, Fig. 9 pictures two counter-examples: on the left, the WMG cyclically solves the word $w = aacbbdabd$ with ${\mathbf P}(w)=(3,3,1,2)$, which is prime, while its projection $u=aabbab$ on $\{a,b\}$ leads to $v=u$, and ${\mathbf P}(v)=(3,3)$ is not prime, hence is not cyclically solvable by a WMG; on the right, the WMG cyclically solves the word $w = aacbbeabd$ with ${\mathbf P}(w)=(3,3,1,1,1)$, which is prime, while its projection $u=aabbab$ on $\{a,b\}$ leads to $v=u$, and ${\mathbf P}(v)=(3,3)$ is not cyclically solvable by a WMG.

Fig. 9.

The WMG on the left solves aacbbdabd cyclically, and the WMG on the right solves aacbbeabd cyclically.

However, presently we do not know what happens for ternary words w such that ${\mathbf P}(w)$ is prime with three values, nor when w has four labels and ${\mathbf P}(w)$ is prime with two values.

7 Conclusions and Perspectives

In this work, we specialised 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 labels, we provided a characterisation of the WMG-solvable labelled transition systems formed of a single cycle. We also extended this investigation to finite LTS containing several cycles, and to infinite LTS.

Then, leaving out the restriction on the number of labels, we developed a geometric characterisation for acyclic LTS, using convex sets and the theory of regions; in the case circular LTS, we proposed a sufficient condition of WMG-solvability.

We exploited this sufficient condition to obtain a full characterisation of circular WMG-solvability for a subset of the possible Parikh vectors over three labels.

Finally, we proved that this condition for 3 labels does not extend to circular LTSs with 4 labels and three different Parikh values, nor with 5 labels and two Parikh values.

As perspectives of this work, we believe that relaxations of our statements may lead to other characterisations of WMG-solvable LTS, together with efficient algorithms for their analysis and synthesis.