An operating guideline (OG) for a service S nitely characterizes the (possibly in nite) set of all services that can interact with S without deadlocks. This paper presents a decompositional approach to calculate an OG for a service whose underlying structure is acyclic and contains free-choice con icts. This divide-and-conquer approach promises to be more e cient than the classical OG computation algorithm.
We use open nets [
De nition 1 (Controllability, strategy). Let N be an open net. N is controllable, i there exists an open net M such that N M is weakly terminating. Then M is called a strategy for N . Denote the set of all strategies for N by Strat (N ).
In [
Theorem 1 ([
a, b d a, b
a, b (d) OGN true Example Figure 1 depicts an open net N. The net is controllable, as there exists a strategy M which rst receives either an a or a b message and then responds with a c or a d message, resp. This and all other strategies are characterized by the operating guideline OG N. The conjunction a ^ b annotated to the initial node states that a strategy must be ready to initially both receive an a message and a b message. The node with the true formula is a technical necessity. Though it will never be reached in a composition (e. g., after having received an a message, the further receipt of either a or b is impossible, because N will not send these messages), such respective branches may be still part of a strategy, because they do not jeopardize weak termination. 3
In a Petri net, a place with more than one transition in its postset models a con ict.
De nition 2 (Con ict cluster, free choice). Let x 2 P [ T be a node of a net. The con ict cluster x, denoted by [x], is the minimal set of nodes such that: { x 2 [x]. { If p 2 [x] for a place p 2 P , then p [x].
{ If t 2 [x] for a transition t 2 T , then t [x]. [x] is free choice if for all t; t0 2 [x] \ T holds: either t \ t0 = ; or t = t0.
Given a marking of a net, this marking either enables all transitions in a free choice con ict cluster or none of them. We exploit this property by using the transitions of a free choice con ict cluster to decompose the net. For each possible outcome of the con ict, we de ne one net in which only this transition is present and all others are removed together with their adjacent arcs. De nition 3 (Decomposition). Let N = [P; T; F; m0; ] be an open net and C a free choice con ict cluster of N with C \T = ft1; : : : ; tmg. The decomposition of N w.r.t. C is the set fN1; : : : ; Nmg with Ni = [P; T nft1; : : : ; ti 1; ti+1; : : : ; tmg; F n ((P ft1; : : : ; ti 1; ti+1; : : : ; tmg) [ (ft1; : : : ; ti 1; ti+1; : : : ; tmg P )); m0; ], for i 2 f1; : : : ; mg.
Theorem 2. Let N be a safe acyclic open net and fN1; : : : ; Nmg be its decomposition w.r.t. a free-choice con ict cluster C of N with C \ T = ft1; : : : ; tmg. Then Strat (N ) = Tim=1 Strat (Ni).
Proof. We prove the equality by showing mutual set inclusion.
: Let M 2 Strat (N ). We will show by contradiction that M 2 Tim=1 Strat (Ni).
Assume M 2= Tim=1 Strat (Ni). Then M Ni contains a deadlock for a net Ni. Let m0 ! md be a transition sequence to this deadlock in M Ni. This sequence is also realizable in M N . There, md might activate a transition not present in M Ni, which can only be a transition in (C \ T ) n ftig. As C is a free choice con ict cluster, md also activates ti in M Ni which contradicts the assumption that M Ni contains a deadlock. Consequently, M Ni is deadlock free and M 2 Strat (Ni). Repeating the arguments, we can conclude M 2 Tim=1 Strat (Ni). : Let M 2 Tim=1 Strat (Ni). We will show by contradiction that M 2 Strat (N ).
Assume M 2= Strat (N ). Then M N contains a deadlock. Let m0 ! md be a transition sequence to this deadlock in M N . There are two cases: { contains a transition of C \ T . Then, by de nition of the decomposition, there exists a net Ni such that is realizable in M Ni, because due to safeness and acyclicity, transitions in C \ T can occur at most once in . { contains no transition of C. Then is realizable in M Ni, for any 1 i n.
Both cases would contradict the assumption that M 2 Tim=1 Strat (Ni). Hence, M N is deadlock free and M 2 Strat (N ). tu
Theorem 1 describes the relationship between the strategy set of a service
and its OG. The intersection of strategy sets can be related to OGs using the
product operator [
Theorem 3 ([
Then
This result allows us to express Theorem 2 in terms of operating guidelines: Corollary 1. Let N be a safe acyclic open net and fN1; : : : ; Nmg be its decomposition w.r.t. a free-choice con ict cluster C of N with C \ T = ft1; : : : ; tmg. Then Comply (OG N ) = Comply (OG N1 OGNm ).
We are now able to calculate an operating guideline for N by calculating the operating guidelines for the decomposition of N , followed by calculating the product of the operating guidelines. Note that Theorem 2 does not require the whole net to be free choice, but only the con ict cluster under consideration. t1 p a b c d q1 a a c q3 final
b q2 c a, b true q4 a, b a, b, c, d p t2 b a c d r1 b b d r3 final
a r2 d a, b true r4 a, b a, b, c, d [q2,r4] a a ∧ b [q1,r1] c ∧ true b
a, b c [q4,r2] d ∧ true a, b fitnraule∧ a, b d a, b [q3,r4] fitnraule∧ [q4,r3] [q4,r4] true Example (cont.) The net N in Fig. 1 contains a free choice con ict cluster fp; t1; t2g and can be decomposed into the nets N1 and N2, depicted in Fig. 2. The respective OGs characterize the strategies for the decomposed nets. To determine the intersection of these strategy sets, the product OG N1 OG N2 needs to be constructed. As described earlier, it is the product of the underlying automata, and each state is annotated with the conjunction of the respective formulae. For example, the annotation of state [q1; r1] is the conjunction of the formulae of q1 (a) and r1 (b). The resulting product OG N1 OG N2 is equivalent to OG N (cf. Fig. 1); that is, it characterizes the same set of strategies.
The advantage of the decompositional OG calculation is the reduced complexity of the intermediate results. Though the OGs of the decomposed nets might have more nodes, the state space of the decomposed nets is usually much smaller. Furthermore, the product operator's associativity allows to interleave the OG calculation and the product construction. 4
Though the requirements of Theorem 2 (safeness, acyclicity) are very restrictive,
the decompositional approach to calculate an OG can still be used for industrial
speci cation languages. In the following, we evaluate which features of the
languages BPEL [
BPEL For BPEL there exists a feature-complete Petri net semantics [
BPMN Dijkman et al. [
The nets are acyclic if the control ow is acyclic and no activities with explicit loop annotation are used. Again, many occurring con icts are not free-choice, especially when exception ow is modeled. However, decision gateways can be translated into free choice con icts.
UML-AD UML2 activity diagrams have a very close relationship to BPMN and Petri nets. An activity diagram can be translated into an acyclic Petri net if its control ow is acyclic. In case the diagram contains no lack of synchronization, the translation results a safe Petri net. Additionally, the whole net (i. e., every con ict cluster) is free choice if no pinsets are used.
Table 1 summarizes the language constructs that are forbidden or that guarantee acyclic and safe Petri nets, and that yield free choice con icts. The latter constructs can be used to discover free choice con ict clusters already during the translation of a process described in BPEL, BPMN or UML-AD into Petri nets. This allows for avoiding an a-posteriori discovery of free choice con ict clusters.
We implemented the described decomposition approach in the compiler
BPEL2oWFN [
We presented a decompositional approach that uses free-choice con ict clusters to decompose a safe acyclic open net. The operating guidelines for the resulting nets can be calculated independently and subsequently merged using the product operator. Hence, the calculation can be seen as a divide-and-conquer approach to calculate operating guidelines.
Both the calculation of the OGs for the decomposed nets and the product operators are currently implemented to cope with arbitrary nets and OGs, resp. In future work we plan to adjust these algorithms to exploit the simpler structure of the intermediate constructs. In particular, we plan to study free choice open net, because they can be decomposed into con ict free open nets for which the OG construction should be less complex.
In addition, the requirements of Theorem 2 might be relaxed. For example, the theorem still holds if every transition sequence marks the con ict cluster at most once. This requirement can also be ful lled by open nets which are cyclic or non-safe. 1 Both tools are available for download at http://service-technology.org/tools.