The reachability graph of a Petri net is a labelled transition system that can have a very complex structure. A characterisation of reachability graphs of Petri nets with only two transitions gives insight into typical structures that also might occur with arbitrarily large nets. An important means for such a characterisation is region theory, which allows to draw conclusions from cycles occurring in labelled transition systems. Attention is drawn especially to generalised cycles, i.e. cycles in the underlying undirected graph. Our characterisation also gives rise to an algorithm for the over-approximation of a given prefix-closed language by a Petri net language.
Introduction When looking at a Petri net [5] and its reachability graph we can take system analysis or system synthesis as a point of view on their relationship. In system analysis, we can e.g. model a system by a marked Petri net and construct its (unique) reachability graph to analyse its behaviour [6]. In system synthesis, a behavioural specification is typically given, and a system implementing it is sought. For example, one may try to find a Petri net whose reachability graph is isomorphic to a given labelled transition system [1].
Our ultimate aim is to characterise, graph-theoretically, exactly the labelled transition systems that are synthesisable into a place/transition Petri net. To our knowledge, such a characterisation is difficult and has not yet been achieved in general. In the special case of binary words, there have been approaches via pattern matching and via letter counting [2–4] which successfully lead to a characterisation of Petri net synthesisable words, i.e. where the reachability graph consists of a single, specific sequence of states without any branching.
In this paper, we try to lift this limitation a bit and find the common structure of reachability graphs of Petri nets with only two transitions (generating sets of binary words). Based on region theory [1], we show how these reachability graphs can be partitioned into only a few classes each having strong common properties. The classes closely depend on the presence or absence of generalised cycles in the reachability graph (i.e. cycles in the underlying undirected graph).
In case a given behaviour cannot be synthesised, we might ask for a small over-approximation, i.e. a reachability graph including all the required behaviour and allowing as few as possible additional words. If the given behaviour is finite, we can extend our results to obtain an algorithm for computing the minimal over-approximation by computing a convex hull for a subset of N2.
In section 2 we briefly recapitulate some basic definitions about labelled transition systems, Petri nets, and regions. Section 3 describes shapes of reachability graphs containing generalized cycles with non-zero Parikh vectors, while section 4 handles those where all generalised cycles have Parikh vector zero, essentially allowing a transformation to some subset of N2. In section 5 we present the algorithm for over-approximating the behaviour of a finite, binary, prefix-closed language, before concluding the paper in section 6. 2
Basic Concepts LTS. A labelled transition system (LTS) with initial state is a tuple T S = (S, →, T, s0) with nodes S (a countable set of states), edge labels T (a finite set of letters), edges → ⊆ (S ×T ×S), and an initial state s0 ∈ S. An edge (s, t, s0) ∈ → may be written as s →t s0 or s0 ←t s. We use s t s0 as an abbreviation for (s →t s0 ∨ s ←t s0) and call it a generalised edge or g-edge (in the underlying σ undirected graph). A path (g-path) σ ∈ T ∗ from s to s0, written as s → s0 (s σ s0), is given inductively by s = s0 for the empty word σ = ε and by ∃s00 ∈ S: s →w s00 →t s0 (s w s00 t s0) for σ = wt with w ∈ T ∗ and t ∈ T . A path s →σ s0 (g-path s σ s0) is a cycle (g-cycle) if and only if s = s0. It is called elementary if |σ| is the number of different states occurring on the path, i.e. every state appears only once. The Parikh vector ℘(σ) : T → Z of a g-path s σ s0 is a mapping defined by ℘(ε) = 0 (with 0(t) = 0 for all t ∈ T ) for the empty word σ = ε, by ℘(wt)(t0) = ℘(w)(t0) for σ = wt and t 6= t0, by ℘(wt)(t) = ℘(w)(t) + 1 in case the g-path is s w s00 →t s0, and ℘(wt)(t) = ℘(w)(t) − 1 if the g-path is s w s00 ←t s0 for some s00 ∈ S.
Two labelled transition systems 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. We call T S1 a sub-LTS of T S2 if S1 ⊆ S2, →1 ⊆ →2, and s01 = s02. A binary LTS (bLTS) is an LTS (S, →, T, s0) with |T | = 2, in this paper usually with T = {a, b}. A word over T is a sequence w ∈ T ∗, and it is binary if |T | = 2. A word w = t1t2 . . . tn of length n ∈ N uniquely corresponds to a finite transition system T S(w) = ({℘( ), ℘(t1), . . . , ℘(t1 . . . tn)}, {(℘(t1 . . . ti−1), ti, ℘(t1 . . . ti)) | 0 < i ≤ n ∧ ti ∈ T }, T, ℘( )). A language over T is a set L ⊆ T ∗. For a finite language L we can uniquely define a transition system T S(L) = Sw∈L T S(w), where for words w1, w2 ∈ T ∗ and T S(w1) = (S1, →1, T, ℘( )), T S(w2) = (S2, →2, T, ℘( )) we write T S(w1) ∪ T S(w2) = (S1 ∪ S2, →1 ∪ →2, T, ℘( )).
Since we are interested in behaviour expressed as an LTS, we will assume LTS to be totally reachable, i.e. for every state there is a path from the initial state to it. This also means that each two states are connected by a g-path. In case of a not totally reachable LTS we may drop all unreachable states without loss of behaviour.
Petri net. 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 Petri net N is the labelled transition system with the set of vertices [M0i, initial state M0, label set T , and set of edges {(M, t, M 0) | M, M 0 ∈ [M0i ∧ M [tiM 0}. If a labelled transition system T S is isomorphic to the reachability graph of a Petri net N , we say that N PN-solves (or simply solves) T S, and that T S is synthesisable to N . We say that N solves a word w if it solves T S(w). We frequently identify the states of T S with the markings of N then, writing e.g. s(p) ≥ F (p, t).
Reachability graphs (and their underlying LTS) have some nice properties we can make use of: They are fully deterministic (s1 ←σ1 s →σ2 s2 ∧ ℘(σ1) = ℘(σ2) =⇒ s1 = s2 and s1 →σ1 s ←σ2 s2 ∧ ℘(σ1) = ℘(σ2) =⇒ s1 = s2), totally reachable (∀s ∈ S ∃σ ∈ T ∗: s0 →σ s), and zero-path-cyclic (s σ s0 ∧ ℘(σ) = 0 =⇒ s = s0). Separation problem. Let a labelled transition system T S = (S, →, T, s0) be given. If we want to synthesise a Petri net with isomorphic reachability graph, T must be used directly as the set of transitions, since we do not consider any transition labels. In case the LTS is finite, we have to solve 21 ·|S|·(|S|−1) state separation problems for the places and up to |S|·|T | event/state separation problems, as follows: – A state separation problem consists of a set of states {s, s0} with s 6= s0, and it can be solved by a place that distinguishes them, i.e. has a different number of tokens in the markings corresponding to the two states. – An event/state separation problem consists of a pair (s, t) ∈ S×T with ¬(s →t). For every such problem, one needs 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. On the other hand, for every edge s0 →t s00 we must guarantee M 0(p) ≥ F (p, t), M 0 being the marking corresponding to state s0. If the LTS is infinite, also the number of separation problems (of each kind) becomes infinite.
Region. An abstract region r of an LTS (S, →, {t1, . . . , tn}, s0) is a tuple r = (r0, r1, . . . , rn) where r0 ∈ NS and ri ∈ Z for 1 ≤ i ≤ n with the following consistency property: ∀s, s0 ∈ S ∀i ∈ {1, . . . , n}: (s →ti s0 =⇒ r0(s0) = r0(s) + ri). The property implies that for every g-cycle s σ s in the LTS holds Pn i=1 ℘(σ)(ti)· ri = 0. It follows that the value r0(s) is fully defined by r0(s0) and the ri with 1 ≤ i ≤ n.
An abstract region in a reachability graph gives rise to an equivalence class of places p where M0(p) = r0(s0) and ri = F (ti, p) − F (p, ti). If the region distinguishes the states s and s0 of two reachable markings M and M 0 (by r0(s) 6= r0(s0)), the firing rule of the Petri net ensures that M (p) 6= M 0(p). Lemma 1 (Indistinguishable Regions). Let r = (r0, r1, . . . , rn) be an abstract region of some (fully reachable) LTS (S, →, {t1, . . . , tn}, s0) with s, s0 ∈ S. If r does not solve the state separation problem {s, s0} (by distinguishing s and s0), neither does r0 = (k · r0 + i, k · r1, . . . k · rn) with i, k ∈ Z.
Proof. Note: If k · r0(s) + i < 0, r0 is not a region and there is nothing to prove. Assume r0(s) = r0(s0). Then, (k·r0(s0)+i)−(k·r0(s)+i) = k·(r0(s0)−r0(s)) = 0. tu
Places constructed from abstract regions are sufficient to deal with all state separation problems but not event/state separation problems. For fully determined places (with exactly known values for F (p, ti) and F (ti, p)) one would have to consider more refined regions. Instead, we argument directly about the loops at some place p in a Petri net, i.e. about the value kt := min{F (p, t), F (t, p)} for each transition t. Together with a region for p, they fully determine the arc weights between p and its neighboring transitions. Places derived from the same region, distinguished by the loop values kt only, can easily be unified. Lemma 2 (Loop maximisation). Let N = (P, T, F, M0) be a Petri net with p1, p2 ∈ P and kt ∈ Z for each t ∈ T such that M0(p2) = M0(p1), ∀t ∈ T : F (p2, t) = F (p1, t) + kt and F (t, p2) = F (t, p1) + kt. Define a new Petri net N 0 by adding kt to each of F (p1, t) and F (t, p1) if kt > 0, for every t ∈ T , and then deleting p2 including all adjacent arcs. N 0 has the same reachability graph as N . Proof. Note that M (p1) = M (p2) holds for all reachable markings M in N . A transition t is not firable in N at M , if M (p1) < F (p1, t) or M (p2) < F (p2, t), or put differently, if M (p1) < max{F (p1, t), F (p2, t)}. This maximum is exactly the arc weight F (p1, t) as defined for N 0. Since the token change on p1 by firing a transition is the same in N and N 0 and enabledness of transitions also remains unchanged from N to N 0, both nets have the same reachability graph. tu
So, of all places constructed from the same region, we need only one, i.e. the place with the maximal number kt of loops, separately computed for each adjacent transition t in the Petri net. 3
Generalised Cycles with Non-Zero Parikh Vectors We would like to characterise the reachability graphs of Petri nets with at most two transitions. As a first case we consider only reachability graphs that contain at least one generalised cycle with a non-zero Parikh vector. Theorem 1 (Shapes with Non-Zero Parikh Cycles). If the reachability graph of a Petri net (P, {a, b}, F, M0) contains a g-cycle with a non-zero Parikh vector, it has one of the seven general shapes shown in Figures 1, 3, and 5 or it consists of just the initial state without any edges.
Proof. Let (S, →, {a, b}, s0) be a synthesisable bLTS, i.e. the reachability graph of some Petri net (P, {a, b}, F, M0), with some g-cycle s σ s such that ℘(σ) 6= 0.
From the definition of abstract regions we know that every g-cycle must have a weighted sum of zero in any region of the LTS. Let r = (r0, ra, rb) be any such region, then ℘(σ)(a) · ra + ℘(σ)(b) · rb = 0. Our knowledge about ra and rb depends directly on the Parikh vector of σ.
Case 1: ℘(σ)(a) = 0. Obviously then, ℘(σ)(b) 6= 0 and thus rb = 0, but we know nothing about ra. As a consequence, following a b-edge s →b s0 in the LTS cannot modify the region value, i.e. r0(s0) = r0(s) + rb = r0(s). Therefore, because no region can distinguish s and s0, and neither can any place distinguish the corresponding markings in the Petri net, the markings must be identical. We conclude that s = s0 for every b-edge s →b s0, all b-edges must be loops in the reachability graph. Figure 1 depicts all possible reachability graphs, with a (class of) example Petri nets on the left. The shape of the reachability graph depends on whether the occurring regions have positive, zero, or negative ra values: a a a a q q q q f f −r f −r b b b b b a b 0 0 0 a 1 0 a 1 – If in all regions r = (r0, ra, 0) holds ra = 0, transition a cannot change the marking in the Petri net either. If a can fire at all, we obtain the reachability graph in the first row of Figure 1. If a cannot fire, we get the second row. – If there is a region with ra > 0 but none with ra < 0, and assuming that a can fire at all, its firing will increase the number of tokens on any place connected to it. With increasing markings we obtain an infinite series of pairwise distinguishable states as in the third row of Figure 1. Since b occurs in the reachability graph, there is some earliest state q at which it forms a loop. As the markings rise from this point on, b is also activated at all later states. – If there is a region with ra < 0, there must be a place from which a removes tokens and eventually becomes deactivated. In the fourth line of Figure 1 a can fire exactly f times. The transition b can be deactivated at an earlier state r, if the place is a side-place of b (in the picture with arc weight f − r). If there is also a region with ra > 0, b may not be activated until some state q just as in the previous subcase.
Case 2: ℘(σ)(b) = 0. This case is analogous to the previous one.
Case 3: ℘(σ)(a) · ℘(σ)(b) > 0. Quite obviously then, ra · rb < 0 and rb = − ℘℘((σσ))((ab)) ·ra, so ra and rb have a fixed ratio in every region. For every pair of such regions, we can use Lemma 1 to find a new region that is a common multiple with modified initial value r0, i.e. any two such regions solve exactly the same state separation problems. Therefore, only two regions are of interest, one with ra < 0 and rb > 0 that can prevent an a, and one with ra > 0 and rb < 0 which can prevent b. By Lemma 2, the number of places constructed from each region can be reduced to one, the one with the maximal number of loops at each transition. Therefore, it is sufficient to have at most two regions, (r0, ra, rb) and (r00, −ra, −rb), and to construct one place from each region. A representative class of Petri nets with such two regions is shown in Figure 2.
On the right hand side of Figure 2 we can see an LTS representing the reachability graph. For simplicity, we have named the initial state 0, which leads to states with negative numbers. By adding j, we can obtain the values of a possible region.
If we omit one of the two regions (places), the state space will become infinite, as either the boundary −j or the boundary i will fall. We may think of this as replacing −j by −∞ or i by ∞. If we omit both places, the reachability graph collapses to the first row of Figure 1. increment will complete a new diamond in the graph (here with 28 →b 25 →a 30). Incrementing j will analogously add a diamond at the other end. Adding loops via parameters k1 to k4 essentially cuts off such diamonds again, unless the cutting point is near the initial state. In this case, only one kind of edge is removed. The initial state will then not lie on a cycle anymore but form a path (using the other kind of edges) that leads to the cyclic part of the LTS. The parameters m and n determine the length of cycles in the LTS and the ratio of a and b on these cycles. 5 a s0 0 a b b 9 a
b 14 b a 17 b 12 22
a a 25 b
b b a a 13 b a a b k2 k3
Unlike Case 3, there is a steady token flow from the left to the right place, no matter which transition is fired. Therefore, the right place determines when a transition may start firing and the left place when the firing must cease. Since the left place will at some point stop both transitions from firing, the reachability graph will normally be finite. Only if we remove the left place from the net, we can obtain an infinite behaviour (with states then named according to the number of tokens on the right place). These possibilities are shown in Figure 5.
Case 4: ℘(σ)(a) · ℘(σ)(b) < 0. With the same reasoning as in the previous case but ra · rb > 0, we find that again two regions (r0, ra, rb) and (r00, −ra, −rb) and one place constructed from each region must be enough. This leads to the class of Petri nets shown in Figure 4.
The upper reachability graph (with the dotted edge) corresponds e.g. to the Petri net with parameters i = 8, j = 0, m = 2, n = 3, and k1 = k2 = k3 = k4 = 0. Introducing loops at the left place will prevent the rightmost edges, i.e. setting b b a 2 a 6 k4 = 1 will eliminate the dotted b-edge, setting it to 2 will also prevent the b-edge ending at state 1, and so on.
The lower reachability graph corresponds to a Petri net without the left place and its adjacent edges. It has the parameters j = 0, m = 2, n = 3, and k2 = k3 = 0. Adding a loop at the right place prevents edges beginning at the initial state. Setting k3 = 1 will remove the b-edge at 0 and make state 3 unreachable. Therefore, the edges from state 3 also become unusable (shown as dotted lines).
With cases 1 to 4, we have covered all possible g-cycles with non-zero Parikh vector that might occur in a reachability graph of a Petri net with transitions a and b. This concludes the proof of Theorem 1. tu 4
Generalised Cycles with Zero Parikh Vectors only Let us now assume, that our LTS does not have any g-cycle σ with ℘(σ) 6= 0. In this case, the transitions a and b are independent, and we may use a base transformation to project the LTS onto the plane N2, with the initial state mapped to (0, 0). The transitions a and b become the base vectors, i.e. firing a increments the first component of a state, (x, y) →a (x + 1, y), and firing b increments the second component, (x, y) →b (x, y + 1), whenever the transitions are allowed.
Since all g-cycles σ have zero Parikh vectors, ℘(σ) = 0, the equation ℘(σ)(a)· ra + ℘(σ)(b) · rb = 0 does not restrict the values for ra and rb of a region in any way. If we distinguish regions (r0, ra, rb) by the signs of ra and rb, there are essentially nine types of regions. Regions with non-negative values for ra as well as rb do not restrict the enabledness of transitions. With positive values for ra and rb, the five remaining types can be written as (r0, −ra, +rb), (r0, −ra, 0), (r0, −ra, −rb), (r0, 0, −rb), and (r0, +ra, −rb). An example LTS with one region of each of the five types is shown in Figure 6.
Let now N = (P, {a, b}, F, M0) be a Petri net and G the projection of the reachability graph onto N2. Furthermore, let R be the set of regions of G. with (x, y) →b (x, y + 1).
Lemma 3 (Inner States). Let N be pure (i.e. ∀p, t : F (p, t) · F (t, p) = 0) and (x, y) ∈ G be some state. If ∀(r0, ra, rb) ∈ R: r0((x+1, y)) ≥ 0, then (x+1, y) ∈ G with (x, y) →a (x+1, y). If ∀(r0, ra, rb) ∈ R: r0((x, y +1)) ≥ 0, then (x, y +1) ∈ G Proof. Note first, that for any state (x, y) ∈ N2 and any region (r0, ra, rb) ∈ R holds r0((x + 1, y)) = r0((x, y)) + ra and r0((x, y + 1)) = r0((x, y)) + rb by the definition of a region, since we use a and b as base vectors in N2.
To prevent (x, y) →a in G, there must be a region (r0, ra, rb) ∈ R with ra < 0. For a place p constructed from such a region, ra = F (a, p) − F (p, a) must hold. Since N is pure, F (p, a) > 0 and F (a, p) = 0. Now, r0((x + 1, y)) − r0((x, y)) = ra = −F (p, a) and with r0((x + 1, y)) ≥ 0 we conclude r0((x, y)) ≥ F (p, a). Since by construction of p, r0((x, y)) is the number of tokens on p at the state (x, y), a a b b a a a a a a b b b b b a a a a a b b b b a a a a a b b b b a a a b b a a a b b b p cannot prevent firing a at the corresponding marking. Since the region and p were arbitrary, (x, y) →a (x + 1, y) holds in G, i.e. (x + 1, y) ∈ G.
An analogous reasoning holds for (x, y + 1) and the transition b. tu Theorem 2 (Reachability graphs of pure nets without Parikh-nonzero g-cycles). An LTS G in which all g-cycles have Parikh vector zero is the reachability graph of a pure Petri net N = (P, {a, b}, F, M0) if and only if it can be viewed as a weakly connected convex subset of N2 containing the initial state (0, 0) such that for each two states (x, y), (x + 1, y) ∈ G: (x, y) →a (x + 1, y) and for each two states (x, y), (x, y + 1) ∈ G: (x, y) →b (x, y + 1). Proof. Note that convex subsets of N2 can be defined by cutting off parts of N2 using straight lines, and that these lines may not cut off the initial state, so our five types of regions give rise to exactly this kind of convex subset.
Using Lemma 3 proves that all necessary states and edges exist. In some
extreme cases, e.g. with regions (
It remains to show that a pure Petri net can be found such that its
reachability graph does not identify any two of the states in N2. This can easily be
done using the regions (
To characterise the reachability graphs of non-pure nets in the same way, we need to consider the effect of adding a self-loop between a place (representing some region (r0, ra, rb)) and the transition a or b. The dotted lines in Figure 6 show where the corresponding region has the value zero, or put differently, they are the border that edges cannot cross. We can also interpret them as two different lines at the same location, one preventing the a-edges, the other preventing the b-edges from crossing into the half-plane of negative region values. Let us call these lines the a-line and b-line of the region.
Lemma 4 (Shifting enabledness lines). Let N = (P, {a, b}, F, M0) be a pure Petri net with a place p ∈ P (with corresponding region (r0, ra, rb)), and let N 0 be derived from N by adding k ∈ N to both F (p, a) and F (a, p). Let G and G0 be the reachability graphs of N and N 0 projected to N2. Then, from G to G0, the a-line is shifted by the fraction of rka of the unit-a-vector, unless ra = 0, then it is shifted by the fraction of rkb of the unit b-vector. If ra = rb = 0, either nothing happens (in case r0 ≥ k) or G0 collapses and does not contain any a-edges (if r0 < k).
Proof. Note first, that G0 is a subgraph of G since N 0 has a more restricted behaviour than N . If ra 6= 0, any a-edge changes the number of tokens on p by ra, therefore the rka th fraction of an a-edge increases the number of tokens on p by k. This is exactly the additional amount of tokens needed in G0 to allow an a-edge, thus the a-line moves from G to G0 by the rka th fraction of a unit-a-vector (possibly in the opposite direction if ra < 0).
If ra = 0, still a-edges are allowed only if the region value is at least k, since in N 0 we have F (p, a) = k = F (a, p). A line representing the region value of k is exactly at a distance of rkb times the unit-b-vector from the b-line, and becomes the new a-line.
If the region is (r0, 0, 0) neither transition can change the start value r0. We either have r0 ≥ k, i.e. r0 ≥ F (p, a) = F (a, p), so the number of tokens on p is sufficient to allow an a at all states. Or we have r0 < k, in which case there are no a-edges in G0 at all and G0 represents some word from b∗. tu
This lemma can obviously be formulated for the transition b as well. In
Figure 8 we can see the effect of adding one self-loop with a for each of the five places
representing one of the regions (
b a a b
Theorem 3 (Reachability graphs of nets without Parikh-non-zero gcycles). Let C ⊆ N2 be a convex area and let Ca, Cb be derived from C by shifting borders of C only. Let G be the graph including (0, 0) such that (x, y) →a (x + 1, y) ∈ G ⇐⇒ (x, y) ∈ G ∩ Ca, (x + 1, y) ∈ Ca and (x, y) →b (x, y + 1) ∈ G ⇐⇒ (x, y) ∈ G ∩ Cb, (x, y + 1) ∈ Cb. Then, G is the projection of a reachability graph of a Petri net N = (P, {a, b}, F, M0) to N2. If the reachability graph of a Petri net (P, {a, b}, F, M0) does not contain g-cycles σ with ℘(σ) 6= 0, Ca and Cb meeting the above conditions can always be found.
Over-approximation of finite languages Assume now that we have a finite language L over a binary alphabet {a, b} given, and we aim to synthesise a Petri net which allows firing of all the words of this language. Due to the fact that for each Petri net, every prefix of a feasible transitions sequence is also feasible, we will assume L to be prefix-closed, i.e. for every uv ∈ L with u, v ∈ {a, b}∗, it holds u ∈ L. For a Petri net N , let L(N ) be the set of all transition sequences fireable in N . Since we consider only unlabelled Petri nets, it may be the case that there is no net N such that L(N ) = L. Nevertheless, there exists a net N such that L ⊆ L(N ) (for instance, the net N = ({Pa, Pb}, {a, b}, {(Pa, a) 7→ 1, (Pb, b) 7→ 1}, (l, l)) with l = maxw∈L |w|). Hence the challenging problem is to find a net N such that L ⊆ L(N ) and the difference between L(N ) and L is minimal. The characterisations established in Theorem 2 and 3 suggest a possible algorithm for such an over-approximation of finite languages.
a a b a a b b b a b a b a a b
b 4 3 2 1 0 b b b
a a (2,
Let L = {abbabaa, bbababaa}, where over-line stands for prefix-closure, be
an example language for which we seek to produce a Petri net whose language
includes L. We can easily translate L into a labelled transition system T S(L)
without Parikh-non-zero g-cycles (l.h.s. in Figure 9). As we have established in
Section 4, regions are represented as lines on N2, and these lines are essentially
the borders that the projected arcs cannot cross. According to Lemma 4,
being considered as a line, the same region can simultaneously impose for each
transition its own border. In order to find the over-approximating Petri net, we
first build regions for each letter, a and b, separately. E.g., for b in our example
in Figure 9 we construct the regions (
Algorithm 1 Over-approximation of a finite language Input: finite (prefix-closed) language L ∈ {a, b}∗ Output: Petri net over-approximating L compute sets Wa = {(x, y) | ℘(wa) = (x, y) ∨ ℘(w) = (x, y), wa ∈ L}
Wb = {(x, y) | ℘(wb) = (x, y) ∨ ℘(w) = (x, y), wb ∈ L} find the convex hulls Ha = ((xi, yi))0≤i≤ka ⊆ Wa of Wa (enumerated clockwise)
Hb = ((xj, yj))0≤j≤kb ⊆ Wb of Wb (enumerated clockwise) (Pa, T, Fa, M0,a) ← partialSolution(a, b, Wa, Wb, Ha) (Pb, T, Fb, M0,b) ← partialSolution(b, a, Wb, Wa, Hb) N ← (Pa ∪ Pb, {a, b}, Fa ∪ Fb, M0,a ∪ M0,b) return N procedure partialSolution(a, b, Wa, Wb, H)
{construct the net restricting the firings of one transition} begin procedure m ← |H|, P ← ∅ {find the size m of the hull, define the set of places P } for i = 0 to m − 1 do {construct places from H taking into account Wb} raii ← yi − yi+1 {define a region as a line through two points} rbi ← xi+i1 − xi {orthogonal’s direction accords with the ordering of H} r0 ← −ra · xi − rbi · yi define place pi M0(pi) ← r0i iiff rrbaii ≥≥ 00 tthheenn FF((ba,,ppii)) ←← rrbiai,,FF((ppii,,ba))←←00eelslseeFF((ppi,i,ba))←←rbr,ai,FF(b(,ap,ip)i)←←0 0 i if Wb \ Wa 6= ∅
then add place pi to P endfor return (P, {a, b}, F, M0) end procedure (x0, y0) ← arg max{(x,y)∈Wb\Wa|r0i+x0·rai+y0·rbi<0}{|r0i + x · rai + y · rb|} i {arg max returns the argument yielding the maximum of the set} k ← |x0 · rai + y0 · rbi| − r0i {define the “moving factor”} M0(pi) ← M0(pi) + k, F (pi, a) ← F (pi, a) + k, F (a, pi) ← F (a, pi) + k {adjust the restrictions to include outer states}
Algorithm 1 describes this process formally. In order to construct a convex hull, one can use the Quickhull [7] algorithm which produces the hull in O(n2) in the worst case, where n is the size of the initial set (which is the set of states of the LTS in our case). For a language L we have n ≤ |L| · l (l being the length of the longest word). The complexity of the partialSolution procedure is O(n2) in the worst case. Hence, the total complexity of the algorithm does not exceed O(n2). Applying the algorithm to the language L, we obtain the Petri net on the left hand side of Figure 10, its reachability graph being depicted on the right hand side.
a 2 In this paper a graph-theoretical characterisation of the reachability graphs of Petri nets over the binary transition set is presented. The characterisation relies on the notion of generalised cycles. Based on this characterisation and the absence of Parikh-non-zero g-cycles, an algorithm for over-approximating a finite language by a Petri net language is suggested.
A natural continuation of this line of work is to use more than two transitions. Unluckily, just considering all pairs of transitions (others being “invisible”) is insufficient, so even an extension to only three transitions is far from trivial.