s from data, the synthesis problem is already solved. In this paper, we present an approach for a class of services that deals with data explicitly.
start order wait [e = e0] use equipment • e e • final (a) medic pn(e) e0 o d o d n
n pn−1(n) • n • start’ receive order order deliver equipment final’ o d n e • n n • start’ receive order order deliver equipment final’ (b) supply center
(c) supply center 2
The following example illustrates the interaction of a medic with a medical supply center from which the medic orders medical equipment. Both the medic and the supply center are services represented by the open nets in Fig. 1a and Fig. 1b. The composition (medic⊕supply center) of the open nets medic and supply center is the Petri net we obtain by fusing the interface places o and d. The medic orders medical equipment by firing the transition order. Thereby the token • is removed from place start. The variable e is assigned the equipment the medic orders, e. g., a syringe. Therefore, a token with value syringe is produced on place wait. The term pn(e) evaluates to the product number of the syringe. A token with that value is produced on the output place o. This corresponds to sending a message to supply center.
The medic waits for an incoming delivery on place d. supply center receives the order message from o by firing receive order and n is assigned the product number of syringe. The transition deliver equipment takes the product number from place order and produces the equipment corresponding to that number (in this case syringe) on interface place d. Since the tokens on wait and d are equal, the guard e = e0 of transition use equipment is fulfilled. Therefore use equipment can fire and (medic⊕supply center) reaches its final marking, i. e. the marking in which both places final and final’ are marked with the token •.
Two open nets N1 and N2 are called partners, if from each reachable marking of N1 ⊕N2 a final marking of N1 ⊕N2 is reachable. The medic and supply center are partners. The medic and supply center 2 are not partners: When deliver equipment fires, any arbitrary equipment may be assigned to e which in general does not correspond to the product number assigned to n. Therefore, there is a marking reachable in (medic⊕supply center) with a token with value syringe on wait and a token with another value (e. g. stethoscope) on d. This marking is a deadlock, because e = e0 is not satisfied and use equipment can not fire. On acyclic open nets, the reachability of a final marking is equivalent to deadlock freedom.
An open net N1 is called controllable, if it has a least one partner. medic is controllable. In this example, we assumed that function pn has an inverse pn−1. However, if we replace pn by a function pn0 which is not bijective, medic becomes uncontrollable. In that case, a supply center can not infer the equipment the medic is waiting for from the product number. Therefore, it is not possible to guarantee that e = e0 is always satisfied and the final marking will be reached.
In the next section, we sketch an approach to synthesize a partner for a specific class of open nets. 3
In this section, we sketch a partner synthesis algorithm for a given open net
N . We consider a class of Petri nets where the domain of the variables and the
colours of the tokens is infinitely large. The guards are denoted in a subset of
first order logic that contains boolean algebra and quantifiers. For computational
reasons, we assume that this subset is decidable (like e. g. Presbuger arithmetic
[
Due to infinitely many colours, the state space of N is infinitely large.
Therefore the synthesis algorithm for finite state services given in [
Now we give an overview of our synthesis algorithm. The details will be explained later by example. First, we construct an over-approximation S0 of the partners of N . S0 is a prefix of depth k of an infinite tree-like open net U we call universal environment. Then we iteratively add guards to S0. Adding a guard corresponds to removing states from the over-approximation in the finite case. The iteration is repeated until no deadlock is reachable in the composition of N and S0. Each time a guard is added, some of the deadlocks of the composition become unreachable. Each iteration step may also introduce new deadlocks which will then be eliminated in the next iteration step. If (and only if) N is controllable, the composition will eventually be deadlock free and the modified S0 is a partner.
Now we show the derivation of a partner of medic from Fig. 1a. We assume that the colours of medic are integers and pn is the bijective function with pn(x) = x + 1. Therefore, medic can be expressed with Presburger arithmetic. d o x1 (x0, x1) s0 q1 s1 q2 • (x0, x1)
x1 (x0, x1) (a) Universal environment U (b) Finite prefix S0 of U
Fig. 2a shows the universal environment of medic. U is an infinite open net that has the inverse interface of N . U has a regular tree-like structure and can send and receive any (possibly infinite) sequence of messages. Therefore, U is an over-approximation of every partner of N . U stores every message sent or received from N . Each of the variables x0, x1, . . . corresponds to the value of a message. These variables will be used in the guards which we will add later on. Since U is infinitely large, it is not suited for computational methods. Due to the acyclicity of N , the number of messages N can send and receive is bounded by a number k. Therefore, the prefix of U of depth k is still an over-approximation of the partners of N .
In the example, k is 2. In this particular case, we can even remove the branches of U which send or receive two messages on the same interface place without destroying the over-approximation property. This is possible because medic sends or receives at most one message on each interface place. Thus, we get the prefix S0 of U in Fig. 2b.
Now we iteratively derive a guard for each transition of S0. The transitions are processed in bottom-up order. Thereby, we obtain a sequence S0, S1, S2, . . . of open nets with successively smaller reachability graphs.
Intuitively, a guard forbids a transition s of S0 to fire in a certain firing mode if there is the possibility to reach a deadlock after s has fired in that mode. That way, deadlocks are successively removed from the composition.
Since a transition has infinitely many firing modes, we need a syntactical
representation of all firing modes that may not lead to a deadlock. We derive the
guard predicate that is assigned to each transition using a technique outlined in
[
In our example, the integer that is chosen non-deterministically by order for e is represented by the variable v0 in marking M1. Analogously, the integer sent by s1 on d is represented by v1. The effect of the guard e = e0 of use equipment is represented by the condition v0 = v1 of the markings M4 and M7. Every other symbolic marking has the condition true.
The method we use to derive the guard of a transition s of S0 is inspired
by Dijkstra’s predicate transformer semantics [
M4 and M7 are final markings. Therefore, DF 0(M4) ≡ DF 0(M7) ≡ true. Since M3 has a successor marking only for those assignments of v0 and v1 with v0 = v1, we get DF 0(M3) ≡ v0 = v1. Analogously, DF 0(M6) ≡ v0 = v1. For every other symbolic marking M we get DF 0(M ) ≡ true.
From every predicate DF (M ), we derive a predicate DF 0(M ) which expresses the condition that M does not evaluate to a deadlock in terms of the variables used by the transition s of S0 that precedes M in the SRG (s is unique because S0 is a tree). By assigning DF (M ) as a guard to s, every evaluation of M which is a deadlock becomes unreachable. The relationship between the variables x0, x1, . . . of S0 and the variables v0, v1, . . . of the SRG is established by the the symbolic firing mode of s.
In the example, M3 is reachable via exactly one path of the SRG. The last transition of S0 on this path is s1 with the symbolic firing mode hx0 = pn(v0), x1 = v1i. As stated above, DF 0(M3) ≡ v0 = v1. With x0 = pn(v0), x1 = v1 and the assumption that pn is injective follows that v0 = v1 is equivalent to pn−1(x0) = x1. Formally, we express this transformation by universal quantification of v0, v1: DF 00(M3) ≡ ∀v0, v1 : x0 = pn(v0) ∧ x1 = v1 =⇒ v0 = v1
≡ x1 = pn−1(x0) In words: DF 00(M3) describes all assignments of x0, x1 for which the post-condition v0 = v1 is guaranteed to hold after the firing of s1 in mode hx0 = pn(v0), x1 = v1i, regardless of which integers might have been non-deterministically chosen for v0, v1.
The general form of a DF 0 predicate (for the special case that there is only one path in the SRG to M ) is
∀v0, . . . , vj : COND(M ) ∧ x0 = T0 ∧ . . . xn = Tn =⇒ DF (M ) where hx0 = T0, . . . , xn = Tni is the symbolic firing mode of the last transition s of S0 on the path to M .
For M4, we obtain DF 0(M4) ≡ true. We add the conjunction DF 0(M3) ∧ DF 0(M4) as a guard to the transition s1 that precedes both M3 and M4 in the SRG. After adding this guard x1 = pn−1(x0) to s1, every deadlock in which q2 is marked becomes unreachable.
We repeat this procedure for s3. M6 is reachable via two paths of the SRG (which differ only insignificantly). The last transition of S0 on both paths is s3 with firing mode hx0 = v1, x1 = pn(v0)i. Analogously, we get
DF 00(M6) ≡ ∀v0, v1 : x0 = v1 ∧ x1 = pn(v0) =⇒ v0 = v1
≡ x1 = pn(x0) In a more general case, we may get a different predicate for each path on which a marking M is reachable. Then DF 0(M ) is the conjunction of these predicates. With DF 00(M7) ≡ true we get the conjunction DF 00(M6) ∧ DF 00(M7) ≡ x1 = pn(x0). After assigning x1 = pn(x0) to s3 as a guard, no deadlock is reachable in which q4 is marked.
Let S1 be the open net derived from S0 by adding the two guards to s1 and s3. These guards introduce new deadlocks in which q2 and q4 are not marked, e. g. [wait.0, q3.3, o.1, d.3] is a deadlock in medic ⊕ S1 but not a deadlock of medic ⊕ S0. These new deadlocks will become unreachable in the next iteration step. In the SRG of medic ⊕ S1 (Fig. 4), M3 has the condition v0 = v1 and M6 has the condition pn(v0) = pn(v1) due to the guards that were added. Therefore we obtain the predicates
DF 01(M2) ≡ ∀v0 : x0 = pn(v0) =⇒ ∃v1 : v0 = v1 ≡ true DF 01(M5) ≡ ∀v0, v1 : x0 = v1 =⇒ pn(v0) = pn(v1) ≡ false orderhe = v0i
Variable v1 is existentially quantified, because v1 is not yet defined in M2 but will be created and chosen appropriately by s1 in the step from M2 to M3. Please note that existential quantifiers may only appear as a part of a DF 0 predicate. o d x0 x0 [true]• s0 q1 q2 x1x0 [xs11= pn−1(x0)]
Eventually, by assigning the predicate DF 01(M2) ≡ true to s0 and DF 01(M5) ≡ false to s2, we obtain the open net S2 shown in Fig. 5a. By repeating our calculation on the SRG of medic ⊕ S2 (Fig.5b), we obtain DF 2(M0) ≡ true. This indicates that no reachable marking in which q0 is marked is a deadlock. Therefore, every deadlock has been eliminated from medic⊕S2 and S2 is a partner of medic by definition. Please note that S2 is very similar to N2 from Fig. 1b. In general, the last open net Si of the sequence is a partner of N iff for every symbolic marking M in which the root place q0 is marked the predicate DF i(M ) is fulfilled for every assignment that fulfils CONDi(M ).
We sketched an algorithm to synthesize a partner of a service represented by a
High-Level Petri net. Currently, our approach is limited to acyclic services. We
show a systematic approach to derive the relations between the values of incoming
and outgoing messages that a service has to adhere to in order to be a partner
of the given service. Since relations are denoted in first-order logic which is
undecidable in the general case, we rely on an oracle to decide controllability. For
a decidable theory like presburger arithmetic [
Lohmann et al. [
In contrast to their approach, our approach does not consider structural aspects of the partner synthesis at all. All information concerning the behaviour of the partner is encoded by the guards. The structure of the partner is chosen in a generic way. However, our approach can handle values that are nondeterministically chosen by the service.
In our future work we aim at extending our approach to cyclic services. In this scenario it may be advantageous to chose a specific structure for the synthesized partner. E. g. case distinctions for specific values should result in a distinct node for each case. With a structure reflecting the behaviour of the service, it will be easier to identify isomorphic branches of the structure and nodes that can be combined without changing the behaviour. In order to ensure termination of the synthesis algorithm in the cyclic case, it is necessary to guarantee that there will be only finitely many nodes after the nodes have been combined.