Several works have proposed methods for the analysis and synthesis of Petri net subclasses from labelled transition systems (LTS). In this paper, we focus on Choice-Free (CF) Petri nets, in which each place has at most one output, and their subclass of Weighted Marked Graphs (WMGs). We provide new conditions for the WMG-synthesis from a circular LTS, i.e. forming a single circuit, and discuss the difficulties in extending these new results to the CF case.
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 worst-case intractable, and the efficiency of synthesis algorithms varies widely depending on the constraints imposed on the desired solution. In this study, we focus on the Petri net synthesis problem from a labelled transition system (LTS), which consists in determining the existence of a Petri net whose reachability graph is isomorphic to the given LTS, and building such a Petri net solution when it exists.
In previous studies on analysis or synthesis, structural restrictions on nets
encompassed plain nets (each weight equals 1; also called ordinary nets) [
In this paper, we study the problem of solvability of LTS with weighted marked
graphs (each place has at most one output transition and one input transition)
and choice-free nets (each place has at most one output transition). Both these
classes are important for real-world applications, and they are widely studied
in the literature [
An important purpose of studying such constrained LTS is to better understand
the relationship between LTS decompositions and their solvability by Petri nets.
Indeed, the unsolvability of simple subgraphs of the given LTS, typically
elementary paths (i.e. not containing any node twice) and cycles (i.e. closed paths,
whose start and end states are equal), often induces simple conditions of
unsolvability for the entire LTS, as highlighted in other works [
Contributions. In this work, we study further the links between simple LTS structures and the reachability graph of WMGs and CF nets, as follows. First, we show that a binary LTS is CF-solvable if and only if it is WMG-solvable. Then, we provide new general conditions for the WMG-solvability of a cyclic word over an arbitrary alphabet, together with an algorithm synthesizing a cyclical WMG-solution for a given word. We also discuss the difficulties of extending these results to the CF class.
Organisation of the paper. After recalling classical definitions, notations and properties in Section 2, we present the equivalence of CF- and WMG-solvability for 2-letter words in Section 3. Then, in Section 4, we focus on circular LTS: we develop a new characterisation of WMG-solvability and a dedicated synthesis algorithm. We also provide a number of examples, which demonstrate that some of the presented results cannot be applied to the class of CF-nets. Finally, Section 5 presents our conclusions and perspectives. 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.
LTS, sequences and reachability. A labelled transition system with initial state, LTS for short, 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. Generalising to any (firing) sequences σ ∈ T ∗, s[εi and s[εis are always true, with ε being an empty sequence; 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. For clarity, in case of long formulas we write |rσ|sτ |q instead of r[σis[τ iq, thus fixing some intermediate states along a firing sequence. A state s0 is reachable from state s if ∃σ ∈ T ∗ : s[σis0. The set of states reachable from s is noted [si. TS = (S, →, T, ι) is fully reachable if S = [ιi.
Petri nets and reachability graphs. 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 [M0i, the set of labels T , initial state M0 and transitions
{(M, t, M 0) | M, M 0 ∈ [M0i ∧ M [tiM 0}. A system S is bounded if RG (S) is finite.
Vectors. The support of a vector is the set of the indices of its non-null
components. Consider any net N = (P, T, W ) with its incidence matrix C. A T-vector
is an element of NT ; it is called prime if the greatest common divisor of its
components is one (i.e., its components do not have a common non-unit factor). A
T-semiflow ν of the net is a non-null T-vector such that C · ν = 0. A T-semiflow
is called minimal when it is prime and its support is not a proper superset of
the support of any other T-semiflow [
The Parikh vector P(σ) of a finite sequence σ of transitions is a T-vector counting the number of occurrences of each transition in σ, and the support of σ is the support of its Parikh vector, i.e., supp(σ) = supp(P(σ)) = {t ∈ T | P(σ)(t) > 0}. 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 nonempty cycle s0[σ0is0 in TS with P(σ0) P(σ) (the definition of Parikh vectors extending readily to sequences over the set of labels T of the LTS). A cycle s[σis is prime if P(σ) is prime. TS has the prime cycle property if every small cycle has a prime Parikh vector.
A circular LTS is a finite, strongly connected LTS that contains a unique cycle; hence, it has the shape of an oriented circle. The circular LTS induced by a word w = w1 . . . wk is the LTS with initial state s0 defined as s0[w1is1[w2is2 . . . [wkis0. All notions defined for labelled transition systems apply to Petri nets through their reachability graphs.
Petri net subclasses. A net N is plain if no arc weight exceeds 1; pure if
∀p ∈ P : (p•∩•p) = ∅, where p• = {t ∈ T | W (p, t)>0} and •p = {t ∈ T |
W (t, p)>0}; CF (choice-free [
Isomorphism and solvability. Two LTS TS 1 = (S1, →1, T, s01) and TS 2 = (S2, →2, T, s02) are isomorphic if there is a bijection ζ : S1 → S2 with ζ(s01) = s02 and (s, t, s0) ∈→1 ⇔ (ζ(s), t, ζ(s0)) ∈→2, for all s, s0 ∈ S1.
If an LTS TS is isomorphic to RG (S), where S is a system, we say that S solves
TS . Solving a word w = `1 . . . `k amounts to solve the acyclic LTS defined by the
single path ι[`1is1 . . . [`kisk. A finite word w is cyclically solvable if the circular
LTS induced by w is solvable. An LTS is WMG-solvable if a WMG solves it.
Separation problems. Let T S = (S, →, T, s0) be a given labelled transition
system. The theory of regions [
If the LTS is infinite, also the number of separation problems (of each kind) becomes infinite.
A synthesis procedure does not necessarily lead to a connected solution. However,
the technique of decomposition into prime factors described in [
In this section, we link the CF-solvability of a reversible LTS with 2 letters to the WMG-solvability.
Lemma 1 (Pure CF-solvability).
If a reversible LTS has a CF-solution, it has a pure CF-solution. Proof. Let TS = (S, →, T, ι) be a reversible LTS. First, we observe that, if t ∈ T does not occur in →, TS is solvable iff TS 0 = (S, →, T \ {t}, ι) is solvable and a possible solution of TS is obtained by adding to any solution of TS 0 a transition t and a fresh place p, initially empty, with an arc from p to t (e.g. with weight 1), so that t is pure. We may thus assume that each label of T occurs in →. k1 k2 a1 a2 . . . km am μ0 p
h k+h x
The general form of a place in a CF-solution is exhibited in Figure 1. If h = 0, we are done, so that we shall assume h > 0. If −h ≤ k < 0, the marking of p cannot decrease, and since x occurs in →, the system cannot be reversible. If k = 0, for the same reason all the ki’s must be null too, μ0 ≥ h, and we may drop p. Hence we assume that k > 0 and ∃i : ki > 0. Once x occurs, the marking of p is at least h, remains so, and since the system is reversible, all the reachable markings have at least h tokens in p. But then, if we replace p by a place p0 with initially μ0 − h tokens, the same ki’s and h = 0, we shall get exactly the same reachability graph, but with h tokens less in p0 than in p. This will wipe out the side condition5 for p, and repeating this for each side condition, we shall get an equivalent pure and choice-free solution. Theorem 1 (Reversible binary CF-solvability).
A binary reversible LTS is CF-solvable iff it is WMG-solvable.
Proof. If we have two labels, from Lemma 1, if there is a CF-solution, there will be one with places of the form exhibited in Figure 2, hence a WMG-solution. tu tu a m
i n
b
In the next section, the number of letters is no more restricted. 4
In this section, we recall and extend the conditions for WMG-solvability of some
restricted classes of LTS formed by a single circuit, which were suggested in [
Theorem 3 (Cyclic WMG-solvability of ternary words [
3 a 2 3 c d 3 3 2 b a a m m pa,b pb,a i j n n 3 3 3 c d e 3 3 3 3 a 2 3 c d 3 3 2
b For a circular LTS, the solvability of its binary projections by circuits is a sufficient condition, as specified by Theorem 2, but it turns out not to be a necessary one. Indeed, for the cyclically solvable sequence w1 = aacbbdabd (cf. left of Fig. 4), its binary projection on {a, b} is w1 a,b = aabbab which is not cyclically solvable with a WMG (neither generally solvable). Looking only at the Parikh vector of the sequence is also not enough to establish its cyclical (un)solvability. For instance, sequences w2 = abcabdabd and w3 = abcbadabd are Parikh-equivalent: P(w2) = P(w3) = (3, 3, 1, 2) (and also Parikh-equivalent to w1), but w2 is cyclically solvable with a WMG (e.g. with the WMG on the right of Fig. 4) and w3 is not WMG-cyclically solvable.
All the binary projections of w1 and w3 are cyclically WMG-solvable, except wi a,b. But only the unsolvability of w3 a,b implies the unsolvability of w3. Since all the wi are Parikh-equivalent, then so are their binary projections. So, to find the difference we have to look at the sequences themselves, without abstracting to Parikh-vectors. Since the projections w1 a,b and w3 a,b are equivalent (up to cyclical rotation and swapping a and b), it is also not enough to look only at the ‘problematic’ binary projections. We then look at the conditions for solvability of separation problems. 4.1
SSPs for Prime Cycles a m μ0 n
b
Lemma 2 (SSPs are solvable for prime cycles). If for the cyclical transition system T S = (S, →, T, s0) defined by some word w = t0 . . . tk, where S = {s0, . . . , sk}, →= {(si−1, ti−1, si) | 1 ≤ i ≤ k} ∪ {(sk, tk, s0)} with ti ∈ T , P(w) is prime, then all the SSPs are solvable.
Proof. If |T | = 1, then k = 0 (otherwise P(t0 . . . tk) is not prime) and |S| = 1, so that there is no SSP to solve. We may thus assume |T | > 1.
For 0 ≤ i, j ≤ k such that si 6= sj (so that i 6= j), we note Pij = P(titi+1 . . . tj−1) if i < j and Pij = P(titi+1 . . . tk−1tkt0t1 . . . tj−1) if i > j. For each pair of distinct labels a, b ∈ T that are adjacent in T S, construct places pa,b (and pb,a since adjacency is commutative) as in Fig. 5 with m =
P(w)(b) gcd(P(w)(a), P(w)(b)) , n =
P(w)(a) gcd(P(w)(a), P(w)(b)) and μ0 = n · P(w)(b). Clearly, the markings of pa,b reachable by repeatedly firing u = w ab are always non-negative, and the initial marking is reproduced after each repetition of the sequence u. Consider two distinct states si, sj ∈ S (w.l.o.g. i < j). We now demonstrate that there is at least one place of the form pa,b such that Mi(pa,b) 6= Mj (pa,b), where Ml denotes the marking corresponding to state sl for 0 ≤ l ≤ k. If j − i = 1, then any place of the form pti,∗ distinguishes states si and sj . The same is true if j − i > 1 but ∀l ∈ [i, j − 1] : tl = ti. Otherwise, choose some letter a from ti . . . tj−1 and an adjacent letter b. Then Mj (pa,b) = Mi(pa,b) + m · Pij (a) − n · Pij (b). If Mi(pa,b) 6= Mj (pa,b), place pa,b distinguishes si and sj . Otherwise we have m · Pij (a) = n · Pij (b), hence, due to the choice of m and n: (so that b also belongs to ti . . . tj−1). Consider some other letter c which is adjacent to a or b. If place pa,c distinguishes si and sj , we are done. Otherwise, Pij (a) P(w)(a) due to the choice of the arc weights for these places, we have
Since ti . . . tj−1 is finite, by progressing along the adjacency relation, either we find a place which has different markings at si and sj , or for all a, b ∈ supp(ti . . . tj−1) we have
If supp(ti . . . tj−1) = supp(w), P(w) is proportional to P(ti . . . tj−1), but since
ti . . . tj−1 is smaller than w (otherwise si = sj ) this contradicts the primality of
P(w). Hence, there exist adjacent c and d such that c ∈ supp(w)\supp(ti . . . tj−1)
and d ∈ supp(ti . . . tj−1). For the place pc,d we have Mj (pc,d) 6= Mi(pc,d). tu
This property has some similarities with Theorem 4.1 in [
The reachability graph of any CF net, hence of any WMG, satisfies the prime
cycle property [
ESSPs in Cyclical Solvability with WMGs Now, consider further conditions for the cyclical WMG-solvability of a sequence w = t0 . . . tk, where P(w) is prime. Let us assume that the system ((P, T, W ), M0) is a WMG solving w cyclically. Due to the definition of WMGs, all the places that we have to consider are of the form schematised in Fig. 6. The arc weights may differ due to the integer parameter l ≥ 1, but the ratio WW((ap,ap,ba,,bb)) = mn is determined by the Parikh vector of w and its cyclical solvability (let us notice that the initial marking is to be defined). Moreover, we have to consider only these places, which are connected to the pairs of adjacent transitions in w. Indeed, if w = u1 |si a |si+1 b u2, where si is the state reached after performing u1 and si+1 is the state reached after performing u1a, then any place that solves the ESSP7 ¬Mi[bi is an input place for b. On the other hand, any place whose marking at Msi differs from its marking at Msi+1 is connected to a. Hence, a place p ∈ P solving ¬Mi[bi is of the form pa,b. Since p is only affected by a and b, it also disables b at all the states between sl and si in w when it is of the form w = u3 |sj tj |sj+1 b+ |sl u4 |si abu2 with P(u4)(b) = 0 (in the case there is no b in the prefix between s0 and abu2, sl = s0). Analogously, if tj 6= b, there must be a place q ∈ P of the form ptj,b that solves ¬Msj [bi. Doing so, we ascertain that the places of the form schematised in Fig. 6 for the adjacent pairs of transitions are sufficient to handle all the ESSPs. 7 Assuming b 6= a. l · m l · n
b pa,b
In fact, for every pair of adjacent transitions a and b in w, a single place of the form pa,b is sufficient. Indeed, assume there are p1, p2 ∈ P of the form pa,b.
M0(p1) M0(p2) If gcd(W (a,p1),W (p1,b)) ≥ gcd(W (a,p2),W (p2,b)) then for any M ∈ [M0i, M (p1) < W (p1, b) implies M (p2) < W (p2, b). Hence, p1 is redundant in the system, and the following is true.
Lemma 3. If w ∈ T ∗ is cyclically solvable by a WMG, there exists a WMG S = ((P, T, W ), M0), where P consists of places pa,b, for each pair of distinct circularly adjacent a and b (i.e., either w = u1abu2 or w = bu3a). Let w be cyclically solvable with a WMG S = ((P, T, W ), M0) as in Lemma 3, and place p ∈ P be of the form pa,b (as in Fig. 6, with l = 1) for an adjacent pair ab. Choose two successive ab’s in w = u1 |sr a |sr+1 b |sr+2 . . . |sq a |sq+1 b u2 with possibly other letters between sr+2 and sq (if there is only one ab, apply the argumentation while wrapping around w circularly, i.e., with sr = sq). Since p solves ESSPs ¬sr[bi and ¬sq[bi, the next inequalities hold true, where μr denotes the marking of pa,b at state sr: ∀j : r ≤ j ≤ q : ¬sr[bi : sr+1[bi : ¬sq[bi : μr μr + m μr + Prj (a) · m − Prj (b) · n μr + Prq(a) · m − Prq(b) · n < n ≥ n ≥ 0 < n From the first and the third line of (2) we get Prj (a) · m − Prj (b) · n > −n. This implies:
Prj (b) − 1 <
Prj (a) m
, r < j ≤ q. n From the third and the fourth line of (2) we obtain
(Prq(a) − Prj (a)) · m − (Prq(b) − Prj (b)) · n < n.
For Pjq(a) 6= 0, since Prq = Prj + Pjq this inequality can be written as Thus, from (3) and (4) we have a necessary condition for solvability in the following sense.
m n < (2) (3) (4) Lemma 4 (A necessary condition for cyclical solvability with a WMG). If w ∈ T ∗ is cyclically solvable by a WMG, then for any adjacent transitions a and b in w, and any two successive-up-to-rotation occurrences of ab in w = u1 |sr a b . . . |sq a b u2, the inequality
Prj (b) − 1
Prj (a) < m n < holds true, where m, n are as in (1), r < j ≤ q, and the right inequality is omitted when Pjq(a) = 0. In particular, Lemma 4 explains the cyclical unsolvability of the word w3 = |sr ab c b |sj a d |sq ab d. Indeed, P(w3)(b) = 3 = P(w3)(a), so that m/n = 1 and Lemma 5 (A sufficient condition for cyclical solvability by a WMG). If w ∈ T ∗ has a prime Parikh vector, and for each pair of circularly adjacent ab in w = . . . |q a b . . . , the inequality m n <
Proof: We have earlier proved (Lemma 2) that all SSPs are solvable for prime cycles. Let us now consider the ESSPs at states s as in w = . . . |sab . . ., i.e. ¬s[bi. Since we are looking for a WMG-solution, all the sought places are of the form pa,b (see Lemma 3 and Fig. 6) with m, n as in (1). To define the initial marking of pa,b, let us put n · P(w)(b) tokens on it and fire the sequence w once completely. Choose some state s0 in w = . . . |s0 a . . . such that the number k of tokens on pa,b at state s0 is minimal (it may be the case that such an s0 is not unique; we can choose any such state). Define M0(pa,b) = n · P(w)(b) − k as the initial marking of pa,b. By construction, the firing of w reproduces the markings of pa,b and M0 guarantees their non-negativity. Let us now demonstrate that the constructed place pa,b solves all the ESSPs ¬s[bi, where w = . . . |sab . . .. Consider such a state s in w (w.l.o.g. we assume s 6= s0, since s0 certainly disables b). From w = u1 |s0 a . . . |s a b u2, and from inequality (6) for sj = s0 we get Ps0s(a) · m − Ps0s(b) · n < n. Since Ms0 (pa,b) = 0, Ms(pa,b) = Ms0 (pa,b) + Ps0s(a) · m − Ps0s(b) · n < n, i.e., pa,b disables b at state s.
Now, we show that places of the form pa,b also solve the other ESSPs against b, i.e., at the states where b is not the subsequent transition. Sequence w (up to rotation) can be written as w = u1 bx1 u2 bx2 . . . ul bxl , 1 ≤ l ≤ P(w)(b), and for 1 ≤ i ≤ l: xi > 0, ui ∈ (T \ {b})+. Transition b has to be deactivated at all the states between neighbouring b-blocks. Consider an arbitrary pair of such blocks bxj and bxj+1 in w = . . . bxj uj bxj+1 . . . = . . . bxj |s u0j |r t bxj+1 . . ., with uj = u0j t. Place pt,b does not allow b to fire at state r. We have to check (5) (6) that b is not activated at any state between s and r, i.e., it is not activated ‘inside’ u0j . If u0j is empty, then s = r, and we are done. Let u0j 6= ε. Due to P(u0j )(b) = P(uj )(b) = 0, the marking of place pt,b cannot decrease from s to r, i.e., Ms(pt,b) ≤ Ms00 (pt,b) ≤ Mr(pt,b) for any s00 ‘inside’ u0j . Since pt,b deactivates b at r, it then deactivates b at all states between s and r, inclusively. tu From Lemma 4 and Lemma 5 we can deduce the following characterisation. Theorem 4 (A characterisation of cyclical solvability with a WMG). A sequence w ∈ T ∗ is cyclically solvable with a WMG iff P(w) is prime and for any pair of circularly adjacent labels in w, for instance w = . . . |q ab . . ., m n < holds true with m, n as in (1). A WMG-solution can be found with the places of the form pa,b for every such pair of a and b.
Based on the characterisation from Theorem 4 and the considerations above,
Algorithm 1 below synthesizes a cyclical WMG-solution for a given sequence w ∈
T ∗, if one exists, with a runtime in O(|w|2). For a comparison, the general
regionbased synthesis typically uses ILP-solvers, and for Karmarkar’s algorithm [
CF-solvability vs WMG-solvability of Cycles The class of WMGs is clearly a proper subset of the class of CF nets. If we are only looking at cyclical solvability of sequences, this inclusion remains strict, i.e., there exist sequences which are cyclically solvable by a CF net but have no cyclical solution in the form of a WMG. E.g., the sequence w = abcbad has a cyclical CF-solution (cf. Fig. 7). On the other hand, for a |r b c |q b a d we have PP((ww))((ab)) = 22 ≮ 0+1 = Prq(a)+1 which, by Theorem 3, implies the cyclical 1 Prq(b) unsolvability of w by a WMG.
From Lemma 3, for the cyclical solvability by a WMG it is enough to use only
places between adjacent transitions. For the sequence abcbad in Fig. 7, transition
b follows a and c, and the input place of b in the CF-solution is an output place
for both a and c. The situation is similar for transition a, which follows b and d.
However, this is not always the case when we are looking for a solution in the
class of CF nets. For instance, the sequence cabdaaabeab is cyclically solvable
by a CF net (see Fig. 8). In this sequence, b always follows a. But in order to
solve ESSPs against b, we need a place which is an output place for c and e (in
addition to a).
Algorithm 1: WMG-cycles
input : w ∈ T ∗, T = {t0, . . . , tn−1}
output: A WMG N cyclically solving w if it exists
var: T [0 .. |T | − 1] = (t0, . . . , tn−1), v[0 .. |w| − 1], a, b, na, nb, ia, ib, M , M min;
compute the Parikh-vector P[0 .. |T | − 1] of w;
if P is not prime then return unsolvable ; // Parikh-primeness
b ← w[0];
for j = 0 to |T | − 1 do // index of b
if b = T [j] then ib ← j ;
for i = 0 to |w| − 1 do
v ← w[i] . . . w[|w| − 1]w[0] . . . w[i − 1] ;
a ← b, b ← v[
if b = T [j] then ib ← j ; na ← 1, nb ← 1 ; if a 6= b then for k = 2 to |w| − 1 do if PP[[iiab]] ≥ PP[i[bi]a−]−nbn+a1 then
return unsolvable ; if v[k] = T [ia] then na ← na + 1 ; if v[k] = T [ib] then nb ← nb + 1 ; M ← P[ia] · P[ib], M min ← M ; for k = 0 to |w| − 1 do if w[k] = a then M ← M + P[ib] ; if w[k] = b then M ← M − P[ia] ; if M < M min then M min ← M ; add new place pT [ia],T [ib] to N with
W (T [ia], p) = P[ib], W (p, T [ib]) = P[ia], M0 = P[ia] · P[ib] − M min; return N // rotation of w // fix first adjacent pair // check solvability condition
// find initial marking a d b a c b b 3 2 2 a 3 2 d
2 c 2
2 3 d e 3 2 a 2 c Indeed, if there is a place pa,b as on the left of Fig. 9 which solves ESSPs against b, then for ca |s bdaa |q abeab s[bi
: μ0 + 3 ¬q[bi : μ0 + 3 · 3 − 5 ≥ 5 < 5 Subtracting the first inequality from the second one, we get 6 − 5 < 0, which is a contradiction. Hence, a place of form pa,b cannot solve all ESSPs against b in cabdaaabeab.
a 3 5
b μ0 pa,b μ0 p k
a b f d c e
kc kb kd ke kf In a WMG, a place can have at most one input transition. This restriction is relaxed for choice-free nets and multiple inputs are allowed. Nevertheless, this does not imply that a single input place for each transition will always be sufficient. As an instance, consider the sequence bcaf deaaabcdaaf dcaaa (see Fig. 10) which is cyclically solvable with a CF net.
Assume that we can solve all ESSPs against transition a with a single place p as on the right of Fig. 9 (we know that we do not need any side-conditions). Then, for p and w = |s0 b c a f d |s5 e |s6 a a a b c |s11 d |s12 a a f d |s16 c |s17 a a a, the a c a a a f d e c d f a a a a a d b c f 9 2 a 2 10 following system of inequalities must hold true: cycle ¬s5[ai s6[aaai ¬s11[ai s12[aai ¬s16[ai : 2 · kb + 3 · kc + 3 · kd + ke + 2 · kf : μ0 + kb + kc + kd + kf − k : μ0 + kb + kc + kd + ke + kf − k : μ0 + 2 · kb + 2 · kc + kd + ke + kf − 4 · k : μ0 + 2 · kb + 2 · kc + 2 · kd + ke + kf − 4 · k : μ0 + 2 · kb + 2 · kc + 3 · kd + ke + 2 · kf − 6 · k s17[aaai : μ0 + 2 · kb + 3 · kc + 3 · kd + ke + 2 · kf − 6 · k = 9 · k (0) < k (1) ≥ 3 · k (2) < k (3) ≥ 2 · k (4) < k (5) ≥ 3 · k (6) From the system above we obtain: (2) − (1) : ke (4) − (3) : kd (6) − (5) : kc > 2 · k > k > 2 · k which implies 3 · kc + 3 · kd + ke > 13 · k, contradicting the equality (0). Hence, the ESSPs against a cannot be solved by a single place. 5
In this work, we specialised previous methods of analysis and synthesis to the CF nets and their WMG subclass, two useful subclasses of weighted Petri nets allowing to model various real-world applications. We highlighted the correspondance between CF-solvability and WMG-solvability for binary alphabets. We also tackled the case of an LTS formed of a single circuit with an arbitrary number of letters, for which we developed a characterisation of WMG-solvability together with a dedicated and efficient synthesis algorithm. Finally, we discussed the applicability of our conditions to CF synthesis. As a natural continuation of the work, we expect extensions of our results in two directions: generalising the class of goal-nets (e.g. to choice-free or forkattribution nets), and relaxing the restrictions for the LTS under consideration.
We would like to thank the anonymous referees for their useful suggestions.