Organizations often do not want to reveal the way a product is created or a service is delivered. As a consequence, if two organizations want to cooperate, they contact a trusted third party. Each specifies how it wants to communicate with the other party. The trusted third party then needs to assure that the two organizations cooperate correctly. In this paper, we study requirements on trusted third parties to ensure correct cooperation between the different organizations.
Organizations need to anticipate on the increasing dynamicity and complexity
of business markets. Therefore, organizations focus more and more on their core
activities. As a result, organizations need to cooperate in large networks. The
organizations in the network have as common goal the delivery of their services.
Such a network is called a virtual enterprise [
Communication between the organizations is asynchronous by nature: an organization sends some data, like an inquiry, to some other organization, and eventually the latter organization sends a response. Therefore, we use Petri nets to model organizations using components. Components can be composed into networks of components. Such a network is again a component. A component has an initial state and a desired final state. We say that a component, or a network of components communicates correctly if it is sound, i.e., if in all its reachable states the component is always able to eventually reach the desired final state.
Trust is an important property in a network of cooperating organizations: organizations share business knowledge and intellectual property with other organizations within the network in order to organize the component network properly and achieve desired goals. At the same time, organizations often want to keep some intellectual property within their organization and avoid sharing it for clear reasons. A common approach used in non-virtual life is the use of trusted third parties. It becomes nowadays also quite common in the virtual world. In this paper, we consider the use of a third party, also called a notary, that is trusted by all the organizations in the network. By using a notary, each Fig. 1. If the notary N communicates correctly with A and B individually, we want to conclude correctness of the network of A, B and N
. of the organizations explains to the notary the way it wants to conduct business, and the notary will assure that the organizations can do business together. This requires the notary to ensure that it communicates correctly with each of the organizations, i.e., that the notary with each of the individual organizations can reach the common goals, and secondly, that the complete network with all the organizations together can reach its common goals. If this is the case, we call the notary trusted.
In this paper we limit ourselves to the cooperation between two organizations using a notary. Rather than to use verification to check whether the communication between the notary and the two organizations is correct, we search for conditions such that if the communication between the notary and each of the individual organizations is correct, we can automatically conclude that the communication between the three parties is correct, as depicted in Fig. 1.
This paper is structured as follows. Sec. 2 introduces the basic notions needed throughout the paper. Sec. 3 explains the concept of components and their composition. In Sec. 4 we study the conditions under which the notary is guaranteed to ensure soundness of the composition of the three parties. Sec. 5 concludes the paper.
Let S be a set. The powerset of S is denoted by P(S) = { S′ | S′ ⊆ S} . We use | S| for the number of elements in S. Two sets S and T are disjoint if S ∩ T = ∅.
A bag m over S is a function m : S → N, where N = { 0, 1, . . .} denotes the set of natural numbers. We denote e.g. the bag m with an element a occurring once, b occurring three times and c occurring twice by m = [a, b3, c2]. The set of all bags over S is denoted by NS . Sets can be seen as a special kind of bag where all elements occur only once; we interpret sets in this way whenever we use them in operations on bags. We use + and − for the sum and difference of two bags, and =, <, >, ≤, ≥ for the comparison of two bags, which are defined in a standard way. The projection of a bag m ∈ NS on some set U is a bag defined by m| U (s) = m(s) if s ∈ U and m| U (s) = 0 otherwise.
A sequence over S of length n ∈ N is a function σ : { 1, . . . , n} → S. If n > 0 and σ(i) = ai for i ∈ { 1, . . . , n} , we write σ = ⟨a1, . . . , an⟩. The length of a sequence is denoted by | σ| . The sequence of length 0 is called the empty sequence, and is denoted by ϵ. The set of all finite sequences over S is denoted by S∗. We write a ∈ σ if σ(i) = a for some 1 ≤ i ≤ | σ| . Concatenation of two sequences ν, γ ∈ S∗, denoted by σ = ν; γ, is a sequence defined by σ : { 1, . . . , | ν| + | γ|} → S, such that σ(i) = ν(i) for 1 ≤ i ≤ | ν| , and σ(i) = γ(i − | ν| ) for | ν| + 1 ≤ i ≤ | ν| + | γ| . We inductively define the projection of σ ∈ S∗ on some set U by a; σ′| U = ⟨a⟩; σ′| U if a ∈ U and a; σ′| U = σ′| U otherwise.
P and T are two disjoint sets of places and transitions respectively, we call an element of the set (P ∪ T ) a node of N ; and (2) F ⊆ (P × T ) ∪ (T × P ) is the flow relation . An element of F is called an arc.
Let N = (P, T, F ) be a Petri net. Given a node n ∈ (P ∪ T ), we define its preset by N• n = { x | (x, n) ∈ F } , and its postset by n•N = { x | (n, x) ∈ F } . We omit the subscript if the context is clear.
Let N = (P, T, F ) be a Petri net. A path from a node n ∈ P ∪ T to a node m ∈ P ∪ T is a sequence π ∈ (P ∪ T )∗ such that (π(i), π(i + 1)) ∈ F for all 1 ≤ i < n. The set of all paths from n to m is denoted by Π(n, m). A path is called cyclic if there exists a path π of length n > 0 such that π(1) = π(n). If N has a cyclic path, the net is called cyclic. If no such cycle exists, it is called acyclic.
To describe the semantics of a Petri net, we use markings. A marking of N is a bag m ∈ NP , where m(p) denotes the number of tokens in place p ∈ P . If m(p) > 0, place p is called marked in marking m. A Petri net N with a marking m is written as (N, m) and is called a marked Petri net.
Given a marked Petri net (N, m) with N = (P, T, F ), a transition t ∈ T is enabled, denoted by (N : m −→t), if • t ≤ m. If a transition is enabled in (N, m), it can fire . A transition firing, denoted by ( N : m −→t m′), results in a new marking m′ = m − • t + t• . We lift the firing to sequences of transitions in the standard way. A sequence σ ∈ T ∗ of length n is a firing sequence from m0 to mn, if there exist markings mi, mi+1 ∈ NP such that (N : mi −σ(→i) mi+1) for all 1 ≤ i < | σ| . The set of reachable markings from a given marking m is denoted as R(N, m) = { m′ | ∃ σ ∈ T ∗ : (N : m −σ→ m′)} . We lift the set of reachable markings from a single marking to a set of markings in a standard way, i.e., given a set M ⊆ NP , R(N, M ) = ∪m∈M R(N, m).
Given a marked Petri net (N, m0) with N = (P, T, F ), a place p ∈ P is called k-bounded for some k ∈ N if m(p) ≤ k for all markings m ∈ R(N, m0). If all places are k-bounded, we call (N, m0) k-bounded. A transition t ∈ T is called live if for all markings m ∈ R(N, m0) there exist a firing sequence σ ∈ T ∗ and a marking m′ ∈ R(N, m) such that (N : m −→ m′ −→t). If all transitions of σ (N, m0) are live, (N, m0) is called live. A transition t ∈ T is called quasi-live if there exists a marking m ∈ R(N, m0) such that (N : m −→t). If all transitions of (N, m0) are quasi-live, the marked Petri net is called quasi-live. A marking m ∈ R(N, m0) is called a home marking if m ∈ R(N, m′) for all m′ ∈ R(N, m0). A reachable marking m ∈ R(N, m0) is called a deadlock of (N, m0) if there is no transition t ∈ T with (N : m −→t). Given a desired marking f ∈ R(N, m0), a non-empty subset of markings L ⊆ R(N, m0) is called a live-lock w.r.t f if f ̸∈ R(N, L) and L = R(N, L), i.e., from L the desired marking is not reachable, and no other marking then a marking in L can be reached from L.
On Petri nets, we define two classes based on their structure: S-Nets, also called state machines, and workflow nets. A Petri net N = (P, T, F ) is a S-net if | • t| ≤ 1 and | t• | ≤ 1 for all transitions t ∈ T .
Definition 2 (Workflow net, closure). Let N = (P, T, F ) be a Petri net. It is a workflow net (WFN) if there exist two places i ∈ P and f ∈ P , called the initial place and final place respectively, such that • i = f • = ∅, and all nodes of N are on a path from i to f . Its closure is the net N ∗ = (P, T ∪{ t∗} , F ∪{ (t∗, i), (f, t∗)} , where t∗ ̸∈ T .
A workflow net is called sound if (1) it is weakly terminating, i.e., it always
has the option to reach the final marking in which only the final place is marked,
(2) it is properly completing, i.e., if in a marking the final place is marked, it
is the only place marked, and (3) all transitions have a function, i.e., for every
transition a reachable marking exists that enables the transition. Note that we
use the classical soundness definition [
Definition 3 (Soundness). A workflow net N = (P, T, F ) with initial place i and final place f is called sound if (1) [f ] is a home marking of (N, [i]), (2) for any reachable marking m ∈ R(N, [i]), if m ≥ [f ] then m = [f ], and (3) (N, [i]) is quasi live.
A WFN N = (P, T, F ) with initial place i is sound if and only if the marked
Petri net (N ∗, [i]) is live and bounded [
If we give a tuple a name, we subscript the elements with the name of the tuple, e.g. for N = (A, B, C) we refer to its elements by AN , BN , and CN . If the context is clear, we omit the subscript.
In this paper, we use asynchronously communicating components [
Petri net (OPN) is an 6-tuple (P, I, O, T, F, i, f ) where An open – ((P ∪ I ∪ O, T, F ), i) is a marked Petri net; – P is a set of internal places; – I is a set of input places, and • I = ∅; – O is a set of output places, and O• = ∅; – P , I and O are pairwise disjoint; – ∀t ∈ T : | (• t ∪ t• ) ∩ (I ∪ O)| ≤ 1; and – i ∈ NP is the initial marking; and – f ∈ NP is the final marking .
We call the set I ∪ O the interface places of the OPN. Two OPNs N and M are called disjoint if (PN ∪ IN ∪ ON ∪ TN ) ∩ (PM ∪ IM ∪ OM ∪ TM ) = ∅. An OPN N is called closed if IN = ON = ∅. We write R(N, m) for R((PN ∪ IN ∪ ON , TN , FN ), m) for m ∈ NPN ∪IN ∪ON .
The skeleton of N is defined as the Petri net S(N ) = (PN , TN , F ) with F = FN ∩ ((PN × TN ) ∪ (TN × PN )). For nodes n ∈ (PN ∪ TN ), we write N◦n and t◦N as a shorthand for •
S(N)t and t•S(N), respectively.
If S(N ) is a workflow net with initial place s and final place o, i = [s] and f = [o], N is called an open workflow net .
OPNs are composed with each other to build networks of communicating components. As a network of components can be used as a component again, the result of the composition is a component too. We say two OPNs are composable if the only elements shared between the two OPNs are their interface places, such that input places of the one are output places of the other and vice versa. Composition is then defined as the union of the two OPNs.
able, denoted by A⊕ B, if and only if (PA ∪IA ∪OA ∪TA)∩(PB ∪IB ∪OB ∪TB) = (OA ∩ IB) ∪ (IA ∩ OB).
If A and B are composable, their composition results in an OPN A ⊕ B = (PA ∪ PB ∪ H, (IA ∪ IB) \ H, (OA ∪ OB) \ H, TA ∪ TB, FA ∪ FB, iA + iB) with H = (OA ∩ IB) ∪ (IA ∩ OB).
Note that two disjoint OPNs are composable by definition. Two important
properties of composition are commutativity and projection, as shown in [
σ m −→ m′).
two composable OPNs. Then N = A⊕ B = B ⊕ A, and (S(A) : m| PA for all firing sequences σ ∈ Tn∗ and markings m, m′ ∈ NPN such that (S(N ) : σ| TA m′| PA ) −→
The composition operator allows to create arbitrary networks of communicating components. As long as the interface places match, it is allowed to compose the components. However, it does not guarantee that the components communicate correctly. Composition is thus a syntactic check whether components are able to communicate.
Components communicate correctly if all components in the network are able to reach their desired final marking, and no messages are pending in one of the interface places. Further, we do not want to have transitions that are unreachable in the composition. To express this property, we use the notion of soundness for components: a component is sound if, ignoring the communication with other components in the network, all components can reach their final marking, no tokens are left in the network, and for each transition in the network, a marking should be reachable in which the transition is enabled.
3. ∀t ∈ TN : ∃m ∈ R(S(N ), iN ) : ◦t ≤ m (quasi liveness). 1. ∀m ∈ R(S(N ), iN ) : fN ∈ R(S(N ), m) (weak termination); 2. ∀m ∈ R(S(N ), iN ) : m ≥ fN
=⇒ m = fN (proper completion); and
Note that this soundness definition is stronger than the soundness notion used
in [
A direct consequence of the projection property and soundness is that if in a composition between A, B and C, such that A and C are disjoint, and A and B are composable, as well as B and C, and B is in its final marking, then the other two components can reach their final marking as well.
Lemma 8. Let A, B and C be three pairwise composable OPNs such that A and C are disjoint, and A ⊕ B and B ⊕ C are sound. Define L = A ⊕ B ⊕ C.
Then fL ∈ R(S(L), m) for all markings m ∈ R(S(L), iL) such that fB ≤ m.
μ Proof. Define K = A ⊕ B. By the projection property, (S(K) : iK −→ Since fB ≤ m, and K is sound, there exists a firing sequence µ ∈ TA∗ such that (S(K) : m| PK
−→ fK ), and hence (S(L) : m −→ m′) for some m′ ∈ NPL with ν ∈ TB∗ such that (S(L) : m′ −ν→ fL), which proves the statement. fK ≤ m′. Applying the same argument for B ⊕ C, there exists a firing sequence ⊔⊓ μ σ| TK m| PK ).
Organizations have to cooperate more and more in order to do their business. However, they often do not want to share the way they operate, for example to hide internal business knowledge or intellectual property. An often proposed solution is a third party that is trusted by all organizations within the network. This third party, the notary, needs to ensure that it knows how the organizations within the network want to operate. On the one hand the notary needs to ensure that it works correctly with each individual organization, and on the other hand, that the network of all organizations, including the notary, is correct.
As the main purpose of a notary is to ensure correct behavior of the
communication between the two organizations that want to cooperate, we model the
notary by an OWN. The main actions of the notary are the sending and
receiving of messages of the different components. Therefore, each transition that is
communicating is labeled with the sending or receiving of a message, or as silent
if the transition represents an internal step of the notary. We restrict the notary
to state machines, i.e., each notary is sound by its structure [
As each transition is connected to at most one component, we introduce the communication function CN : T → { A, B, τ } such that CN (t) = X if • t∩OX ̸= ∅ for X ∈ { A, B} and CN (t) = τ otherwise. 4.1
We first consider the case of an acyclic notary. If a notary is acyclic, then its set of possible firing sequences is finite. For acyclic notaries, soundness can be guaranteed, as shown in this section.
p u t Notary t Notary p u
One source of possible erroneous behavior lies in the control of conflicts: if in a notary two transitions share a place in their presets, then the transitions should either be both controlled by the same component, or by the notary. Consider the examples of Fig. 2. Taking the composition A ⊕ N of Fig. 2(a), then transition u is always enabled if transition t is enabled, whereas in Fig. 2(b), component A controls the conflict in the composition of
CN (t) = CN (u).
Let A and B be two components such that A and C are disjoint, and let N be an acyclic notary between A and B. If A ⊕ N and N ⊕ B are sound, then for all places p ∈ P and transitions t, u ∈ p• we have Proof. Let p ∈ P and t, u ∈ p• . Suppose CN (t) ̸= CN (u). This implies that at least one of the transitions t and u is controlled by a component (otherwise we would have CN (t) = CN (u) = τ ). Without loss of generality, assume this transition to be t and component to be A, i.e., CN (t) = A. Then there exists a place q ∈ IN ∩ OA, with q ∈
• t.
Define there exists a reachable marking m ∈ R(S(M ), iM ) with (S(M ) : m −→t), and thus m(q) > 0. Note that transition u is also enabled in m. Hence, we can
M = A ⊕ N . Since N is an S-net, M◦u ⊂ M◦t. Since M is sound, fire transition u u and obtain a marking m′ ∈ NPM : (S(M ) : m −→ m′), where m′ = m − M◦u + u◦M and m′(q) = m(q) (since q ̸∈ M◦u).
As N is acyclic and t is the only transition consuming from q, the token from q will never be consumed by any sequence firing from m′. Thus, M is not sound, which is a contradiction. Hence, the lemma holds. ⊔⊓
The lemma shows that conflicts (choices) in the notary component are always controlled correctly, either by a single component or the notary itself. Consequently, if the composition of the components of A and B with N individually is sound, the composition of the three is sound as well, as proven in the next theorem.
are not in their final markings; A ⊕ N ⊕ B is sound.
Theorem 11. Let A and B be two OPNs such that A and B are disjoint. Let N be an acyclic notary between A and B. If A ⊕ N and N ⊕ B are sound, then an m, and, additionally γ| TN = ∅ for all firing sequences (S(M ) : m −γ→). Now consider the following two possible cases:
M = A ⊕ N ⊕ B. Suppose M is not sound. Then there exist a σ marking m ∈ R(S(M ), iM ) and a firing sequence σ ∈ T M∗ such that (S(M ) : iM −→ m), fM ̸∈ R(S(M ), m). Moreover, since N is acyclic, there exists such γ ∈ T M∗ such that 1. Notary N is in its final place in this marking m, i.e. m ≥ fN , but A or B 2. Notary N is not in its final place in marking m, i.e. m ̸≥ fN . will be enabled in (S(M ), m), and N is not in its final marking. As and S(N ) is an S-net, there exist a place p ∈ PN of the notary such that m(p) > 0. p• cannot contain any transition t with CN (t) = τ , since this transition fN ̸= m| PN would be enabled in m. Due to Lm. 10, all transitions t from p• have the same value for CN (t). Without the loss of generality, we suppose it to be A. Since A ⊕ N is sound, there is a firing sequence σ; t from marking m| A⊕N in A ⊕ N such that σ ∈ TA∗ and t ∈ TN . This firing sequence is then also a firing sequence of M , but this contradicts the statement that no transition from TN can fire Acyclic notaries ensure the correctness of the composition of two components if these components communicate correctly with the notary. Often, cyclic behavior between components is needed. For example, in order to agree on some quote, several cycles may be involved. In this section, we extend acyclic nets with singleentry-single-exit (SESE) loops.
A SESE loop consists of an entry place and an exit place, not being the same, and all nodes inside the loop are on a path from entry to exit or vice versa, on a path from exit to entry. Furthermore, we require each place in the loop to have exactly one transition in its preset and one in its postset, except for the entry and exit place. An example of a SESE loop is depicted in Fig. 3(b).
An S-net is a Simple Cyclic S-net (SCS-net) if all loops in the net are disjoint, i.e., each place and transition of the net belongs to at most one loop. In simple starting from m in M .
Therefore, A ⊕ N ⊕ B is sound. 4.2
⊔⊓ Notary N Component A
net. A set L ⊆ P ∪ T is a called a single-entry-single-exit loop (SESE loop) with entry place e ∈ L ∩ P and exit place o ∈ L ∩ P if all nodes n ∈ L are on a path from e to o or on a path from o to e, • e \ L ̸= ∅, e• ⊆ L, o• \ L ̸= ∅, and • o ⊆ L, and for all places p ∈ L ∩ P , if | • p| > 1 then p = e and if | p• | > 1 then p = o.
Let (P, T, F ) be an S-net. It is called a simple-cyclic S-net (SCS-net) if all loops are SESE loops and pairwise disjoint, i.e., for all loops L1, L2 ⊆ P ∪ T if L1 ∩ L2 ̸= ∅ then L1 = L2.
Note that in the definition of SCS-nets, we require each node to be in at most one loop. By the definition of the SESE loop, we have that if a node contains multiple elements in its preset or postset, it is either the entry or the exit of the loop. As a consequence, all SESE loops are simple: there is one path from entry to exit and one path from exit to entry. The basis of an SCS-net is an acyclic S-net. Consequently, each loops will be entered at most once.
Whereas in an acyclic notary every conflict is controlled by a single component, this is not the case in the simple-cycled case, as shown in Fig. 4. Choices still need to be controlled by a single component, but silent loops, i.e., no transition in the loop is connected with an interface places, are allowed.
Similarly to the acyclic case, if the skeleton of a notary is a simple-cyclic Snet, soundness of the three parties is assured if the notary composed with each of the organizations individually is sound. Whereas in the acyclic case every conflict is controlled by a single component, if the notary is cyclic, the moment of control can be postponed. As a consequence, we need to also consider the possibility of live-locks in which the notary is involved.
Theorem 13. Let A and B be two disjoint OPNs and let N be an simple-cyclic notary such that A ⊕ N and N ⊕ B are sound. Then A ⊕ N ⊕ B is sound. is not sound. Then there exists a marking m ∈ R(S(M ), iM ) such that fM ̸∈
K = A ⊕ N , L = N ⊕ B and M = A ⊕ N ⊕ B. Suppose M
The first case contradicts with Lm. 8.
Next, consider the second case. Suppose a marking m ∈ R(S(M ), iM ) not being the final marking exists that is a deadlock. Then, a place Without loss of generality assume CN (t) = A and CN (u) = B. with p ̸= fN , m(p) = 1 and • t ̸≤ m for all transitions t ∈ p• . Let t ∈ p• . Then CN (t) ̸= τ . If CN (t) = CN (u) for all t, u ∈ p• , then either A ⊕ N or N ⊕ B would not be sound. Hence, transitions t, u ∈ p• exist such that CN (t) ̸= CN (u).
Since S(N ) is an SCS-net, place p is either an entry or exit point of a loop, or outside a loop. Suppose place p is not the exit of a loop. Then in K, transition p ∈ PN exists u is enabled in m| PA⊕N t. Thus, a marking m′ ∈ . Since K is sound, it must be possible to fire transition
R(S(K), iL) exists such that (S(K) : m′ −→t). As transition u is also enabled in m′, u has to be in a loop, since otherwise K the would never be consumed. Hence, a deadlock cannot occur. token from the places q ∈
• t ∩ OA would never be consumed. Similarly, transition t has to be in a loop, since otherwise the token from the places q ∈ • u ∩ OB
Last, consider the case in which N reaches a live-lock, i.e, it entered a loop
L with entry i and exit o such that it cannot leave the loop. Hence, CN (t) ̸= τ for all transitions t ∈ o• \ L. If CN (t) = CN (u) for all t, u ∈ p• , then either A ⊕ N or N ⊕ B would not be sound. Hence, transitions t, u ∈ p• exist such that CN (t) ̸= CN (u). Without loss of generality assume CN (t) = A and CN (u) = B.
As all cases lead to a contradiction, A ⊕ N ⊕ B is sound. ⊔⊓ 5
We studied in this paper the problem of ensuring correctness of networks of cooperating organizations. By introducing a trusted third party, called a notary, organizations do not need to share their knowledge with the other organizations within the network. The notary needs to ensure that firstly it works correctly with each of the organizations individually, and secondly that all organizations in the network, including the notary itself, work correctly together. In this paper, we showed for two organizations and a notary that if the notary is an acyclic state machine, or it contains only single-entry-single-exit (SESE) loops, then the notary ensures soundness if it is sound with each of the organizations individually.
In literature, different approaches exist. For example, in the approach of [
The disadvantage of these approaches is that each of the organizations need
to implement a private view, whereas often organizations already have existing
components. In these approaches, the organizations have to re-engineer the
existing components, and prove that these re-engineered components adhere to the
views defined in the contract using e.g. accordance [
The setting in this paper is comparable with the more general setting of
decentralized controllability [