In this paper we investigate synthesis of place/transition Petri nets from three different finite representations of infinite partial languages, generalizing previous results.
In the last two years we generalized the theory a b a c a b a b of regions for the syn- a b a b a a b a b ... tsheeqsuiesnotfiaPl elatrnignueatgsefsroamnd a b c a b a c step languages to so a b a called partial languages A B C (A || (B + C))* [LJ06]. A partial language specifies the be- Fig. 1. Partial language given by a term. haviour of a concurrent system through a possibly infinite set of labeled partial orders (LPOs). Each LPO specifies a run of the system given by a partial order between events labeled by action names. Unordered events are interpreted to be concurrent. The left side of Figure 1 shows three different LPOs, the right side shows a partial language. Through the theory of regions it is possible to compute from a given partial language a Petri net having all specified LPOs as partially ordered runs and having minimal additional behaviour.
In this paper we consider classical place/ b a a a a transition Petri nets (p/t- a b a b b b a b a b dneevtse)l.oIpne[dLBanD Mef0fe7c]tiwvee 2 a b b b synthesis algorithm based on the theory of regions (N1,m1) L(N1,m1) from finite partial languages. In [LBDM08] Fig. 2. Partial language without term-based representation. we generalized this result to such infinite partial languages having a finite term based representation using operators for iteration (∗), sequential composition (;), alternative composition (+) and parallel composition (k). Figure 1 shows some of the LPOs of the infinite partial language given by the term (A k (B + C))∗ composing elementary LPOs A, B, C.1
Unfortunately only a small class of infinite partial lan- a a a guages can be represented in a a a a a ... such a term based form. The Figures 2 and 3 show ex- 2 a a a a amples of infinite partial languages which can not be given (N2,m2) L(N2,m2) by a term as above. The main reason for that is, that by the it- Fig. 3. Partial language without term-based represeneration operator it is not possi- tation. ble to append events only to a part of an LPO, but only to the whole LPO. In both cases a p/t-net having the given partial language as its set of (partially ordered) runs is shown.
In this paper we propose three different more general finite representations of infinite partial languages. Each of these representations allows to iteratively append events to parts of LPOs. Therefore, it is possible to represent the finite complete prefix of the branching process of bounded p/t-nets, i.e. we claim that by each of these finite representations the language of (partially ordered runs) of arbitrary bounded p/t-nets can be specified.
Due to lack of space we mostly present the ideas lying behind these finite representations only in an informal way through examples. Finally, very briefly, we suggest how regions could be defined for each of the finite representations. 2
In this section we introduce three different finite representations of infinite partial languages.
By N we denote the nonnegative integers. N+ denotes the positive integers. Given a finite set A, the symbol |A| denotes the cardinality of A. The set of all multi-sets over a set A is the set NA of all functions f : A → N. Given a binary relation R ⊆ A × A, we write aRb to denote (a, b) ∈ R. A directed graph is a pair (V, →), where V is a finite set of nodes and →⊆ V × V is called the set of arcs. A partial order is a directed graph po = (V, <), where <⊆ V × V is irreflexive and transitive.
Definition 1 (Labeled partial order). A labeled partial order (LPO) is a triple lpo = (V, <, l), where (V, <) is a partial order and l : V → T is a labeling function with set of labels T .
In our context, a node v of an LPO (V, <, l) is called event, representing an occurrence of l(v). Two nodes v, v′ ∈ V are called independent if v 6< v′ and v′ 6< v. Notice that by this definition, independence is reflexive. By co ⊆ V × V we denote the set of all pairs of independent nodes of V . A co-set is a subset C ⊆ V satisfying 1 Note that for a clearer presentation no transitive edges of the LPOs are drawn. ∀x, y ∈ C : x co y. A cut is a maximal co-set (w.r.t. set inclusion). For a co-set C of a partial order (V, <) and a node v ∈ V \ C we write v < C, if v < s for an element s ∈ C, and v co C, if v co s for all elements s ∈ C. A partial order (V ′, <′) is a prefix of a partial order (V, <) if V ′ ⊆ V , <′=< |V ′×V ′ and (v′ ∈ V ′ ∧ v < v′) =⇒ (v ∈ V ′). Given two partial orders po1 = (V, <1) and po2 = (V, <2), we say that po2 is a sequentialization of po1 if <1⊆<2. We use the notations defined for partial orders also for LPOs. If T is the set of labels of lpo = (V, <, l) then for a set V ′ ⊆ V , we define the multi-set |V ′|l ⊆ NT by |V ′|l(t) = |{v ∈ V ′ | l(v) = t}|. We consider LPOs only up to isomorphism Definition 2 (Partial language). Let T be a set. A set L of LPOs lpo = (V, <, l) with l(V ) ⊆ T and S(V,<,l)∈L l(V ) = T is called partial language over T .
A net is a triple (P, T , F ), where P is a (possibly infinite) set of places, T is a finite set of transitions satisfying P ∩ T = ∅, and F ⊆ (P × T ) ∪ (T × P ) is a flow relation.
(P, T , F, W ), where (P, T , F ) is a net, and W : F → N+ is a weight function.
We extend the weight function W to pairs of net elements (x, y) ∈ (P ×T )∪(T ×P ) with (x, y) 6∈ F by W (x, y) = 0. A marking of a net N = (P, T , F, W ) is a function m : P → N, i.e. a multi-set over P . A marked p/t-net is a pair (N, m0), where N is a p/t-net, and m0 is a marking of N , called initial marking. The occurrence rule of p/t-nets is defined as usual. The non-sequential semantics of a p/t-net can be given by enabled LPOs, also called runs. An LPO is enabled in a net if the events of the LPO can occur in the net respecting the concurrency relation of the LPO.
Definition 4 (Enabledness). Let (N, m0) be a marked p/t-net, N = (P, T , F, W ). An LPO lpo = (V, <, l) with l : V → T is called enabled w.r.t. (N, m0) if for every cut C of lpo and every p ∈ P there holds m0(p) + Pv∈V ∧v<C (W (l(v), p) − W (p, l(v))) ≥ Pv∈C W (p, l(v)). Its occurrence leads to the marking m′ given by m′(p) = m0(p) + Pv∈V (W (l(v), p) − W (p, l(v))) for each p ∈ P .
The set of of LPOs enabled w.r.t. a given marked p/t-net (N, m0) is denoted by L(N, m0). L(N, m0) is called the partial language of runs of (N, m0).
An alternative characterization of enabled LPOs is through so called process nets. A process net is an acyclic net without conflicts which “unfolds” a p/t-net by representing tokens from some marking of the p/t-net through places (called conditions) and transition occurrences through transitions (called events). Since in a process net the flow relation has no cycles and thus defines a partial order among conditions and events. Omitting the conditions and keeping this partial order between the events yields an enabled LPO, called run underlying the process net. The other way round, each enabled LPO sequentializes the run underlying some process net.
The set of all (alternative) process nets of a p/t-net can be represented by the (possibly infinite) branching process which is an acyclic net including conflicts. In the case the p/t-net is bounded, there is a finite prefix of the branching process (called complete finite prefix) which represents all reachable markings. Roughly speaking, it is determined through cutting the branching process if a marking is repeated. Omitting the conditions and keeping the partial order and conflict relation between the events yields a so called prime event structure (underlying the finite complete prefix) which represents a set if runs underlying process nets.
Note that the partial language of runs of a p/t-net is always prefix- and sequentializationclosed. In examples and Figures we often do not draw all prefixes and sequentializations but assume that they are present.
The finite complete prefix (resp. its underlying prime event structure) of b a a a a a a bounded p/t-net can be represented b a a b b b on the level of languages by a finite set of LPOs. Of course, from this finite set the complete non-sequential A1 A2 A3 A4 A5 A6 behavior can only be re-constructed, & if one keeps the information, at which A2[A6]=A2[A5]=A4[A5] points the branching process was cut w.r.t. which repeated marking. This Fig. 4. Set of LPOs with identification of states can be done by remembering, which representing L(N1, m1). prefixes of which LPO lead to the same marking. That means, a possibility for specifying the non-sequential behavior of bounded p/t-nets is through a finite set of LPOs together with some equivalence relation on prefixes of these LPOs.
If two prefixes are equivalent, this means that all events occurring after the one prefix a a a also can occur after the second prefix and vice a a a versa. Infinite behavior is specified for example if a prefix is prefix of an equivalent prefix.
Figure 4 shows, how by this method the lan- A1 A2 A3 guage L(N1, m1) from Figure 2 can be given. & The equation A2[A6] = A2[A5] = A4[A5] A1[A3]=A2[A3] means that after occurrence of A2 in A6 the same marking is reached as after occurrence Fig. 5. Set of LPOs with identification of A2 in A5 or after occurrence of A4 in of states representing L(N2, m2). A5. Therefore, after the occurrence of A4, the same events as after A2 in A5 or A6 can occur and so on. Also L(N2, m2) from Figure 3 can be represented this way (see Figure 5). This means, that through identifying states also the non-sequential behavior of unbounded nets can be specified (at least in some cases). 2.2
In [LBDM08] we introduced a term-based representation of infinite partial language. These terms, called composed runs, are build through composing inductively (elementary) LPOs from some given finite set of LPOs A. LPOs can be composed sequentially (;), alternatively (+) and parallel (k) and can be iterated (∗). That means each LPO A ∈ A is a composed run and if α, β are composed runs, then also α; β, α + β, α k β and α∗ are composed runs. Each composed run represents a set of LPOs, where an elementary LPO A represents the one-LPO set L(A) = {A}. The composed run α; β represents the set L(α; β) = {A; B | A ∈ α, B ∈ β}, α + β the set L(α + β) = L(α) ∪ L(β), α k β the set L(α k β) = {A k B | A ∈ α, B ∈ β} and α∗ the set L(α∗) = {A1; ...; An | Ai ∈ α}. On the level of LPOs A; B means that each event in A precedes each event in B and A k B means that there is no order between events in A and in B.
Such a representation of partial languages by composed runs is quite b a a b b b a a restrictive as shown in the introduc- a b b b tion, because through sequential composition and iteration it is not possible to append an LPO only to parts of A1 A2 A3 A4 R S some previous LPO. We therefore introduce here the possibility to iterate α = A1 + ((A2 ; (A3)* R);S A4) and sequentially compose LPO w.r.t. an “interface” specifying to which Fig. 6. Composed run with partial iteration parts of a previous LPO a subsequent representing L(N1, m1).
LPO is appended. Such an interface is given through an LPO I connecting events in the previous LPO to minimal events in the subsequent LPO. The composition w.r.t. to such an interface I is denoted by ∗I resp. ;I and is realized w.r.t. the ordering given by I.
Figure 6 shows, how by this method the language L(N1, m1) from Figure 2 can be specified: b a The LPO A3 is iterated through appending it only to the a-labeled event and finally A4 also is appended only to the a-labeled event. Note that it is in principle also possible to represent L(N2, m2) through A1 A2 A1; (A1 k A1)∗A1;(A1kA1). But the interpretation of X = A2 ; ((X + A1)|| A1) this expression is not totally clear because there are α = A1 + X two possibilities to use the interface A1; (A1 k A1) to iterate A1 k A1. One interpretation is that only Fig. 7. Composed term one of the possibilities can be applied, another is that with recursion representing both possibilities can be applied in parallel (and only L(N1, m1). in this second case L(N2, m2) is represented). 2.3
Another possibility to generalize composed runs is to equip them with recursion. Through recursion it is possible specify that some behavior is repeated at certain points of a composed run. For this also variables can be used in a composed run. Each variable represents a set of LPOs. The set of LPOs specified through a variable X is given through an equation X = α(X ), where α(X ) is a composed run including X (X need not be minimal in α(X )). The interpretation of such an equation is, that each occurrence of X on the right side may be replaced by the empty LPO or by α(X ) and so on. It is in general also possible that there are more variables in one composed run and that there are more equations.
Figure 7 shows, how by this method the language L(N1, m1) from Figure 2 can be given. Figure 8 shows, how by this method the language L(N2, m2) from Figure 3 can be given. 3
The general ideas of region based synthesis of p/tnets from partial languages L are as follows: The set a of transitions of the synthesized net is the finite set of labels of L. Places are defined by their initial marking and the weights on the arcs connecting them to transitions. Two kinds of places can be distinguished. A1 In the case that there is an LPO specified in L which is no run of the net which has only the one con- αX == XA1 ; (X || X) sidered place, this place restricts the behaviour too much. Such places are non-feasible (w.r.t. L). In the other case, the considered place is feasible (w.r.t. L). Fig. 8. Composed term The aim is to add enough feasible places in order ex- with recursion representing actly reproduce the specified behavior. L(N2, m2).
Feasible places are computed through so called token flow regions which are defined on the level of the partial language [LJ06]: If two events x and y satisfy x < y in an LPO lpo = (V, <, l) ∈ L, this specifies that the corresponding transitions l(x) and l(y) may be causally dependent. Such a causal dependency arises exactly if the occurrence of the transition l(x) produces one or more tokens in a place, and some of these tokens are consumed by the occurrence of the other transition l(y). Such a place can be defined as follows: Assign to every edge (x, y) of an LPO in L a natural number r(x, y) representing the number of tokens which are produced by the occurrence of l(x) and consumed by the occurrence of l(y) in the place to be defined. For this, we extend each LPO lpo ∈ L by an initial event vlpo and a final event, representing transitions producing the initial marking and consuming the final marking (after the occurrence of lpo). A feasible place pr is then defined by assigning for each extended LPO lpo = (V, <, l) ∈ L a natural number r(x, y) to each edge (x, y) function r, where it holds that (IN ): In(y, r) = Px<⋆y r(x, y) = Px<⋆z r(x, z) = In(z, r) for l(y) = l(z), (OU T ): Out(y, r) = Py<⋆x r(y, x) = Pz<⋆x r(z, x) = Out(z, r) for l(y) = l(z) and (IN IT ): Out(vlpo1 , r) = Out(vlpo2 , r) for lpo1, lpo2 ∈ L. We call In(y, r) the intoken flow of y which is interpreted as the weight of the arc connecting the new place pr with the transition l(y) (i.e. W (pr, l(y)) = In(y, r)). We call Out(y, r) the outtoken flow of x, which is interpreted as the weight of the arc connecting the transition l(x) with the new place pr (i.e. W (l(y), pr) = Out(y, r)). The outtoken flow of vlpo is called initial flow and is interpreted as the initial marking of the new place pr (i.e. m0(pr) = Out(z, r)). The value r(x, y) is called the token flow between x and y. A function r satisfying (IN ), (OU T ) and (IN IT ) is called region. The main result of [LJ06] is that the set of places corresponding to regions of a partial language equals the set of feasible places w.r.t. this partial language.
This notion of regions can easily be adapted to each of the proposed finite representations. Namely, in each case a token flow function r need to fulfil requirements additional to (IN ), (OU T ) and (IN IT ). In case, a partial language is given by a finite set of LPOs and an equivalence relation on prefixes of those LPOs, we require that – r satisfies (IN ), (OU T ) and (IN IT ) on the finite set of LPOs. – r satisfies that for equivalent prefixes the sum of token flows on edges leaving one prefix equals the sum of token flows on edges leaving the other prefix. In case, a partial language is given by a composed run using partial iteration, we require the same properties as for composed runs introduced in [LBDM08]. There an additional requirement was introduced for the so called set of iterated LPOs postulating that the initial and the final token flow of such iterated LPOs should be equal. The only difference now is that the initial and final token flow of such LPOs is computed in another way, namely w.r.t. the given interface. In case, a partial language is given by a composed run equipped with recursion equations, we require – the same as for composed runs and additionally that – for each equation X = α(X ) the intial flow of α(X ) equals the sum of token flows on edges ingoing an occurrence of X in α(X ) for each such occurrence. All these additional requirements can be represented as homogenous linear inequations as it is the case for (IN ), (OU T ) and (IN IT ). Thus effective solution algorithms can be adapted.