A nite 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.
Region theory [1] provides a polynomial algorithm, based on solving linear inequations, that checks whether a given nite 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 di erent 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 e cient and possibly also more deterministic synthesis algorithms. It may even be possible to nd exact structural characterisations, based solely on graph-theoretical properties, such as for the class of nite labelled transition systems which correspond to T-systems [2].
This paper reports progress on a similar e ort about characterising the set of nite words over an alphabet fa; bg 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 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 nding 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 nite labelled transition system with initial state is a tuple T S = (S; !; T; s0) with nodes S (a nite set of states), edge labels T , edges ! (S T S), and an initial state s0 2 S. A label t is enabled at s 2 S, written formally as s[ti, if 9s0 2 S : (s; t; s0) 2!. A state s0 is reachable from s through the execution of 2 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 ( ring) sequence 2 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) 2!1 , ( (s); t; (s0)) 2!2, for all s; s0 2 S1. A word over T is a sequence w 2 T , and it is binary if jT j = 2. A word t1t2 : : : tn of length n 2 N uniquely corresponds to a nite transition system (f0; : : : ; ng; f(i 1; ti; i) j 0 < i n ^ ti 2 T g; T; 0).
An initially marked Petri net is denoted as N = (P; T; F; M0) where P is a nite set of places, T is a nite set of transitions, F is the ow 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 = ft 2 T j F (p; t)>0g and p = ft 2 T j F (t; p)>0g. N is pure or side-place free if it has no sideplaces. A transition t 2 T is enabled at a marking M , denoted by M [ti, if 8p 2 P : M (p) F (p; t). The ring 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 2 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 nite number) Petri net N is the labelled transition system with the set of vertices [M0i, initial state M0, label set T , and set of edges f(M; t; M 0) j M; M 0 2 [M0i ^ M [tiM 0g. 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 reachability graph, T is used as the set of transitions, and for the places, 12 (jSj (jSj 1)) state separation problems and up to jSj jT j event/state separation problems have to be solved. A state separation problem consists of a set of states fs; s0g 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 counting place which simply has j tokens in state j. An event/state separation problem consists of a pair (s; t) 2 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 S1
w = aab 0 a 1 a 2 b 3
N1 q a p 2
b
For example, in gure 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 satis es :(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 gure 2. It is useful to speak of the e ect E( ) of a sequence 2 T on place q. For the letter a, the e ect is de ned as E(a) = (a+ a ), and this can be generalised easily. Thus, for instance, the e ect 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. 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 ve 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 = fa; bg.
Minimal unsolvable binary words, and some conjectures Let a word w0 2 T be called a subword (or factor) of w 2 T if 9(u1; u2 2 T ) : w = u1w0u2, 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-de ned (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.
If both aw and wb are solvable, then awb is also solvable.
Proof: Assume that aw and wb are PN-solvable words over fa; bg. If w = bk (for k 2 N) then awb = abk+1 is obviuosly solvable, hence we assume that b contains at least one a. Let N1 = (P1; fa; bg; F1; M01) and N2 = (P2; fa; bg; 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 e ect 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). De ne N as the union of the two nets thus modi ed, and see gure 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 de nition and in N2 by the additional tokens. The subsequent w is allowed in both nets, and hence in their synchronisation. The nal b is allowed in N2 by de nition and in N1 by the additional tokens. No premature b is allowed by the arc weight increase, and no nal 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
with a not being separated at s. For example, abbaa satis es (
If a word over fa; bg has a subword of the form (
(r) a (sep) 0 m m + E + k Eb + Eb m + E + k Eb + ` E m E k Eb + a for some xed k 0 for the same k and some xed ` > 0 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
Suppose a word over fa; bg is non-PN-solvable and minimal with that property.
Then it is (modulo swapping a and b) of the form given in (
1
Let w be of the form s0[ is[ ir[ai such that starts with a and starts with b.
If #a( ) #b( )
#a( ) #b( ) then w is unsolvable.
For instance, for w = abbaa,
= ab and
= ba, and (
Conj. 1
(
starts with a)
Adding (0)+(sep) yields 1 E , hence (A): (#a( )Ea + #b( )Eb) 1, where
Ea and Eb denote the e ects 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 (
If a word av is PN-solvable then aav is, too.
Proof: Let N = (P; fa; bg; F; M0) be a net solving av. We shall construct a net which solves aav. The idea is to obtain such a net by \un ring" 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 rst 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 rst prevents b explicitly in the initial phase, and the second prevents a after the last occurrence of a. They are de ned by M0(pb) = 1, F (a; pb) = 1, F (b; pb) = `+1 = F (pb; b), where ` is the number of a before the rst 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) = fp 2 a j M0(p) < F (a; p)g be the set of places which do not allow the \un ring" of a at M0. Note that neither pb nor qa are in NUF (a). Note also that for every p 2 NUF (a), F (p; a) M0(p) < F (a; p) { the rst because a is initially enabled, the second by p 2 NUF (a). That is, a has a positive e ect on p. Without loss of generality, b has a negative e ect on p (otherwise, thanks to the normalising place pb, p could be deleted without changing the behaviour of N ). For every p 2 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; fa; bg; 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 de nition, the latter by construction). For an inductive proof, suppose that M0[aiM1[ iM and M00 [aiM10 [ iM 0. We have M [bi i M 0[bi by construction. If 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 2= 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 2= 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; fa; bg; F 0; M000) from N 0 by de ning M000(p) = M00 (p) F 0(a; p) + F 0(p; a) for every place p. By construction, aav is a ring sequence of N 00. Furthermore, M000 does not enable b because of pb. 4 p 2 2 b N p 2 2 2 b N 0 a qa pb p 2 b 2 2
N 00 a
a qa pb qa
pb If a minimal non-PN-solvable word is of the form u = a a, then either not contain the factor aa or does not contain the factor bb. does Proof: By contraposition. Assume that Two cases are possible: contains a factor aa and a factor bb.
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)kam i r [ : : : i s0 [ : : : i q [ (ab)bn 2(ba)k+1aam 2 i r [ : : : i where n; m 2; k
0. Recombine the letters in u to the following form: Since u ends with a, (ab)bn 2(ba)k+1a 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 ` = maxfi j xi > 1g. If ` = 0, we get a contradiction to proposition 4. Hence, ` > 0. Let t = minfj j yj > 1g. Then u has the form s0 [ a : : : i q [ bax` (ba)n `(ba)tbyt i r [ : : : a i Recombine the letters in u to the form
s0 [ a : : : i q [ (ba)ax` 2(ab)n `+t+1bbyt 2 i r [ : : : a i
Hence, u has a proper subword (ba)ax` 2(ab)n `+t+1b, 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
(
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 (
Some results about words of the form bx1 a : : : abxn
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.
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
(
a )
m + (x1 + : : : + xn)(b+
m (x1 + : : : + xk)(b+
The rst 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 full lled, 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
The relation 0 b0+ b0 m0 still holds for the new values. Also, all inequalities
in (
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 1ir1[b a bx2 1ir2[b a i : : : [ a bxk 1irk[bisk[ a i : : : [bxn 1 1irn 1[b a bxn i
Suppose some place q as on the right-hand side of gure 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 su ciently 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 q0 which is an exact copy of q, except that a+ = a 1 for
q0. This place q0 also disables a at state r1 (because it has the same marking as
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+
a+
The rst 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 full lled, then the
marking is a+ at all states after the rst 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 e ects 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
because of b+ b as noted above. The left-hand sides of the rst n 1
inequalities in (
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 (
Suppose w = bx1 abx2 a : : : abxn . If x1 minfx2; : : : ; xn 1g 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
considerations, 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 (
Case 1: m > 0 and a+ > 0. Then consider the transformation
m0 = m
1 and a0+ = a+
By m > 0 and a a+ > 0, we get new values m0; a0+; a0 0. Moreover, (
The rst of the inequalities (
x b+ The rst inequality follows because m = 0 and q has enough tokens after the rst x1 occurrences of b in order to enable a. The second inequality follows from x1 x. But then, since a only removes a tokens from q0 and the subsequent block of b's puts at least x b+ tokens back on q0, the marking on q0 is always 0, up to and including the last block of b's. 3
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 minfx2; : : : ; xn 1g, then w is solvable side-place-freely. 1
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.
Suppose w = bx1 abx2 a : : : abxn is solvable side-place-freely. Then in aw, all occurrences 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
(
and b0+ = b+ and a0 = a
These values satisfy (8), provided m, b+ and a (together with a+ = 0 and
b = 0) satisfy (
Note 2: Place q should not be removed as soon as q0 is added, because q could also be preventing a at some other rk. In that case, a new place q00 must be computed from q for this di erent 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 \un ring" 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 gure 5.
a 2 2 q1 p q2
b solves babbabb a 2 2 The places q1; q2 can be treated as in the above proof (that is, by changing their markings by \un ring" a) and yield new places q10; q20 with marking f(q10; 3); (q20; 3)g. If we allowed negative markings, then a new place p0 with initial marking (p0; 1) (and otherwise duplicating p) would do the job of solving ababbabb (as in the middle of the gure). However, we shall need a more re ned 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, + new inequation system: b+, b , + a+ and a , as well as a b0 + 0 m0 + (x1 + : : : + xi) (b0+
b0 ) + i (a0+
m0
(x1 + : : : + xk) (b0+
b0 )
k (a0+
a0 ) for 1
a0 ) + b0
i
1
n
This system has to be compared with a restricted form of (
+ + (x1 + : : : + xi) ( + b+; b ;
+ ) + i ( + (x1 + : : : + xk) ( + ) k ( + a+;
a ) + a+ ) 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.
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 (
If aw has a solution, then w has a side-place-free solution. Corollary 2. Side-place-free solvability of bx1 abx2 a : : : abxn w = bx1 abx2 a : : : abxn is solvable side-place-freely i aw is solvable. 2 6
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 lettercounting 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 2 fx; x + 1g 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 nding 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.