On Binary Words Being Petri Net Solvable Kamila Barylska1,2?† , Eike Best1∗,?? , Evgeny Erofeev1? ? ? , Lukasz Mikulski2† , Marcin Pia,tkowski2† 1 Department of Comp. Sci., Carl von Ossietzky Univ. Oldenburg, Germany {eike.best,evgeny.erofeev}@informatik.uni-oldenburg.de 2 Faculty of Math. and Comp. Sci., Nicolaus Copernicus University Toruń, Poland {kamila.barylska,lukasz.mikulski,marcin.piatkowski}@mat.umk.pl Abstract. A finite word is called Petri net solvable if it is isomorphic to the reachability graph of some unlabelled Petri net. In this paper, the class of two-letter Petri net solvable words is studied. Keywords: Binary words, labelled transition systems, Petri nets, syn- thesis 1 Introduction Region theory [1] provides a polynomial algorithm, based on solving linear inequations, that checks whether a given finite labelled transition system is the reachability graph of some place/transition Petri net [5], and if it is, synthesises one of them. Due to the size of a transition system, this algorithm may be very time-consuming. Moreover, it may produce one out of a class of different nets, and there may not be a unique simplest one. For some applications, only certain types of labelled transition systems are relevant. This leads to the idea of investigating properties of labelled transition systems before synthesising them, in the hope of obtaining more efficient and possibly also more deterministic synthesis algorithms. It may even be possible to find exact structural characterisations, based solely on graph-theoretical properties, such as for the class of finite labelled transition systems which correspond to T-systems [2]. This paper reports progress on a similar effort about characterising the set of finite words over an alphabet {a, b} which are Petri net solvable, i.e., for which a place/transition net with an isomorphic reachability graph exists. We shall put forward two conjectures, and describe some progress in analysing them. This ? Supported by a research and a visiting fellowship within the project ”Enhancing Educational Potential of Nicolaus Copernicus University in the Disciplines of Mathe- matical and Natural Sciences” (project no. POKL.04.01.01-00-081/10) ?? Supported by the German Research Foundation through the DFG/RFBR cooperation project CAVER, BE 1267/14-1 ??? Supported by the German Research Foundation through the Research Training Group (DFG GRK 1765) SCARE – http://www.uni-oldenburg.de/en/scare/ † Supported by the National Science Center under grant no. 2013/09/D/ST6/03928 1 work could well be of interest in a wider context, as it might entail a nontrivial necessary condition for the solvability of an arbitrary labelled transition system. If the latter is solvable, then finding a PN-unsolvable word as a path in it may have a strong impact on its structure / shape. 2 Basic notations and conventions used in this paper A finite labelled transition system with initial state is a tuple T S = (S, →, T, s0 ) with nodes S (a finite set of states), edge labels T , edges →⊆ (S × T × S), and an initial state s0 ∈ S. A label t is enabled at s ∈ S, written formally as s[ti, if ∃s0 ∈ S : (s, t, s0 ) ∈→. A state s0 is reachable from s through the execution of σ ∈ T ∗ , denoted by s[σis0 , if there is a directed path from s to s0 whose edges are labelled consecutively by σ. The set of states reachable from s is denoted by [si. A (firing) sequence σ ∈ T ∗ is allowed from a state s, denoted by s[σi, if there is some state s0 such that s[σis0 . Two lts T S1 = (S1 , →1 , T, s01 ) and T S2 = (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 . A word over T is a sequence w ∈ T ∗ , and it is binary if |T | = 2. A word t1 t2 . . . tn of length n ∈ N uniquely corresponds to a finite transition system ({0, . . . , n}, {(i − 1, ti , i) | 0 < i ≤ n ∧ ti ∈ T }, T, 0). An initially marked Petri net is denoted as N = (P, T, F, M0 ) where P is a finite set of places, T is a finite set of transitions, F is the flow function F : ((P × T ) ∪ (T × P )) → N specifying the arc weights, and M0 is the initial marking (where a marking is a mapping M : P → N, indicating the number of tokens in each place). A side-place is a place p with p• ∩• p = 6 ∅, where p• = {t ∈ T | F (p, t)>0} • and p = {t ∈ T | F (t, p)>0}. N is pure or side-place free if it has no side- places. A transition t ∈ T is enabled at a marking M , denoted by M [ti, if ∀p ∈ P : M (p) ≥ F (p, t). The firing of t leads from M to M 0 , denoted by M [tiM 0 , if M [ti and M 0 (p) = M (p) − F (p, t) + F (t, p). This can be extended, as usual, to M [σiM 0 for sequences σ ∈ T ∗ , and [M i denotes the set of markings reachable from M . The reachability graph RG(N ) of a bounded (such that the number of tokens in each place does not exceed a certain finite number) Petri net N is the labelled transition system with the set of vertices [M0 i, initial state M0 , label set T , and set of edges {(M, t, M 0 ) | M, M 0 ∈ [M0 i ∧ M [tiM 0 }. If an lts T S is isomorphic to the reachability graph of a Petri net N , we say that N solves T S. 3 Separation problems, and an example In region theory, a labelled transition system (S, →, T, s0 ) is assumed to be given as an input. In order to synthesise (if possible) a Petri net with isomorphic reacha- bility graph, T is used as the set of transitions, and for the places, 12 ·(|S|·(|S|−1)) state separation problems and up to |S|·|T | event/state separation problems have 2 to be solved. A state separation problem consists of a set of states {s, s0 } with s 6= s0 , and for each such set, one needs a place that distinguishes them. Such problems are always solvable for words; for instance, we might introduce a count- ing place which simply has j tokens in state j. An event/state separation problem consists of a pair (s, t) ∈ S×T with ¬(s[ti). For every such problem, we need a place p such that M (p) < F (p, t) for the marking M corresponding to state s, where F refers to the arcs of the hoped-for net. T S2 0 5 N1 w = abbaa a a T S1 w = aab q p 1 4 0 a 1 a 2 b 3 2 b a b a 2 3 b Fig. 1. N1 solves T S1 . No solution of T S2 exists. For example, in figure 1, the labelled transition systems T S1 and T S2 correspond to the words aab and abbaa, respectively. The former is PN-solvable, since the reachability graph of N1 is isomorphic to T S1 . T S2 contains an unsolvable event/state separation problem. The state s = 2 just between the two b’s satisfies ¬(s[ai). We need a place q whose number of tokens in (the marking corresponding to) state 2 is less than needed for transition a to be enabled. Such a place q has the general form shown on the right-hand side of figure 2. It is useful to speak of the effect E(τ ) of a sequence τ ∈ T ∗ on place q. For the letter a, the effect is defined as E(a) = (a+ −a− ), and this can be generalised easily. Thus, for instance, the effect E(abbaa) is E(abbaa) = 3·(a+ − a− ) + 2·(b+ − b− ). If q prevents a at state 2 in abbaa, then it must satisfy the following inequalities, amongst others: a− ≤ m, since a is enabled initially; a− ≤ m + E(abba), since state 4 enables a; and m + E(ab) < a− , or equivalently, 0 ≤ −m − E(ab) + a− − 1, expressing the fact that q solves the event/state separation problem ¬(2[ai). Later, we show that this set of inequalities cannot be solved in the natural numbers. a+ b+ a+ b+ a m b a m b a− p b− a− q b− Fig. 2. Places p / q with four arc weights a− , a+ , b− , b+ and initial marking m. They are similar, but p will be used for preventing b, and q for preventing a. In a word of length n, the equation system for a single event/state separation problem comprises n + 1 inequations. In binary words, we have n + 2 such problems, one for every state 0, . . . , n − 1 and two for the last state. Thus, a word w of length n is PN-solvable if and only if all those n + 2 systems, each having n + 1 inequalities and five unknowns a− , a+ , b− , b+ , m, are solvable in N. The question dealt with in this paper is whether the set of binary words that are PN-(un)solvable can be characterised equivalently, in a more structural way. We shall assume, from now on, that T = {a, b}. 3 4 Minimal unsolvable binary words, and some conjectures Let a word w0 ∈ T ∗ be called a subword (or factor) of w ∈ T ∗ if ∃(u1 , u2 ∈ T ∗ ) : w = u1 w0 u2 , and let #t (w) denote the number of times the letter t occurs in w. Observe that if w is PN-solvable then all its subwords are, too. To see this, let the Petri net solving w be executed up to the state before w0 , take this as the new initial marking, and add a pre-place with #a (w0 ) tokens to a and a pre-place with #b (w0 ) tokens to b. Thus, if a subword of w is unsolvable, then w is. For this reason, the notion of a minimal unsolvable word is well-defined (namely, as an unsolvable word all of whose subwords are solvable). A complete list of minimal unsolvable words up to length 110 can be found in [6]. As a consequence of the next proposition, any minimal unsolvable word either starts and ends with a or starts and ends with b. Proposition 1. Solvability of aw and wb implies solvability of awb If both aw and wb are solvable, then awb is also solvable. Proof: Assume that aw and wb are PN-solvable words over {a, b}. If w = bk (for k ∈ N) then awb = abk+1 is obviuosly solvable, hence we assume that b contains at least one a. Let N1 = (P1 , {a, b}, F1 , M01 ) and N2 = (P2 , {a, b}, F2 , M02 ) be Petri nets such that N1 solves aw and N2 solves wb. We can assume that N1 and N2 are disjoint, except for their transitions a and b. Forming the union of N1 and N2 gives a net which is synchronised at a and b, and which allows all (and only) sequences allowed by both N1 and N2 . We modify N1 and N2 before forming their union, as follows: (i) Modify N1 by adding, to each place p in • b ∩ P1 , another F1 (p, b) tokens. This allows an additional b. (ii) Modify N2 by adding, to each place q in • a ∩ P2 , another F2 (q, a) tokens. This allows an additional a. Further, for each place p in a• ∩ P2 ∩ • b, add the quantity F2 (a, p) both to F2 (p, b) and to F2 (b, p). The new arc weights lead to the same effect of b on p, but prevent premature occurrences of b which could have been allowed by adding the tokens in front of b in step (i). Define N as the union of the two nets thus modified, and see figure 3 for an example. (The added tokens are drawn as hollow circles.) In general, N solves awb in the following way: The initial a is allowed in N1 by definition and in N2 by the additional tokens. The subsequent w is allowed in both nets, and hence in their synchronisation. The final b is allowed in N2 by definition and in N1 by the additional tokens. No premature b is allowed by the arc weight increase, and no final additional a is allowed because N1 does not allow it. 1 ¿From the list [6], it can be observed that all minimal unsolvable words starting and ending with a are of the following general form: s0 [ (abα) b∗ i s [ (baα)+ i r [ a i where α ∈ T ∗ and s0 , s, r are states (1) 4 ◦ • • 3 2 p 2 p 2 a • b a ◦ b a • b •• •◦ •• N1 N2 N Fig. 3. N1 (black tokens) solves aw = abab. N2 (black tokens) solves wb = babb. N (redundant places omitted) solves awb = ababb. with a not being separated at s. For example, abbaa satisfies (1) with α = ε, the star ∗ being repeated zero times, and the plus + being repeated just once. Indeed, it is easy to prove that such words are generally PN-unsolvable: Proposition 2. Sufficient condition for the unsolvability of a word If a word over {a, b} has a subword of the form (1), then it is not PN-solvable. Proof: For a word w of the form (1), we prove that w cannot be solved (implying the proposition in the context of the considerations above). Because baα occurs at least once after state s, b is enabled at s, and a is not enabled at s. Suppose that some place q as in figure 2 (r.h.s.) exists which separates a at s. Let E be E(abα), i.e., the effect of abα on q, and let Eb = E(b). E(b) ≥ 1 because q separates a at s but not at s + 1. For w, we derive the following inequalities: (0) a− ≤ m (s+1) a− ≤ m + E + k·Eb + Eb for some fixed k ≥ 0 (r) a− ≤ m + E + k·Eb + `·E for the same k and some fixed ` > 0 (sep) 0 ≤ −m − E − k·Eb + a− − 1 for the same k (0) is true because at s0 , a is enabled. (s+1) is true because a is enabled one state after s. (r) is true because a is enabled at r; and ` > 0 because of the + . Finally, (sep) is true because q disables a at state s. Adding (s+1)+(sep) gives 1 ≤ Eb . Adding (0)+(sep) gives 1 ≤ −E − k·Eb , and using also 1 ≤ Eb gives 1 ≤ −E − k·Eb ≤ −E. Adding (r)+(sep) gives 1 ≤ `·E, contradicting 1 ≤ −E. The system cannot be solved, and no place q separating a at s exists. 2 Conjecture 1. A converse of proposition 2 Suppose a word over {a, b} is non-PN-solvable and minimal with that property. Then it is (modulo swapping a and b) of the form given in (1). Strengthened bj bk ba |{z} conjecture: It is either of the form ab |{z} bj a with j ≥ 0, k ≥ 1 or of the α α form abα(baα)` a with ` ≥ 1 Conj. 1 Proposition 3. Another sufficient condition for unsolvability Let w be of the form s0 [αis[βir[ai such that α starts with a and β starts with b. If #a (β)·#b (α) ≥ #a (α)·#b (β) (2) then w is unsolvable. For instance, for w = abbaa, α = ab and β = ba, and (2) holds true. 5 Proof: If a place q separates a at s and has marking m at s0 , then for Eα = E(α) = #a (α)·Ea + #b (α)·Eb and Eβ = E(β) = #a (β)·Ea + #b (β)·Eb we have: (0) a− ≤ m (since α starts with a) (r) a− ≤ m + Eα + Eβ (sep) 0 ≤ −m − Eα + a− − 1 (since ¬s[ai) Adding (0)+(sep) yields 1 ≤ −Eα , hence (A): −(#a (α)Ea +#b (α)Eb ) ≥ 1, where Ea and Eb denote the effects of a and b on q, respectively. As before, Eb ≥ 1. Adding (r)+(sep) yields 1 ≤ Eβ , hence (B): (#a (β)Ea + #b (β)Eb ) ≥ 1. Then, −#a (β) ≥ #a (β)#a (α)Ea + #a (β)#b (α)Eb (algebra, and by (A)) ≥ #a (β)#a (α)Ea + #a (α)#b (β)Eb (using (2) and Eb ≥ 1) ≥ #a (α) (algebra, and by (B)) However, −#a (β) ≥ #a (α) implies #a (β) = #a (α) = 0, and this is a contradic- tion since α contains at least one a. Thus, such a place q does not exist. 3 Words in which the letters a and b strictly alternate are easy to solve. Therefore, it stands to reason to investigate cases in which a letter occurs twice in a row. Proposition 4. Solvable words starting with a can be prefixed by a If a word av is PN-solvable then aav is, too. Proof: Let N = (P, {a, b}, F, M0 ) be a net solving av. We shall construct a net which solves aav. The idea is to obtain such a net by “unfiring” a once from the initial marking of N . Since this may lead to a non-semipositive marking which we would like to avoid, we will first normalise and modify the net N , obtaining another solution N 0 of av, and then construct a solution N 00 for aav (cf. Fig. 4). For normalisation, we assume that there are two places pb and qa ; the first prevents b explicitly in the initial phase, and the second prevents a after the last occurrence of a. They are defined by M0 (pb ) = 1, F (a, pb ) = 1, F (b, pb ) = `+1 = F (pb , b), where ` is the number of a before the first b in av, and M0 (qa ) = k, F (qa , a) = 1, where k is the number of a in av. (All other F values = 0.) Let NUF (a) = {p ∈ a• | M0 (p) < F (a, p)} be the set of places which do not allow the “unfiring” of a at M0 . Note that neither pb nor qa are in NUF (a). Note also that for every p ∈ NUF (a), F (p, a) ≤ M0 (p) < F (a, p) – the first because a is initially enabled, the second by p ∈ NUF (a). That is, a has a positive effect on p. Without loss of generality, b has a negative effect on p (otherwise, thanks to the normalising place pb , p could be deleted without changing the behaviour of N ). For every p ∈ NUF (a) we add the quantity F (a, p) uniformly to M0 (p), to F (p, b), and to F (b, p), eventually obtaining N 0 = (P 0 , {a, b}, F 0 , M00 ), and we show that N 0 also solves av. First, both M0 [ai ∧ ¬M0 [bi and M00 [ai ∧ ¬M00 [bi (the former by definition, the latter by construction). For an inductive proof, suppose that M0 [aiM1 [τ iM and M00 [aiM10 [τ iM 0 . We have M [bi iff M 0 [bi by construction. If 6 M [ai, then also M 0 [ai, since M ≤ M 0 . Next, suppose that ¬M [ai; then there is some place q such that M (q) < F (q, a). We show that, without loss of generality, q∈/ NUF (a), so that q also disables a at M 0 in N 0 . If M disables the last a in av, we can take q = qa ∈ / NUF (a). If M disables some a which is not the last one in av, then q cannot be in NUF (a), since b acts negatively on such places. Now, we construct a net N 00 = (P 0 , {a, b}, F 0 , M000 ) from N 0 by defining M000 (p) = M00 (p) − F 0 (a, p) + F 0 (p, a) for every place p. By construction, aav is a firing sequence of N 00 . Furthermore, M000 does not enable b because of pb . 4 p p p • 2 2 a • b a • b a •• b 2 2 2 •• • 2 •• • 2 •• • 2 qa pb N qa pb N0 qa pb N 00 Fig. 4. N is normalised and solves abab. N 0 solves abab as well. N 00 solves aabab. As a consequence, if av is minimally PN-unsolvable, then v starts with a b. Proposition 5. No aa and bb inside a minimal unsolvable word If a minimal non-PN-solvable word is of the form u = aαa, then either α does not contain the factor aa or α does not contain the factor bb. Proof: By contraposition. Assume that α contains a factor aa and a factor bb. Two cases are possible: Case 1: There is a group of a’s which goes after a group of b’s. Let am and bn be such groups, assume that am goes after bn and that there are no groups of a or of b between them. Then u is of the following form s0 [ . . . i q [ abn (ab)k am i r [ . . . i where n, m ≥ 2, k ≥ 0. Recombine the letters in u to the following form: s0 [ . . . i q [ (ab)bn−2 (ba)k+1 aam−2 i r [ . . . i Since u ends with a, (ab)bn−2 (ba)k+1 a is a proper subword of u. But it has the form (abw)b∗ (baw)+ a, with w = ε, which implies its unsolvability by proposition 2, contradicting the minimality of u. Case 2: All groups of a precede all groups of b. In this case u is of the form aax0 bax1 . . . baxn by0 aby1 aby2 . . . abym a where at least one of xi and one of yj is greater than 1. Consider ` = max{i | xi > 1}. If ` = 0, we get a contradiction to proposition 4. Hence, ` > 0. Let t = min{j | yj > 1}. Then u has the form s0 [ a . . . i q [ bax` (ba)n−` (ba)t byt i r [ . . . a i 7 Recombine the letters in u to the form s0 [ a . . . i q [ (ba)ax` −2 (ab)n−`+t+1 bbyt −2 i r [ . . . a i Hence, u has a proper subword (ba)ax` −2 (ab)n−`+t+1 b, which is of the form (baw)a∗ (abw)+ b with w = ε, implying its non-P N -solvability, due to proposition 2 with inverted a and b. This again contradicts the minimality of u. 5 For these reasons, we are particularly interested in words of the following form: either abx1 a . . . abxn a or bx1 a . . . abxn where xi ≥ 1 and n > 1 (3) In the first form, there are no factors aa. If factors bb are excluded and the word starts and ends with an a, then we get words that are of the second form, except for swapping a and b. This swapping is useful in order to understand how words of the two forms are interrelated. Conjecture 2. A converse of proposition 3 If a word is of the form w = αβa where α starts with a and β starts with b, and if w is minimal non-PN-solvable and also of the form given in (3), then inequation (2) holds. A stronger variant of this conjecture: If w = αβa is of the form w = [ abx1 . . abxk −1} i s [ |ba . .{z | a . {z . abxn} a i with n ≥ 3 and xi ≥ 1 α β then a is not separated at state s iff #a (β)·#b (α) = #a (α)·#b (β). Conj. 2 5 Some results about words of the form bx1 a . . . abxn 5.1 Side-places in words of the form bx1 a . . . abxn If a word w = bx1 a . . . abxn can be solved at all, then side-places may be necessary to do it. However, we will show that in the worst case, only some side-place q around a, preventing a at some state, are necessary. Lemma 1. side-place-freeness around b If w = bx1 a . . . abxn is solvable, then w is solvable without side-place around b. Proof: Let w and its intermediate states be of the form1 w = s0 [bx1 is1 [abx2 is2 [ai . . . sn−1 [abxn isn (4) Suppose some place p prevents b at some state sk , for 1 ≤ k ≤ n − 1. (The only other state at which b must be prevented is state sn , but that can clearly be done 1 A note on convention: in the following, we use the letter s to denote states at which b has to be prevented, and p for places doing this. Similarly, we use the letter r to denote states at which a has to be prevented, and q for places doing this. 8 by Pna non-side-place, e.g. by an incoming place of transition b that has initially i=1 xi tokens.) Note that b− > b+ , because place p allows b to be enabled at the state preceding sk but not at sk . Similarly, a− < a+ , because b is not enabled at state sk but at the immediately following state, which is reached after firing a. ¿From the form (4) of w, we have b+ ≤ m + x1 (b+ − b− ) b+ ≤ m + (x1 + x2 )(b+ − b− ) + (a+ − a− ) ··· (5) b+ ≤ m + (x1 + . . . + xn )(b+ − b− ) + (n − 1)(a+ − a− ) 0 ≤ −m − (x1 + . . . + xk )(b+ − b− ) − (k − 1)(a+ − a− ) + b− − 1 The first n inequations assert the semipositivity of the marking of place p (more precisely, its boundedness from below by b+ , since p may be a side-place) at the n states s1 , . . . , sn . In our context, if these inequalities are fullfilled, then the marking is ≥ b+ at all states, as a consequence of b− ≥ b+ , a− ≤ a+ , and the special form of the word. The last inequality comes from ¬(sk [bi). We certainly have 0 ≤ b+ ≤ b− ≤ m, because of b− ≥ b+ as noted above, and because b is initially enabled. If b+ = 0, then p is not a side-place around b, and there is nothing more to prove (for p). If b+ ≥ 1, we consider the transformation b0+ = b+ − 1 and b0− = b− − 1 and m0 = m − 1 The relation 0 ≤ b0+ ≤ b0− ≤ m0 still holds for the new values. Also, all inequalities in (5) remain true for the new values: in the first n lines, 1 is subtracted on each side, and on the last line, the increase in −m is offset by the decrease in b− . Thus, we get a solution preventing b with a ‘smaller’ side-place, and we can continue until eventually b+ becomes zero. A side-place around b might, however, still be necessary to prevent a at some state. We show next that such side-places are also unnecessary. Let w and its intermediate states be of the form [bx1 −1 ir1 [b a bx2 −1 ir2 [b a i . . . [ a bxk −1 irk [bisk [ a i . . . [bxn−1 −1 irn−1 [b a bxn i Suppose some place q as on the right-hand side of figure 2 prevents a at state rk , for 1 ≤ k ≤ n − 1. Symmetrically to the previous case, we have b+ > b− . This is true because, while q does not have enough tokens to enable a at state rk , it must have enough tokens to enable a at the directly following state (which we may continue to call sk ). But we also have (w.l.o.g.) a+ < a− . For k ≥ 2, this follows from the fact that if the previous a (enabled at the state sk−1 just after rk−1 ) acts positively on q, then q also has sufficiently many tokens to enable a at state rk . For k = 1, it is possible to argue that a+ ≤ a− is valid without loss of generality. For suppose that q disables a only at r1 and nowhere else. (This is no loss of generality because for the other states rk , k ≥ 2, copies of q can be used.) Then we may consider q 0 which is an exact copy of q, except that a+ = a− − 1 for q 0 . This place q 0 also disables a at state r1 (because it has the same marking as 9 q). Moreover, it does not disable a at any other state after r1 because it always has ≥ a− − 1 tokens, and after the next b, ≥ a− tokens, since b+ > b− . Because of b+ ≥ b− and a+ ≤ a− , q also prevents a at all prior states in the same group of b’s. Moreover, in the last (i.e. n’th) group of b’s, a can easily be prevented side-place-freely. For place q with initial marking m, we have a+ ≤ m + x1 (b+ − b− ) + (a+ − a− ) a+ ≤ m + (x1 + x2 )(b+ − b− ) + 2(a+ − a− ) ··· (6) a+ ≤ m + (x1 + . . . + xn−1 )(b+ − b− ) + (n − 1)(a+ − a− ) 0 ≤ −m − (x1 + . . . + xk − 1)(b+ − b− ) − (k − 1)(a+ − a− ) + a− − 1 The first n − 1 inequations assert the semipositivity of the marking of place q (more precisely, its boundedness from below by a+ , since q may be a side-place of a) at the n − 1 states r1 , . . . , rn−1 . If these inequalities are fullfilled, then the marking is ≥ a+ at all states after the first a, as a consequence of b+ ≥ b− and the special form of the word. The last inequality asserts that place q prevents transition a at state rk , hence effects the event/state separation of a at rk . If b− is already zero, place q is not a side-place of b. Otherwise, we may perform the transformation b0+ = b+ − 1 and b0− = b− − 1 and m0 = m because of b+ ≥ b− as noted above. The left-hand sides of the first n − 1 inequalities in (6) do not decrease, and neither do the right-hand sides. The same is true for the last inequality. 1 Lemma 2. Side-place-freeness around a, preventing b Suppose w = bx1 abx2 a . . . abxn . If w is solvable by a net in which some place p separates b, then we may w.l.o.g. assume that p is not a side-place around a. Proof: The equation system (5) is invariant under the transformation a0+ = a+ − 1 and a0− = a− − 1 and m0 = m as neither the left-hand sides nor the right-hand sides change their values. 2 If some place q prevents transition a, then a side-place q connected to a may be present. It may not always be possible to remove such a side-place. Consider, for instance, the word w = bbbabab. It is of the form (4), and any net solving bbbabab necessarily contains a side-place around transition a.2 The word bbabbababab can also not be solved without a side-place (but bbabbabab can). So far, no tight (weak) sufficient conditions for solvability, or solvability without side-places around a, are known. However, the next lemma shows that the presence of a side-place around a may be due to there being “many” initial b’s. That is, if x1 is “small enough”, then such a side-place is not necessary. 2 The reader is invited to use [7] in order to verify this claim; we will not include a proof in this paper for lack of space. 10 Lemma 3. Side-place-freeness around a, preventing a Suppose w = bx1 abx2 a . . . abxn . If x1 ≤ min{x2 , . . . , xn−1 } and if w is solvable by a net in which some place q prevents transition a at state rk with 1 ≤ k ≤ n, then we may w.l.o.g. assume that q is not a side-place around a. Proof: For preventing a at state rn , we only need a place with no input and output a (weight 1) which has n − 1 tokens initially. Suppose q prevents a at state rk , with 1 ≤ k ≤ n − 1. ¿From previous consider- ations, we know a+ < a− and b+ > b− , and we may assume, w.l.o.g., that q is not a side-place around b, i.e., that b− = 0. The initial marking m of q and the remaining arc weights a+ , a− , b+ satisfy the system of inequations (6), except that it is simplified by b− = 0. If a+ = 0, then q is already of the required form. For a+ > 0, we distinguish two cases. Case 1: m > 0 and a+ > 0. Then consider the transformation m0 = m − 1 and a0+ = a+ − 1 and a0− = a− − 1 By m > 0 and a− ≥ a+ > 0, we get new values m0 , a0+ , a0− ≥ 0. Moreover, (6) remains invariant under this transformation. So, q 0 serves the same purpose as q, and it has one incoming arc from a less than q. By repeating this procedure, we either get a place which serves the same purpose as q, or we hit Case 2. Case 2: m = 0 and a+ > 0. In this case, we consider the transformation m0 = m = 0 and a0+ = 0 and a0− = a− Such a transformation also guarantees m0 , a0+ , a0− ≥ 0. Also, the last line of (6) is clearly satisfied with these new values, since the value of its right-hand stays the same (for k = 1) or increases (for k > 1). To see that the first n − 1 lines of (6) are also true with the new values (and with b− = 0), and that we can, therefore, replace q by q 0 , we may argue as follows. At any marking m e reached along the execution of w, we have the following: m(q) e e 0) ≥ 0 ≥ m(q (7) These inequalities imply that the new place q 0 prevents a at rk , whenever the old one, q, does, and that, moreover, no occurrences of a are excluded by the place q 0 where they should not be prohibited. The first of the inequalities (7) holds because it holds initially (when m e = m, then m(q) e = m = m0 = m(qe 0 )), and because the effect of a before the transformation is (a+ − a− ), and after the transformation, it is (−a− ). In other words, a reduces the token count on q 0 more than it does so on q, while b has the same effect on q 0 as on q. To see the second inequality in (7), let x = min{x2 , . . . , xn−1 }. Then a− ≤ x1 · b+ ≤ x · b+ The first inequality follows because m = 0 and q has enough tokens after the first x1 occurrences of b in order to enable a. The second inequality follows from 11 x1 ≤ x. But then, since a only removes a− tokens from q 0 and the subsequent block of b’s puts at least x · b+ tokens back on q 0 , the marking on q 0 is always ≥ 0, up to and including the last block of b’s. 3 Corollary 1. Side-place-free solvability with few initial b’s If w = bx1 abx2 a . . . abxn is solvable, then side-places are necessary, at worst, between a and q, where q is some place preventing a at one of the states rk with 1 ≤ k < n − 1. If w = bx1 abx2 a . . . abxn is solvable and x1 ≤ min{x2 , . . . , xn−1 }, then w is solvable side-place-freely. 1 5.2 Solving words aw from words of the form w = bx1 a . . . abxn Solving a word of the form w = bx1 a . . . abxn side-place-freely allows us to draw some conclusion about prepending a letter a to it, as follows. Lemma 4. Preventing a in aw Suppose w = bx1 abx2 a . . . abxn is solvable side-place-freely. Then in aw, all oc- currences of a can be separated side-place-freely. Proof: In order to prevent a in w side-place-freely at any state rk , the system (6) has a solution with a+ = 0 and b− = 0 for any fixed 1 ≤ k ≤ n − 1. This refers to a pure input place q of a, which may or may not be an output place of b. In order to prevent a in aw side-place-freely, we need to consider the states rk as before (but shifted to the right by one index position, still just before the last b of the k’th group of b’s) and a correspondingly modified system as follows: 0 ≤ m0 + (x1 + . . . + xi ) · (b0+ ) + (i + 1) · (−a0− ) for all 0 ≤ i ≤ n − 1 (8) 0 ≤ −m0 − (x1 + . . . + xk − 1) · (b0+ ) − k · (−a0− ) + a0− − 1 where m0 , b0+ and a0− refer to a new pure place q 0 preventing a at state rk in aw. The line with i = 0 was added because m0 is required to be bounded from below and a must be enabled initially. (In (6), nonnegativity of m follows from the line with i = 1 and b being the first transition of w, which is no longer true in aw.) Consider the transformation m0 = m + a− and b0+ = b+ and a0− = a− These values satisfy (8), provided m, b+ and a− (together with a+ = 0 and b− = 0) satisfy (6). The line with i = 0 follows from m0 = m + a− ≥ 0. The other lines corresponding to i ≥ 1 reduce to the corresponding lines in (6), since the additional (−a− ) at the end of each line is offset by the additional (+a− ) at the beginning of the line. The last line (which belongs to state rk at which a is separated) corresponds to the last line of (6), because the decrease by a− at the beginning of the line is offset by an increase by a− in the term k · (−a0− ) (compared with (k − 1) · (−a− ) as in (6)). 4 12 Note 1: In order to disable a at rk , q could be replaced by a place q 0 obtained by duplicating q and changing the initial marking m to m0 = m + a− . Intuitively, this means that m0 is computed from m by “unfiring” a once. Note 2: Place q should not be removed as soon as q 0 is added, because q could also be preventing a at some other rk . In that case, a new place q 00 must be computed from q for this different value of k. We may forget about q only after all the relevant indices k have been processed. Next, consider an input place p of b in a side-place-free solution of w and suppose that p prevents b at state sk . Suppose that we want to solve aw. If p is not also an output place of a, then it can simply be retained unchanged, and with the same marking, prevent b at corresponding states in aw and in w. However, if p is also an output place of a, there may be a problem, because “unfiring” a in the initial marking may lead to negative tokens on p. This is illustrated by the example babbabb which has a side-place-free solution, as shown on the left-hand side of figure 5. • −1 0 2 p 2 p 5 p0 3 a • b a •• b a •• b 2 2 • 2 • q1 q10 0 q10 0 q2 solves q q •• •• 2 “solves” •• 2 solves babbabb • ababbabb • ababbabb Fig. 5. Solving babbabb (l.h.s.), (almost) ababbabb (middle), and ababbabb (r.h.s.). The places q1 , q2 can be treated as in the above proof (that is, by chang- ing their markings by “unfiring” a) and yield new places q10 , q20 with marking {(q10 , 3), (q20 , 3)}. If we allowed negative markings, then a new place p0 with ini- tial marking (p0 , −1) (and otherwise duplicating p) would do the job of solving ababbabb (as in the middle of the figure). However, we shall need a more refined argument in order to avoid negative markings. Let p0 be a general new place which is supposed to prevent b at state sk in aw. In order to check the general solvability of aw if w is side-place-freely solvable, we consider a general transformation m0 = m+µ , b0+ = b+ +β+ , b0− = b− +β− , a0+ = a+ +α+ , a0− = a− +α− where µ ≥ −m, β+ ≥ −b+ , β− ≥ −b− , α+ ≥ −a+ and α− ≥ −a− , as well as a new inequation system: b0+ ≤ m0 + (x1 + . . . + xi ) · (b0+ − b0− ) + i · (a0+ − a0− ) for 1 ≤ i ≤ n 0 ≤ −m0 − (x1 + . . . + xk ) · (b0+ − b0− ) − k · (a0+ − a0− ) + b0− − 1 This system has to be compared with a restricted form of (5) (setting b+ = a− = 0, since the solution of w is pure). Doing this by line-wise comparison, we get the 13 following inequation system for the new value differences: µ ≥ −m, β+ ≥ −b+ , β− ≥ −b− , α+ ≥ −a+ , α− ≥ −a− β+ ≤ µ + (x1 + . . . + xi ) · (β+ − β− ) + i · (α+ − α− ) + a+ (9) 0 ≤ −µ − (x1 + . . . + xk ) · (β+ − β− ) − k · (α+ − α− ) − a+ + β− The lines with i must be solved simultaneously for every 1 ≤ i ≤ n while the line with k must be solved individually for every 1 ≤ k ≤ n − 1, in order to get a place preventing b at state sk . This leads to the following lemma. Lemma 5. Solving aw from w Suppose w = bx1 abx2 a . . . abxn is solvable side-place-freely. Then aw is solvable. Proof: Suppose that a pure place p with parameters b− (arc into b), a+ (arc from a) and m (initial marking) is given and suppose it separates b from sk in w. This place solves (5) for that particular k. We distinguish two cases: Case 1: a+ ≤ m. In this case, the place p can essentially be re-used for the same purpose in the solution (that we construct in this way) for aw, since (9) is solved by putting µ = −a+ , β+ = β− = 0 , α+ = α− = 0 Hence, a place p0 which differs from p only by its initial marking (m0 = m − a+ instead of m) separates b at sk in aw. Case 2: a+ > m. In this case, (9) can be solved by µ = −m , β+ = β− = a+ − m , α+ = α− = 0 That is, we may replace p by a place p0 with zero initial marking and adding uniformly the value a+ − m to the incoming and outgoing arcs of b, creating a side-place around b. 5 For instance, in the solution of babbabb shown on the left-hand side of figure 5, the place p from a to b satisfies m=1, b− =1, b+ =0, a− =0 and a+ =2. (9) is solved by µ = −1, β− = 2, β+ = 0, α− = 0 and α+ = 3. Hence with m0 =m − 1, b0− =b− + 2, b0+ =b+ , a0− =a− and a0+ =a+ + 3, the net shown on the right-hand side of figure 5 is a pure solution of ababbabb. (Place p0 prevents b not only in states s1 and s2 but also in the initial state and in the final state.) There exist words such as w1 = bbbabab or w2 = bbabbababab, however, which can be solved but for which aw is not solvable. We have a converse of Lemma 5: Lemma 6. Solving w side-place-freely from aw If aw has a solution, then w has a side-place-free solution. 14 Proof: Suppose that aw has a solution in which some place q 0 , preventing a, has a side-place around a. Because q 0 prevents a, a0− > a0+ (unless it is the first a, but then we don’t need q 0 in solving w). Because a is enabled initially, m0 ≥ a0− . But then, the transformation a00− = a0− − a0+ , a00+ = 0, m00 = m0 − a0+ yields another place q 00 which is not a side-place around a but serves the same purpose as q 0 . The rest of the proof follows because the above transformations (removing side-places around b, or side-places around a which prevent b) do not introduce any new side-places around a. 6 Corollary 2. Side-place-free solvability of bx1 abx2 a . . . abxn w = bx1 abx2 a . . . abxn is solvable side-place-freely iff aw is solvable. 2 6 Concluding remarks If the characterisations of minimal Petri net solvable binary words proposed in this paper are valid, then the usual linear solver for detecting them can be replaced by a pattern-matching algorithm based on conjecture 1, or by a letter- counting algorithm based on conjecture 2. We have described a variety of results providing some insight into this class of words. There are several other facts about them which we did not have space to describe. For example, if a word is solvable side-place-freely, then so is the reverse word. Also, if a word is solvable, then it is solvable by places having exactly one outgoing transition. (This property is not shared by words with three or more letters, a counterexample being abcbaa.) Moreover, PN-solvable words are balanced in the following sense. Referring to w = bx1 abx2 a . . . abxn , call w balanced if there is some x such that xi ∈ {x, x + 1} for all 2 ≤ i ≤ n − 1. We can prove that if w = bx1 abx2 a . . . abxn is PN-solvable, then w is balanced, and moreover, xn ≤ x + 1. Presenting these, and other, properties of PN-solvability must however be left to future publications. Acknowledgements: We would like to thank Harro Wimmel and Uli Schlachter for valuable comments, and Uli for finding weird words (amongst them, abcbaa as mentioned in the conclusion) using [7, 3]. We thank also the anonymous reviewers for their remarks which allowed to improve the presentation of the paper. References 1. É. Badouel, P. Darondeau: Theory of Regions. In W. Reisig, G. Rozenberg (eds): Lectures on Petri Nets I: Basic Models. LNCS Vol. 1491, 529–586 (1998). 2. E. Best, R. Devillers: State Space Axioms for T-Systems. G. Lüttgen, F. Corradini (eds): Special volume on the occasion of Walter Vogler’s 60th birthday. Acta Informatica, Vol. 52(2-3), 133-152 (2015). 3. E. Best, U. Schlachter: Analysis of Petri Nets and Transition Systems. ICE’2015. 4. B. Caillaud: http://www.irisa.fr/s4/tools/synet/ 5. T. Murata: Petri Nets: Properties, Analysis and Applications. Proc. of the IEEE, Vol. 77(4), 541-580 (1989). 6. M. Pia,tkowski et al.: http://folco.mat.umk.pl/unsolvable-words (2015). 7. U. Schlachter et al.: https://github.com/CvO-Theory/apt (2013). 15