Decomposition-based Verification of Global
Compliance in Process Choreographies
Walid Fdhila
SBA-Research,
Vienna, Austria
Stefanie Rinderle-Ma
Faculty of Computer Science
University of Vienna
Vienna, Austria
stefanie.rinderle-ma@univie.ac.at
David Knuplesch
Institute of Databases and Information Systems
Ulm University
Ulm, Germany
Manfred Reichert
Institute of Databases and Information Systems
Ulm University
Ulm, Germany
Abstract—The verification of global compliance rules (GCR) in
process choreographies (e.g., partner-spanning quality assurance
in supply chains) is crucial and challenging due to the restricted
visibility of the private processes of the collaborating partners.
This paper provides a novel algorithm that decomposes global
compliance rules into assertions that can be verified by the
partners in a distributed way without revealing any private
process details. The decomposition is based on transitivity prop-
erties of the underlying GCR specification. This work uses GCR
based on antecedent and occurrence patterns and illustrates the
transitivity properties based on their specification in first order
predicate logic. It is formally shown that the original GCR can
be reconstructed from the assertions, which ensures the viability
of the approach. The algorithms are prototypically implemented
and applied to several scenarios. The ability of checking global
compliance constitutes a fundamental pillar of any approach
implementing process choreographies with multiple partners.
Index Terms—Distributed and cross-organizational business pro-
cesses, Business rules and compliance management, Business
process compliance, Global compliance rules, Rule decomposition
I. INTRODUCTION
The arrival of technologies such as blockchain and Industry
4.0 has pushed the process-oriented collaboration between
distributed business partners [25], realized by so called process
choreographies. Figure 1 depicts a collaboration diagram of a
supply chain scenario as a composition of the public models
[1] of the partners Manufacturer,Middleman,Special Carrier,
and Supplier. The private models of the partners, in turn,
implement and possibly extend the behavior of the public
models. Private tasks–depicted as dashed boxes in Fig. 1–
are not visible to the partners, whereas public tasks can
realize interaction (message exchange) between two partners.
Although private tasks are usually hidden to other partners,
restrictions over them might exist. In this case, no information
about how and when the task is executed, or how it is con-
nected to the other nodes of the corresponding private model
is visible to the other partners. Usually, this happens when a
collaborating partner imposes the execution of a specific task
which must exist in its private process and comply with a
given rule to another partner. The latter should then assure the
existence of such task, and that it follows the imposed rule.
Assume that the supply chain depicted in Fig. 1 is subject
to a Global Compliance Rule (GCR), which stems from legal
regulations and standards such as GDPR or Sarbanes Oxley.
A GCR constrains actions of multiple partners and/or the
interactions between them. Ensuring the compliance of process
choreographies with a GCR is crucial and challenging [16] as
a partner “only has the visibility of the portion of the process
under its direct control” [26]. In Fig. 1, GCR C1 asks for a
safety check, which is accomplished by a private task at the
Special Carrier. To cope with this issue, assertions can be used.
An assertion (A) is a commitment of a partner guaranteeing
that its private/public process complies with the constraint [8].
In the example, the Middleman agrees to get the permission
of the authority before ordering the sepcial transport (A1).
Special carrier commits to perform a safety check before
transporting the intermediate (A2). Combined, A1 and A2
enable checking GCR C1.
[26] tackles the problem of checking GCR on private tasks
based on IoT-enabled artifacts. The approach presented in this
paper aims to exploit assertions in order to stay independent of
a particular technology such as IoT. The fundamental research
question addressed in this work is as follows:
How to decompose a GCR into derived assertions that can be
checked in a distributed way without violating the privacy of
the involved process partners?
We tackle the question by providing a decomposition algo-
rithm that breaks down the initial GCR into derived assertions.
By combining the derived assertions, in turn, we can re-
construct the original GCR, i.e., the decomposition is lossless.
In turn, the assertions obtained from the decomposition can be
checked by the process partners in a distributed way without
revealing any private details. The decomposition relies on
Manufacturer Middleman
Bulk Buyer .
Special
Carrier
Supplier
Process
order
Order
intermediate
Arrival of
intermediate
Production Final
test
Delivery
of product
Order
Get permission
of authority
FWD order
intermediate
Order
special transport
Safety check
FWD order
intermediate
Order
intermediate
Produce
intermediate
Request
Details
Transport
Details
Prepare
Transport
Order
special transport
Request
Details
Transport
Details
Waybill for
intermediate
Arrival of
intermediate
Waybill for
intermediate
Transport
Intermediate
Transport
intermediate
Get permission
of authority
Safety-Check
Full
quality test
intermediate
Assertion A2 of Middleman
Order specialGet permission
of authority
Assertion A3 of Special carrier
Transport
intermediate
Safety-Check
Public
Task
Special
Carrier
C1: Each transport of the intermediate requires
permission of authority. Further, the transporter
must pass a safety check before.
A1: Middleman assures that he gets permission
of the authority for the special transport
before he orders the special transporter.
A2: Special carrier assures to perform a safety check
before he starts the transport of the intermediate.
Interaction
or Message
Exchange
Assertion
Assertion
Global compliance rules
Private
Task
Quick test
intermediate
Fig. 1. Running example with four process partners: Supply chain (adapted from [8])
transitivity properties of the underlying GCR specification.
In order to remain independent of a certain language and
technology, we rely on simple rules that consist of antecedent
and occurrence patterns. The transitivity properties are shown
by the example of a translation to first order predicate logic.
Similarly, for example, [29] presents declarative patterns based
on Linear Temporal Logic (LTL). As part of the evaluation,
the correctness of the decomposition algorithm is formally
proven. Moreover, the algorithm is prototypically implemented
and its application is demonstrated along basic choreography
scenarios.
The remainder of the paper is structured as follows: Section
II provides fundamentals. Section III-B deals with the de-
composition algorithm and Sect. IV with the correctness of
the algorithm. Sections V and III-A present details on the
implementation and application of the algorithm. Section VI
discusses related work and Section VII summarizes the paper.
II. FUNDAMENTALS AND TRANSITIVITY THEOREM
This section presents definitions and formal backgrounds for
global compliance rules (GCR) over a process choreography y.
A choreography includes three types of overlapping models:
(i) a private model representing the executable process and
including private activities as well as interactions with other
partners, (ii) a public model (also called the interface of the
process) that solely highlights the interactions of a given
partner, and (iii) a choreography model providing a global
view on the interactions between all partners [7].
The interactions of a single partner are described in a public
model. The public model thus serves as public (restricted)
view on the private model of the partner which “describes
the internal logic of a partner including its private activities and
interactions” [4]. In this paper, we assume that the choreog-
raphy yis sound, i.e., structural and behavioral compatibility
between public models and consistency between public and
private models are given [7]. For a formal definition of process
choreography, we refer the reader to Def. 3 in Appendix A.
We opt for expressing a GCR based on antecedence and
consequence patterns. An antecedence pattern specifies when
a GCR over yshall be triggered. In this situation, the desired
behavior of yis described by related consequence patterns.
Based on execution traces capturing all events related to the
enactment of y, antecedence and consequence patterns are
interpreted as follows: for each match of the antecedence
pattern there must be at least one match of a consequence
pattern. This simple representation of GCR abstracts from a
certain language and technology, i.e., any language can be cho-
sen that supports antecedence and consequence patterns, and
the transitivity properties defined in this paper. Antecedence
and consequence patterns are specified using occurrence and
absence nodes, which either express the occurrence or ab-
sence of events related to the execution of activities or the
exchange of messages in y. We use the following notation:
A: Antecedence occurrence; A: Antecedence absence; A:
Consequence occurrence; A: Consequence absence
In a previous work [6], multiple formal languages employed
for business process compliance modelling and checking (e.g.,
linear temporal logic LTL, event calculus EC, extended com-
pliance rule graph eCRG) were compared. It was proven that
most of these languages can deal with most qualitative time
patterns, and can therefore be used to model the compliance
constructs addressed in this paper. Similar results were proven
in [14]. In order to specify these constructs as well as
transitivity properties required for the GCR decomposition,
this work uses the eCRG formalism [21]. The latter offers
a visual rule notation for expressing compliance rule graphs
over choreographies and is based on first order predicate logic.
Definition 1 specifies those parts of the eCRG formalism that
are necessary for defining GCRs and their decompositions.
In detail, Def. 1 (i) refers to activities and interactions in y,
(ii) allows for exactly one antecedence occurrence pattern per
rule, and (iii) assumes the rules to be structured as trees. As the
decomposition focuses on the interactions between the partners
and their control flows, (i) does not impose any restriction.
Moreover, (iii) contributes to simplify the algorithm. For the
sake of space and simplicity, we restrict the definition of GCR
to one antecedence occurrence pattern (ii), but will extend this
in future work.
Definition 1 (GCR structure): Given a process choreography
y(cf. Def. 3 in Appendix A), let Abe the set of public
and private activities and Ibe the set of interactions in
choreography model G. Then: a GCR ris defined as tree
r= (N, ρ, ϕ, type, pattern, root)with
•Nbeing the set of nodes,
•ρ:N→ {p1...pn}returning the partner responsible for
a node.
•ϕ:N×N→ { 99K,−→} returning the sequence flow
connector of two nodes, i.e., consequence sequence and
antecedence sequence connectors respectively.
•type :N→ A ∪ I mapping each node to an activity or
an interaction, i.e., message exchange.
•pattern :N→ { A,A,C,C}
•root ∈Nbeing the root node with pattern(root) = A
•∀n∈N\ {root}:pattern(n)6=A
•∀n∈Nwith pattern(n) ∈ { A,C}: n is leaf node
We illustrate the translation of a GCR into a First Order
Logic (FOL) expression using basic equivalences as in Def. 2
following below. As shown in the following, equivalences are
also required for ensuring correctness of the decomposition.
Additionally, throughout the paper we consider the conse-
quence sequence connector. This can be easily extended to
antecedence sequence connectors.
Definition 2 (Basic Equivalences): Based on [22] the
following equivalences hold by definition. Predicate x(t, ty)
describes that at the point in time tan activity (message) of
type ty was executed (i.e., sent or received).
•A99K B:⇔ ∀a:x(a, A)→∃b: (x(b, B)∧a<b)
⇔ ∀a∃b:x(a, A)→(x(b, B)∧a<b)
•A99K B:⇔ ∀b:x(b, B)→∃a: (x(a, A)∧a<b)
⇔ ∀b∃a:x(b, B)→(x(a, A)∧a<b)
•A99K B:⇔ ∀a:
x(a, A)→@b: (x(b, B)∧a<b)
⇔ ∀a, b :x(a, A)→ ¬(x(b, B)∧a < b)
⇔ ∀a, b :x(a, A)→(¬x(b, B)∨b≤a)
•A99K B:⇔ ∀b:
x(b, B)→@a: (x(a, A)∧a < b)
⇔ ∀b, a :x(b, B)→ ¬(x(a, A)∧ ¬a < b)
⇔ ∀a, b :x(a, A)→(¬x(b, B)∨b≤a)
For example, GCR Production 99K Final test is translated
into: ∀a:x(a, Production)→ ∃b:x(b, Final test)∧a < b.
Relation <expresses a temporal precedence between aand b.
The decomposition algorithm presented in Sect. III-B exploits
the transitivities for GRC as in Theorem 1. Specifically, by
combining transitive relations, where each relation can be
checked locally by a single partner, it becomes possible to
reconstruct the original GCR behavior. Theorem 1 ensures that
the behavior of the derived assertions reproduces the behavior
of the GCR, but not vice versa.
Theorem 1 (Transitivities):
Let A, B, and Cbe three activity or message types. Then:
a. The rightwards transitivity holds:
A99K B∧B99K C⇒A99K C
b. The leftwards transitivity holds:
A99K B∧B99K C⇒A99K C
c. The rightwards zig zag transitivity holds for the conse-
quence absence:
B99K A∧B99K C⇒A99K C
d. The leftwards transitivity holds for the consequence ab-
sence:
A99K B∧C99K B⇒C99K A
In the following, the correctness of Theorem 1 is proven
applying Def. 2.
Proof 1 (Rightwards Transitivity): Let A, B, C be three
activities or interactions. Then A99K B∧B99K C
:⇔ ∀a∃b:x(a, A)→(x(b, B)∧a < b)∧∀b∃c:
x(b, B)→(x(c, C)∧b<c)
⇔ ∀a∃b:x(a, A)→(x(b, B)∧a<b)∧∀b:∃c:
x(b, B)→(x(c, C)∧b < c)
⇒ ∀a∃b, c :x(a, A)→(x(b, B)∧a<b)∧x(b, B)→
(x(c, C)∧b < c)
⇒ ∀a∃b, c :x(a, A)→x(b, B)→(x(c, C)∧a < b <
c)
⇒ ∀a∃c:x(a, A)→(x(c, C)∧a < c)⇒A99K C
q.e.d.
Leftwards transitivity can be proven similarly by replacing ’<’
with ’>’.
Corollary 1: Let A, B, C, and Dbe activities or interactions.
Then
A99K B∧B99K C∧C99K D⇒A99K C∧C99K D
⇒A99K D
Proof 2 (Rightwards Zig Zag Transitivity of Absence): Let
A, B, C be activities or interactions. Then:
B99K A∧B99K C
:⇔ ∀a∃b:x(a, A)→(x(b, B)∧b < a)∧ ∀b, c :
x(b, B)→(¬x(c, C)∨c≤b)
⇔ ∀a∃b:x(a, A)→(x(b, B)∧b < a)∧ ∀b, c :
x(b, B)→(¬x(c, C)∨c≤b)
⇒ ∀a∃b∀c:x(a, A)→(x(b, B)∧b<a)∧x(b, B)→
(x(c, C)→c≤b)
⇒ ∀a∃b∀c:x(a, A)→x(b, B)→(x(c, C)→c≤b <
a)
⇒ ∀a∀c:x(a, A)→(x(c, C)→c≤a)
⇒ ∀a, c :x(a, A)→(¬x(c, C)∨c≤a)⇒A99K C
q.e.d.
Leftwards zig zag transitivity of absence can be proven sim-
ilarly by replacing ’<’ with ’>’ and ’≤’ with ’≥’. The
transitivity of other constructs such as “chaining” or “requires
transitivity” can be found in Appendix B.
III. DECOMPOSING GLOBAL COMPLIANCE RULES
At design time, checking a GCR that solely refers to inter-
actions and/or public activities can be achieved by applying
contemporary compliance checking techniques (cf. [13]) either
on the choreography model or the public models of the
involved partners. By contrast, if a GCR refers to private
activities of different partners, it becomes impossible to check
its correctness as partners cannot view the private process
parts of the other partners and, therefore, cannot identify
the dependencies between the private activities involved in
the GCR. To cope with this, we suggest decomposing the
GCR into a set of assertions of which each can be checked
locally by the corresponding partner. The decomposed rules
then reproduce the behavior of the original GCR.
Decomposition in compliance checking has been exploited
by [32], but only at the process model level in order to
achieve performance gains for the compliance checks. The
paper at hand, first of all, proposes to decompose the global
compliance rule to distribute the compliance checks to the
partners for maintaining the confidentiality of their private
tasks. We start with illustrating the idea and the challenges
of GCR decomposition based on different scenarios. Then the
decomposition algorithm is introduced and explained.
A. GCR Decomposition Scenarios and Discussion
In the following, we use a set of scenarios (cf. Figs. 2 and 3)
to illustrate the GCR decomposition process. For the sake of
readability, in these scenarios we assume a simple compliance
rule involving two tasks of two different partners p1and p2.
In Scenarios 1 – 3, we assume rule A99K B, where the
execution of task Ashall be followed by the one of task B.
For simplicity, we use labels A,B,m1,m2,p1and p2instead
of the actual labels taken from the example of Fig. 1.
•In Scenario 1 there exists a message exchange m1
between p1and p2that fulfills conditions A99K m1and
m199K B. The behavioral and structural compatibility
(cf. Sect. II) between the partner processes ensures that
message m1sent by p1shall be correctly received by p2.
•In Scenario 2 we assume that there is no direct interaction
between p1and p2, but there exists a transitive interaction
through partner p3. Partner p1interacts with p3through
m1and p3interacts with p2through m2. In this sce-
nario, the transitive relations A99K m1,m199K m2,
and m299K Breproduce the behavior of A99K B.
Consequently, partner p3, which is initially not involved
in the GCR becomes involved in the derived assertions.
We call p3an intermediary partner.
•In Scenario 3 we assume that, even though there are
interactions between p1and p2, no direct or transitive
interactions reproduce the behavior of A99K B. As such,
additional message exchanges become necessary to in-
form about the execution state of activities involved in the
GCR. Message exchanges can be either synchronous or
asynchronous. Asynchronous message exchange only al-
lows for reactive GCR checking and, hence, for detecting
violations after their occurrence. Synchronous message
exchange is proactive as it enforces the GCR with new
restrictions to the process models, e.g., the execution of
Bis enabled only after receiving the synchronization
message (i.e. whether Ais or is not executed). Partner
p1shall also inform p2in case Ais not executed, as this
does not prevent Bfrom being executed according to the
GCR.
Rightwards transitivity (cf. Theorem 1.a) directly ensures the
correctness of Scenarios 1 and 3 from Figure 4. It should be
clear that the correctness of Scenario 2 can be directly derived
from Corollary 1 (cf. Sect. II).
For the scenarios depicted in Figure 3, we assume differ-
ent compliance rules, where the antecedent presence B
implies the later consequence absence Ain Scenario 4;
i.e., B99K A, and antecedence presence Brequires the
consequence presence Abefore, in Scenario 5, i.e., A99K B.
•In Scenario 4 (includes an adaptation of the example
of Fig. 1), for partner p1, the execution of Aauto-
matically implies non-execution of m1before and vice
versa (due to the used XOR pattern). Consequently, it
ensures rule m199K A. For partner p2, the execution of
Bis always preceded by the one of m1, which implies
m199K B. The composition of the two rules m199K A
and m199K B, in turn, reproduces the behavior of
B99K A. Similarly to Scenario 2, this dependency can
become more complex and transitive. This example also
Order
special transport
Safety check
Get permission
of authority
Get permission
of authority
Order
special transport
Produce
intermediate
Get permission
of authority
Process Order
Order
intermediate FWD order
intermediate
Order
intermediate
FWD order
intermediate Get permission
of authority
Prepare
Transport
Waybill for
intermediate
Get permission
of authority
Safety Check
Waybill for
intermediate
Middleman - P1 Manufacturer - P1
Special Carrier- P2 Supplier - P2Middleman - P3 Special Carrier - P2Supplier - P1
sync
+
A
B
m1 m1 m2
m1
AA
B
B
Scenario (3)
Scenario (1) Scenario (2)
Fig. 2. Scenarios 1–3
m1
Get permission
of authority
Transport
intermediate
Get permission
of authority
Order
special transport
Get permission
of authority
Order
special transport
Get permission
of authority
Quick test
intermediate
Arrival of
intermediate
Arrival of
intermediate
Transport
intermediate
Quick test
intermediate
Scenario (4) Scenario (5)
B
A
A
B
Special Carrier- P1 Manufacturer - P2 Manufacturer - P2Special Carrier- P1
m1
Fig. 3. Scenarios 4–5
illustrates A99K Band A99K Bin a similar way.
•In Scenario 5, if Bis executed, Ashould have been
executed before. However, the execution of Adoes not
imply that Bis always executed. Regarding p1, the
execution of Aimplies the one of m1and vice versa; i.e.,
A99K m1and A99K m1. Regarding p2, the execution
of Balways implies the one of m1before, but not the
other way around; i.e. m199K B. Since both assertions
refer to the same message exchange m1between p1and
p2, in combination with each other, the two assertions
A99K m1and m199K Bcan reproduce the behavior
of A99K B
The correctness of Scenario 5 concludes from the rightwards
transitivity (cf. Theorem 1.b), whereas Scenario 4 relies on
the zig zag transitivity of the absence (cf. Theorem 1.c).
Figure 4 summarizes the decomposition results of the sketched
scenarios. The latter are used to illustrate selected use cases.
The decomposition process is not limited to these scenarios
and, as aforementioned, the decomposition cannot always be
automated, but might require manual interaction and process-
ing. Altogether, the decomposition eases global compliance
rule checking, where each partner checks its corresponding
derived assertions locally. A GCR is rechecked only if at least
one of the derived assertions is not evaluated to true. Note that
this does not necessarily imply that the GCR is violated.
B. GCR Decomposition Algorithm
This section focuses on the decomposition algorithm and
explains the steps to derive assertions using transitivities.
Algorithm 1 realizes GCR decomposition as set out in Def.
1. It assumes that each node of the GCR is assigned to one
partner being responsible for it. Further on, we assume the
input GCR to be consistent and satisfiable (for dealing with
unsatisfiable and inconsistent rules we refer to [5]). In the
following, we first explain Algorithm 1 step by step and then
illustrate the entire algorithm along Example 1 (see below).
Starting from the Anode (cf. Def. 1), Algorithm 1 walks
outwards through all other nodes of the GCR. Thereby, the
visited parts are copied and become assertions. Wherever
the algorithm walks over a connector between two nodes
nand s, which are assigned to different partners ρ(n)and
ρ(s), the GCR is split at this position as this dependency
cannot be evaluated by a single partner. Next, the algorithm
tries to replicate the connector where the GCR was split
through (transitive) message exchanges between both affected
partners by applying the transitive relationships from Section
II. Therefore, sets n•,•s, and Θare calculated. Depending on
the pattern of s(cf. Def. 1), n•and •scontain the messages
succeeding or preceding nand s. Note that these calculations
have to be accomplished in a decentralized manner by ρ(n)
and ρ(s)themselves as nand smay be private tasks. Next, Θ
combines those messages of n•and •sthat can be combined.
If sis a Cnode (i.e., smust follow n), Θcontains message
tuples (m1, m2)that ensure that nis always followed by
m1,m1by m2(unless m1=m2), and m2by s. Any pair
(m1, m2)∈Θcan then be used to complement the created
assertions, i.e., m1becomes a placeholder for swithin the
assertion of ρ(n), whereas m2replaces nfor ρ(s).
Regarding Cnodes (i.e., smust not follow n), all pairs of
messages (m1, m2)∈Θensure that nis preceded by m1
in any case and m1is preceded by m2(unless m1=m2),
whereas snever follows m2. Finally, for Anodes an
occurrence of safter nallows ignoring the rule. Hence, A
nodes result in pairs (m1, m2)such that m1may only occur
after nand m2may only occur after m1(unless m1=m2).
However, there should be at least one case in which m2is
followed by s(i.e., sis not always preceded by m2).
Finally, all assertions of the same partner, which depend on
the same Amessage, are merged to reduce the number
of assertions. Remaining assertions without consequences are
removed as they result from the processing of Anodes, but
have not been merged in the previous step. Remember that
ignoring Anodes is allowed as this makes rules even more
strict.
Example 1: Let us apply Alg. 1 to GCR C1 from the running
example in Fig. 1. Let the responsibilities be ρ(Safety Check)
=Special Carrier,ρ(Get permission of authority) = Middle-
man, and ρ(Transport intermediate) = Special Carrier. After
assigning responsibilities (cf. labels above the nodes), Algo-
rithm 1 starts with Anode Transport intermediate and creates
a new assertion for the Special Carrier who is responsible for
this task. Then the Safety check is discovered and added to the
assertion, since it belongs to the same partner. In turn, another
partner (i.e., Middleman) is responsible for task Get permission
of authority. Hence, the algorithm cuts the respective con-
nector and creates a new assertion for the respective partner.
Next, Special Carrier and Middleman determine n•and •s
with n•={Waybill,T. Details,Req. Details,Order ST}and
•s={Order ST}to calculate those message pairs Θ =
{(Waybill,Order ST),...,(Order ST,Order ST)}that can be
used to transitively replicate the connector where the GCR
was split. Finally, the algorithm places the selected messages
into both assertions in such a way that the correctness of the
original rule is preserved through the (leftwards) transitivity
of eCRGs. Note that the Special Carrier could use message
Waybill instead since (Waybill,Order ST)∈Θholds.
For the same GCR, it is possible to infer several decom-
positions, depending on which interactions are used to find
a transitive control flow relationship between the nodes of
the GCR. It is also possible that no direct link can be
identified between two partners’ GCR nodes (i.e., there is no
interaction between those two partners). As such, interactions
with intermediary partners can be used to find an indirect link
(i.e., transitive interactions). As aforementioned, if no transi-
tivity is identified between the GCR nodes of two partners
(even not through intermediary partners), it becomes necessary
to exchange additional execution data between the partners
involved in the GCR, by, for example, adding sync messages.
Sync messages are specific type of messages communicated
between partners to inform about the state of a given task (e.g.,
terminated, started, not executed). Although sync messages
are not preferred as they expose private data about the exact
execution time of a private task, they become necessary
when the GCR cannot be decomposed into assertions, i.e.,
no transitive relations can be identified.
IV. CORRECTNESS AND COMPLEXITY OF GCR
DECOMPOSITION
At first, this section formally proves the correctness of the
GCR decomposition into assertions (cf. Alg. 1). In detail, it
is shown that we can reconstruct the original GCR from the
assertions, i.e., the decomposition is lossless1.
Let ∆=(N, ρ, ϕ, type, pattern, root)be a GCR (cf. Def.
1). For ∆, a partner pmight be responsible (cf. Alg. 1) for
multiple nodes within N, e.g., if multiple nodes of Nbelong
to the process of p. In this scenario, the decomposition of ∆
might result in multiple sub GCRc (subgraphs) to be checked
by p, in particular if the nodes of pare dispersed over ∆and
are not directly connected. Let {∆i}pbe the set of sub GCRs
issued from the decomposition and involving partner p.
Let’s consider two nodes nand n0∈N, the corre-
sponding connector ϕ(n, n0), and Ψ(n, n0)= (pattern(n),
pattern(n0),ϕ(n, n0)) as the corresponding assertion. Now as-
sume there exists a set of message interaction nodes {mk}k=h
k=1 ,
such as Ψ(n, m1)≡Ψ(mk−1, mk)k=h
k=2 ≡Ψ(mh, n0)≡
1Note: For the sake of simplicity, the notation
A99K B:⇔ ∀a:x(a, A)→∃b: (x(b, B)∧a<b)
has been simplified to: A99K B:⇔ ∀a→ ∃b∧a<b)
Scenario
Global
Compliance
Rule (GCR)
Derived
Assertions (AR) Scenario
Global
Compliance
Rule (GCR)
Derived
Assertions (AR)
(1) A, p199K B, p2
A, p199K m1, p1
m1, p299K B, p2
(2) A, p199K B, p2
A, p199K m1, p1
m1, p399K m2, p3
m2, p299K B, p2
(3) A, p199K B, p2
A, p199K sync, p1
sync, p299K B, p2
(4) B, p299K A, p1
m1, p199K A, p1
m1, p299K B, p2
(5) A, p199K B, p2
A, p199K m1, p1
m1, p299K B, p2
Fig. 4. GCR Decomposition Results
Algorithm 1: GCR decomposition DECOMPOSE(gcr)
•Global compliance rule gcr = (N, ρ, ϕ, type, pattern, root)
•Choreography model y, and Mas the set of all partners’ message nodes.
•We assume that ρalso returns the partner private model of a node n.
select the only a∈Nwith pattern(a) = A
initialize queue Q← {a}
create (incomplete) Assertion Aa←”a”for the partner associated with
ρ(a)
foreach (n←removeHead(Q)) do
foreach (s∈Nwith ϕ(n, s)6=∅)do
Q←Q∪ {s}
if (ρ(n) = ρ(s)) then
//nand sinvolve the same partner
initialize As←@Anas reference on An
if (pattern(s) = A)then extend Aswith ”99K s”
if (pattern(s) = C)then extend Aswith ”99K s”
if (pattern(s) = C)then extend Aswith ”99K s”
else
//nand sinvolve different partners pi,pj
if (pattern(s) = C)then
n•←{m∈ρ(n)|m∈ M, ρ(n)|=n99K m}
•s← {m∈ρ(s)|m∈ M, ρ(s)|=m99K s}
Θ← {(mn, ms)∈(n•×•s)|γ|=mn99K ms}
if (pattern(s) = C)then
n•←{m∈ρ(n)|m∈ M, ρ(n)|=m99K n}
•s← {m∈ρ(n)|m∈ M, ρ(n)|=m99K s}
Θ← {(mn, ms)∈(n•×•s)|γ|=ms99K mn}
if (pattern(s) = A)}then
n•←{m∈ρ(n)|m∈ M, ρ(n)|=n99K m}
•s← {m∈ρ(s)|m∈ M, ρ(s)6|=m99K s}
Θ← {(mn, ms)∈(n•×•s)|γ|=mn99K ms}
if (Θ ∪(n•∩•s) = {∅})then
//No implicit dependency between nand s
add sync message between nand s
update models p1,...,pn, and γ
recalculate n•,•s, and Θ
else
//implicit dependency mbetween nand sexists
select (mn, ms)∈Θ∪(n•∩•s)2
if (pattern(s) = C)then
extend Anwith ”99K mn”
create Assertion As←”ms99K s”for ρ(s)
if (pattern(s) = C)then
extend Aswith ”mn99K ”
create Assertion As←”ms99K s”for ρ(s)
if (pattern(s) = A)then
create Assertion As←”ms→s”for ρ(s)
foreach ((s∈Nwith ϕ(n, s)6=∅)) do
//same as for each (n, s)∈Cabove
//but with flipped directions
foreach (partner i)do
foreach ((Aj, Ak)of partner i)do
if (Aj, Akhave the same Apattern)then
merge Ajand Akbased on the Apattern
foreach (Assertion A)do
if (Ahas empty Cand Cpatterns)then remove A
Ψ(n, n0), where Ψ(n, m1)≡Ψ(n, m1)if and only if pat-
tern(a) = pattern(c) and pattern (b)=pattern(d) and ϕ(a, b) =
ϕ(c, d). Then according to Theorem 1 it holds:
Ψ(n, m1)[
k=h
^
k=2
Ψ(mk−1, mk)] ∧Ψ(mh, n0) =⇒Ψ(n, n0)
This implies that the first assertion can be decomposed into
a conjunction of finite sets of transitive relations. If there
exists a message interaction mthat transitively ensures the
original relation between niand nj,Ψ(ni, nj)is decom-
posed into Ψ(ni, send(m)) ∧Ψ(send(m), receive(m)) ∧
Ψ(receive(m), nj). For the sake of simplicity, we directly
use Ψ(ni, m)∧Ψ(m, nj). Doing so is possible due to the
compatibility property in process collaborations that ensures
that each send task of one partner is necessarily connected
to a receive task of another one. Note that a node n∈N
is not always solely connected to one single node, but may
have multiple connections defining its semantics. For example,
regarding GCR C1(cf. Fig. 1), Transport Intermediate has two
incoming connectors. We call such a node an inner node. In
the following, we are interested in proving that the semantics
of such nodes are preserved after decomposition. For the sake
of readability, we consider a GCR composed of one single
inner node of type A. However, the proof can be extended to
multiple composite nodes and different node types (e.g., C
A), following the same logic. We define •nand n•as the set
of all nodes preceding and succeeding nrespectively. Consider
a composite node nof type A, which is preceded by two
sets of antecedence and consequence occurrence nodes (i.e.,
•Aand •Crespectively), and followed by two other sets of
antecedence and consequence occurrence nodes (i.e., A•and
C•respectively). Assume •A={ai}, A•={bj},•C={ck},
and C•={dl}, then the generic FOL formula for such a node
is given as follows [22]:
∀ai,∀bj,∀n:Vi(ai< n)Vj(n<bj)→ ∃ck,∃dl:Vk(ck<
n)Vl(n<dl)
Using Theorem 1 each relation of type nprecedes n0(n<n0);
if there exists a message interaction msuch as n<mand
m<n0, then:
∀ai,∃mi,∀bj,∃mj,∀n:Vi(ai< mi)Vi(mi< n)Vj(n <
mj)Vj(mj< n)→
∃ck, mk,∃dl, ml:Vk(ck< mk)Vk(mk< n)Vl(n <
ml)Vl(ml< n)
⇐
Vi(ai→mi)
Vj(mj→bj)
[∀mi,∀mj,∀n:Vj(mi< n)Vj(n<mj)
→ ∃mk,∃ml:Vk(mk< n)Vl(n<ml)∃ck,∃dl:Vk(ck<
mk)Vl(ml< n)]
⇐
Vi(ai→mi)
Vj(mj→bj)
[∀mi,∀mj,∀n:Vj(mi< n)Vj(n<mj)
→ ∃mk,∃ml:Vk(mk< n)Vl(n<ml)∀ck,∀dl:Vk(ck<
mk)Vl(ml< n)]
⇐
Vi(ai→mi)
Vj(mj→bj)
[∀mi,∀mj,∀n:Vj(mi< n)Vj(n<mj)
→ ∃mk,∃ml:Vk(mk< n)Vl(n<ml)Vi(ck→mk)
Vj(ml→dl)
The latter equation corresponds to the decomposition result
produced by Alg. 1, i.e., the decomposition is lossless. Note
that the decomposition is even stronger than the initial GCR,
as it adds compliance on additional messages and enables
distributed compliance checking.
In the following, we discuss the complexity of the GCR
decomposition in Alg. 1. Results on checking regulatory
compliance in general have been provided in [31]. The first
and second loops iterate over the nodes of the compliance
rule. If we consider that two nodes can only have one flow
connector, then the number of required operations will be
nn−1
2, otherwise n(n−1). In both cases complexity is O(n2).
The first if statement is O(1), whereas the else statement
calculates n•,•sand θeach with a worst case complexity
of O(n2). The second inner loop has the same complexity as
the first inner loop. The third nested inner loop iterates over
partners and compare assertions within the same partner with
a number of operations equal to n×mm−1
2, which gives a
complexity of O(n3). The last inner loop has a complexity
of O(n). Obviously, the overall worst case complexity of the
algorithm is polynomial O(n4); i.e., outer loop combined with
the third nested inner loop.
V. IMPLEMENTATION AND DISCUSSION
The presented approach was implemented as part of the C3Pro
framework2, which deals with change and compliance in pro-
cess choreographies [7]. The framework provides sophisticated
functions for defining, propagating and negotiating changes in
the context of process choreographies. Furthermore, it com-
prises a modeling component as one of its core components
for editing and changing process changes, as well as for
visualizing change propagations. In the context of the present
work, the three-layer architecture of the framework [7] (i.e.,
process definition, change and execution) was extended with
an additional layer dealing with compliance.
Figure 5 depicts the main components of the C3Pro frame-
work. The compliance and process modeling environments
allow defining and editing compliable process choreography
models [18], [20]. Compliability was introduced as “a se-
mantic correctness criterion to be considered when designing
interaction models. It ensures that interaction models do not
conflict with the set of imposed global compliance rules” [20].
At design time, it is ensured that the created choreography
models are compliant with the various compliance rules. The
change editor allows defining and editing changes with respect
to process models as well as compliance rules.
2http://www.wst.univie.ac.at/communities/c3pro/
LCR
(Local Compliance Rule) Assertion GCR
(Global Compliance Rule)
Private Model Public Model Choreography
Model
Compliance
Modeling
environment
(DME)
Process
Modeling
environment
(PME)
Change Editor
(CE)
Change
Management
Service
Change
Negotiation
Service
Compliance
Management
Service
Execution
Log
Monitoring
Service
Violations
Log
Change
Log
Execution
Engine
Fig. 5. C3Pro Prototype Architecture
The compliance management service handles the defined
compliance rules and implements the GCR decomposition
algorithm (cf. Section III-B). As process execution engine
we utilized CPEE3. Most functions of the C3Pro framework
are provided as a RESTful service, which enables unified
access from any client being able to communicate via HTTP.
Finally, the Compliance Management Service serves as a
pluggable middleware that may be used to integrate other
process execution engines.
For testing the framework, we edited choreography and col-
laboration models in BPMN 2.0 using Signavio4and exported
them to the C3Pro framework as XML files. Examples are
extended with GCR, which are then decomposed into derived
assertions using Alg. 1.
Applicability and discussion: The implementation of the
decomposition algorithm takes two aspects into consideration:
(i) the distributed execution of the processes, and (ii) the
different visibility levels of tasks and control flow (privacy).
The algorithm is initiated by the partners that share a GCR.
As private tasks and their dependencies are not visible to
all collaborators, parts of the decomposition algorithm are
executed locally by all partners involved in this GCR to
identify possible transitive relations between their correspond-
ing private tasks and possible public tasks or interactions
that replicate the connector where the GCR was split. This
results in multiple derived assertion alternatives, which are
then aggregated to alternatives from other partners in order to
find a combination that recreates the original rule as described
in Section III-B (cf. Example 1). Once the GCR is decomposed
and the corresponding assertions are derived, each partner
locally checks its derived assertions at runtime.
Note that this paper focuses solely on structural compliance.
Compliance patterns that deal with data and resources are
future work. In addition, the presence of XOR branches in the
processes (where sending of messages on these branches is
optional) does not affect the correctness of the decomposition
as long as the processes are compliable with the original GCR
3http://cpee.org
4http://academic.signavio.com/
[20]. As aforementioned, we assume the soundness of the
different process models (i.e., consistency and compatibility)
and their compliability to the original GCR. This means that
original GCR are correctly specified, and the decomposition
enables their checking in a distributed way. In this case,
transitivity ensures correct decomposition of GCR even at
the presence of XOR branches. If no transitive relations are
identified, then sync messages are required.
VI. RELATED WORK
This work is positioned at the interface between process
choreographies and process compliance. Process choreography
research has been concerned with modeling choreographies
and verifying their correctness (for an overview see [33]).
Business process compliance, in turn, has been investigated
for many years and several surveys exist (e.g., [3], [9]). In
particular, existing approaches have dealt with compliance rule
notations, including visual notations [2], [21], logic-based for-
malisms [24], and Event Calculus [27]. Moreover, approaches
target at design and runtime compliance checking (see, e.g.,
[3], [23]) and different process perspectives such as time
[30]. The following approaches address the interface between
process choreographies and compliance: [15] advocates DCF
Graphs for decomposing global contracts into local processes.
[12] provides means to model contractual constraints. Com-
pliance checking mechanisms assuming a trusted party are
proposed by [11]. A distributed approach, which relies on IoT
technology, is suggested by [26]. [34] assumes that partners
try to provide wrong information and, hence, introduce the
notion of accountability. [17] advocates compliance checking
in process choreographies as crucial, but it cannot be assessed
in how far the approach deals with the restricted visibility and
availability of process information. In prior work, we have
introduced the criterion of compliability [20] that captures
the ability of a choreography to comply with a given set of
compliance rules at all and how to check it [18]. [19] allows
for checking effects of changes on compliance in process
choreographies based on dependency graphs between global
and local compliance rules as well as assertions. Finally, [8]
provides an overview on the challenges, related approaches,
and possible solutions at the interplay of compliance, change,
and choreographies.
VII. CONCLUSION
The research question set out in the introduction is how to de-
compose a GCR into derived assertions that can be checked in
a distributed way without violating the privacy of the involved
process partners?
We provided a novel algorithm that decomposes GCR into
assertions, which – as a particular benefit of the approach –
can be checked by the partners in a distributed way and, hence,
do not require any sensitive information to be exchanged at
the choreography level. The correctness of the algorithm, and
hence a formal evaluation, was accomplished as follows: based
on the derived assertions the original GCR (or a stricter one)
can be reconstructed. As a current limitation we assume that
GCRs consist of exactly one antecedence pattern, i.e., a pattern
triggering the rule. While a collection of scenarios is supported
by such rules, future work will extend the algorithm and the
formal proof to GCR with an arbitrary number of antecedence
patterns. In future work, we will further elaborate a full-
blown prototype and demonstration environment including
the implementation of real-world scenarios. As a promising
application area we have identified the manufacturing domain
as indicated by the running example. Others include health-
care and logistics where complex networks are subject to a
multitude of regulations and demand for adaptations at the
same time. Furthermore, we plan to adapt our algorithms to
other languages that are used to specify compliance rules (e.g.,
Declare [28], PENELOPE [10], or BPMN-Q [2]).
REFERENCES
[1] van der Aalst, W.M.P., Lohmann, N., Massuthe, P., Stahl, C., Wolf,
K.: Multiparty contracts: Agreeing and implementing interorganizational
processes. Comput. J. 53(1), 90–106 (2010)
[2] Awad, A., Weidlich, M., Weske, M.: Visually specifying compliance
rules and explaining their violations for business processes. Journal of
Visual Languages & Computing 22(1), 30–55 (2011)
[3] Becker, J., Delfmann, P., Eggert, M., Schwittay, S.: Generalizability
and applicability of model-based business process compliance-checking
approaches - a state-of-the-art analysis and research roadmap. Bus Res
5(2), 221–247 (2012)
[4] Bischoff, F., Fdhila, W., Rinderle-Ma, S.: Generation and transformation
of compliant process collaboration models to BPMN. In: Advanced
Information Systems Engineering. pp. 462–478 (2019)
[5] Ciccio, C.D., Maggi, F.M., Montali, M., Mendling, J.: Resolving incon-
sistencies and redundancies in declarative process models. Inf. Syst. 64,
425–446 (2017)
[6] Fdhila, W., Gall, M., Rinderle-Ma, S., Mangler, J., Indiono, C.: Classi-
fication and formalization of instance-spanning constraints in process-
driven applications. In: BPM. pp. 348–364 (2016)
[7] Fdhila, W., Indiono, C., Rinderle-Ma, S., Reichert, M.: Dealing with
change in process choreographies: Design and implementation of prop-
agation algorithms. Inf Sys 49, 1 – 24 (2015)
[8] Fdhila, W., Rinderle-Ma, S., Knuplesch, D., Reichert, M.: Change and
compliance in collaborative processes. In: SCC. pp. 162–169 (2015)
[9] Fellmann, M., Zasada, A.: State-of-the-art of business process compli-
ance approaches. In: ECIS (2014)
[10] Goedertier, S., Vanthienen, J.: Designing compliant business processes
with obligations and permissions. In: BPM’06 Workshops. pp. 5–14
(2006)
[11] Gonz´
alez, L., Ruggia, R.: A comprehensive approach to compliance
management in inter-organizational service integration platforms. In:
ICSOFT. pp. 722–730 (2018)
[12] Governatori, G., Idelberger, F., Milosevic, Z., Riveret, R., Sartor, G., Xu,
X.: On legal contracts, imperative and declarative smart contracts, and
blockchain systems. Artif. Intell. Law 26(4), 377–409 (2018)
[13] Hashmi, M., Governatori, G., Lam, H., Wynn, M.T.: Are we done with
business process compliance: state of the art and challenges ahead.
Knowl. Inf. Syst. 57(1), 79–133 (2018)
[14] Hashmi, M., Governatori, G., Wynn, M.T.: Normative requirements
for regulatory compliance: An abstract formal framework. Information
Systems Frontiers 18(3), 429–455 (2016)
[15] Hildebrandt, T.T., Mukkamala, R.R., Slaats, T., Zanitti, F.: Contracts
for cross-organizational workflows as timed dynamic condition response
graphs. J. Log. Algebraic Methods Program. 82(5-7), 164–185 (2013)
[16] Kasse, J.P., Xu, L., de Vrieze, P., Bai, Y.: The need for compliance
verification in collaborative business processes. In: PRO-VE. pp. 217–
229 (2018)
[17] Kasse, J.P., Xu, L., de Vrieze, P., Bai, Y.: Verifying for compliance to
data constraints in collaborative business processes. In: PRO-VE. pp.
259–270 (2019)
[18] Knuplesch, D., Reichert, M., Pryss, R., Fdhila, W., Rinderle-Ma, S.:
Ensuring compliance of distributed and collaborative workflows. In:
CollaborateCom’13. pp. 133–142 (2013)
[19] Knuplesch, D., Fdhila, W., Reichert, M., Rinderle-Ma, S.: Detecting the
effects of changes on the compliance of cross-organizational business
processes. In: ER’15. pp. 94–107 (2015)
[20] Knuplesch, D., Reichert, M., Fdhila, W., Rinderle-Ma, S.: On enabling
compliance of cross-organizational business processes. In: BPM, pp.
146–154 (2013)
[21] Knuplesch, D., Reichert, M., Kumar, A.: A framework for visually
monitoring business process compliance. Inf. Syst. 64, 381–409 (2017)
[22] Knuplesch, D., Reichert, M., Ly, L.T., Kumar, A., Rinderle-Ma, S.: On
the formal semantics of the extended compliance rule graph. Tech. Rep.
2013-05, Ulm University (2013)
[23] Ly, L.T., Maggi, F.M., Montali, M., Rinderle-Ma, S., van der Aalst,
W.M.P.: Compliance monitoring in business processes: Functionalities,
application, and tool-support. Inf. Syst. 54, 209–234 (2015)
[24] Maggi, F., Montali, M., Westergaard, M., van der Aalst, W.M.P.:
Monitoring business constraints with linear temporal logic: an approach
based on colored automata. In: BPM. pp. 132–147 (2011)
[25] Mendling, J., et al.: Blockchains for business process management -
challenges and opportunities. ACM Trans. Management Inf. Syst. 9(1),
4:1–4:16 (2018)
[26] Meroni, G., Baresi, L., Montali, M., Plebani, P.: Multi-party business
process compliance monitoring through iot-enabled artifacts. Inf. Syst.
73, 61–78 (2018)
[27] Montali, M., Maggi, F.M., Chesani, F., Mello, P., van der Aalst, W.M.P.:
Monitoring business constraints with the event calculus. Trans on
Intelligent Sys and Tech 5(1), 17.1–17.30 (2014)
[28] Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: DECLARE: full
support for loosely-structured processes. In: EDOC. pp. 287–300 (2007)
[29] Schunselaar, D.M.M., Maggi, F.M., Sidorova, N.: Patterns for a log-
based strengthening of declarative compliance models. In: Integrated
Formal Methods. pp. 327–342 (2012)
[30] Taghiabadi, E.R., Fahland, D., van Dongen, B.F., van der Aalst, W.M.P.:
Diagnostic information for compliance checking of temporal compliance
requirements. In: Advanced Information Systems Engineering. pp. 304–
320 (2013)
[31] Tosatto, S.C., Governatori, G., van Beest, N.: Checking regulatory
compliance: Will we live to see it? In: Business Process Management.
pp. 119–138 (2019)
[32] Tosatto, S.C., Governatori, G., van Beest, N., Olivieri, F.: Efficient full
compliance checking of concurrent components for business process
models. FLAP 6(5), 963–998 (2019)
[33] Weske, M.: Business Process Management - Concepts, Languages,
Architectures, Third Edition. Springer (2019)
[34] Yao, J., Chen, S., Levy, D.: Accountability-based compliance control of
collaborative business processes in cloud systems. In: Security, Privacy
and Trust in Cloud Systems, pp. 345–374 (2014)
APPENDIX
A. Choreography
Definition 3 (Choreography, slightly adapted from [7]): We
define a choreography yas a tuple (P,GΠ,L,ψ,Γ,ξ)
where,
-Pis the set of all participating partners.
-Gis the choreography model representing the interactions I
between partners in P(cf. Fig. 1).
-Π = {πp}p∈P is the set of all private models.
-L={lp}p∈P is the set of all public models.
-ψ={ψp:lp↔πp}p∈P is a partial mapping function
between nodes of the public and private models.
-Γ:l↔l0is a partial mapping function between nodes of
different public models.
-ξ:G ↔ lis a partial mapping function between nodes of
the choreography model and the public models.
Based on functions ψand Γ, certain soundness properties of
choreography ycan be checked, including structural and be-
havorial compatibility between public models and consistency
between public and private models [7].
B. Additional Transitivity Proofs
Proof 3 (Chaining Transitivity): Let A, B, C be three activ-
ities or interactions such as A→B∧A99K C∧C99K B
: if Aand Boccur then Cshould occur in between.
Let Let M, E, F be three activities or interactions such as
•(1) A→M∧A99K E
•(2) M→B∧F99K B
•(3) E→F∧E99K C∧C99K F
Then, (1) ∧(2) ∧(3)
:⇔ ∀a∀m:(x(a, A)∧(x(m, M)∧a < m)→ ∃e:
(x(e, E)∧a<e)∧
∀m∀b:(x(m, M)∧(x(b, B)∧m < b)→ ∃f:
(x(f, F )∧f < b)∧
∀e∀f:(x(e, E)∧(x(f, F )∧e < f)→ ∃c: (x(c, C)∧e <
c∧c < f)
⇔ ∀a∀m∀b:(x(a, A)∧x(m, M)∧x(b, B)∧a < m∧m <
b)→(∃e∃f((x(e, E)∧x(f, F )∧a < e ∧f < b)∧
∀e∀f:(x(e, E)∧(x(f, F )∧e < f)→ ∃c: (x(c, C)∧e <
c∧c<f)
(using Theorem 1) ⇔ ∀a∀b:(x(a, A)∧x(b, B)∧a <
b)→ ∃e∃f: (x(e, E)∧x(f, F )∧a < e ∧f < b)∧
∀e∀f:(x(e, E)∧(x(f, F )∧e < f)→ ∃c: (x(c, C)∧e <
c∧c<f)
⇒ ∀a∀b:(x(a, A)∧x(b, B)∧a < b)→ ∃e∃f∃c:
(x(e, E)∧x(f, F )∧x(c, C)∧a < e∧e<c∧c<f∧f < b)
⇒ ∀a∀b:(x(a, A)∧x(b, B)∧a < b)→ ∃c: (x(c, C)∧a <
c∧c<b)
Proof 4 (Requires transitivity): Let A, B be two activities or
interactions such as A99K B∨B99K A: if Aoccurs then
Bshould occur (before or after, ∃A→ ∃B):.
Let A, B, M be three activities or interactions such as
(A99K M∨M99K A)∧(M99K B∨B99K M). Then
:⇔ ∃a:x(a, A)→ ∃m:x(m, M))∧ ∃m:x(m, M)→
∃b:x(b, B))
⇔ ∃ax(a, A)→ ∃b:x(b, B)
