DIPARTIMENTO DI INGEGNERIA E SCIENZA DELL’INFORMAZIONE

UNIVERSITY OF TRENTO

38050 Povo – Trento (Italy), Xxx Xxxxxxxxx 00 xxxx://xxx.xxxx.xxxxx.xx

A CALCULUS OF CONTRACTING PROCESSES

Xxxxxxx Xxxxxxxxxx and Xxxxxxx Xxxxxx

October 2009

Technical Report #DISI-09-056

A Calculus of Contracting Processes

Xxxxxxx Xxxxxxxxxx

Dipartimento di Matematica e Informatica, Universit`a degli Studi di Cagliari

Xxxxxxx Xxxxxx

Dipartimento di Ingegneria e Scienza dell’Informazione, Universit`a degli Studi di Trento

Abstract

We propose a formal theory for contract-based computing. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We model contracts as formulae in an intuitionistic logic extended with a “contractual” form of implication. Decidability holds for our logic: this allows us to mechan- ically infer the rights and the duties deriving from any set of contracts. We embed our logic in a core calculus of contracting processes, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency. We then show how to exploit our calculus as a tool for modelling services, the interaction of which is driven by contracts.

1 Introduction

Security, trustworthiness and reliability of software systems are crucial issues in the rising Information Society. As new online services (e-commerce, e-banking, e-government, etc.) are made available, the number and the criticality of the problems related to possible misbehaviour of services keeps growing. Neverthe- less, these problems are hardly dealt with in current practice, especially from the client point of view.

The typical dynamics of a Web transaction is that a client chooses a ser- vice provider that she trusts, and then proceeds interacting with it, without any provable guarantee that she will eventually obtain the required feature. Standard service infrastructures are focussed on protecting services from unde- sired interactions, while little effort is devoted to protecting clients. As one can see, the situation is quite unbalanced: clients have to operate with no concrete guarantees, and all they can do is to trust the service providers. At best, the service provider commits himself to respect some “service level agreement”. In the case this is not honoured, the only thing the client can do is to take legal steps against the provider. Although this is the normal practice nowadays, it is highly desirable to reverse this trend. Indeed, both clients and services could incur relevant expenses due to the needed legal disputes. This is impractical, especially for transactions dealing with small amounts of money.

We propose to balance this situation, by regulating the interaction among parties by a suitable contract. A contract subordinates the behaviour promised by a client (e.g. “I will pay for a service X”) to the behaviour promised by a

service (e.g. “I will provide you with a service Y”), and vice versa. The crucial problems are then how to define the concept of contract, how to understand when a set of contracts gives rise to an agreement among the stipulating parties, and how to actually enforce this agreement, in an environment – the Internet – which is by definition open and unreliable.

1.1 An example

To give the intuition about our contracts, suppose there are two kids, Xxxxx and Xxx, who want to play together. Xxxxx has a toy airplane, while Bob has a bike. Both Xxxxx and Xxx wish to play with each other’s toy. Before sharing their toys, Xxxxx and Xxx stipulate the following “gentlemen’s agreement”:

Xxxxx: I will lend my airplane to you, Bob, provided that I borrow your bike.

Bob: I will lend my bike to you, Xxxxx, provided that I borrow your airplane. From the above two contracts, we want to formally deduce that Xxxxx and

Xxx will indeed share their toys, provided that they are real “gentlemen” who always respect their promises. Let us write a for the atomic proposition “Xxxxx lends her airplane” and b for “Bob lends his bike”. A (wrong) formalisation of the above commitments in classical propositional logic could be the following, using implication →. Xxxxx’s commitment A is represented as b → a and Bob’s commitment B as a → b. While the above commitments agree with our intu- ition, they are not enough to deduce that Xxxxx will lend her airplane and Bob will lend his bike. Formally, it is possible to make true the formula A ∧ B by assigning false to both propositions a and b.

The failure to represent scenarios like the one above seems related to the Modus Ponens rule: to deduce b from a → b, we need to prove a. That is, we could deduce that Bob lends his bike, but only after Xxxxx has xxxx Xxx her airplane. So, one of the two parties must “take the first step”. In a logic for mu- tual agreements, we would like to deduce a ∧ b whenever A ∧ B is true, without requiring any party to take the first step. That is, A and B are contracts, that once stipulated imply the duties promised by all the involved parties. Notice that A ∧ B → a ∧ b does not hold neither in classical nor in intuitionistic propo- sitional calculus IPC [35], where the behaviour of implication strictly adheres to Modus Ponens.

To model contracts, we then extend IPC with a new form of implication, which we denote with the symbol ։. The resulting logic is called PCL, for Propositional Contract Logic. For instance, the contract declared by Xxxxx, “I will lend my airplane to Bob provided that Bob lends his bike to me”, will be written b ։ a. This form of, say, contractual implication, is stronger than the standard implication → of IPC. Actually, b ։ a implies a not only when b is true, like IPC implication, but also in the case that a “compatible” contract,

e.g. a ։ b, holds. In our scenario, this means that Xxxxx will lend her airplane to Bob, provided that Bob agrees to lend his bike to Xxxxx whenever he borrows Xxxxx’s airplane, and vice versa. Actually, the following formula is a theorem of our logic:

(b ։ a) ∧ (a ։ b) → a ∧ b

In other words, from the “gentlemen’s agreement” stipulated by Xxxxx and Xxx, we can deduce that the two kids will indeed share their toys.

All the above shows how to deduce, from a set of contracts, the rights and the duties of the involved parties. Yet, it says nothing about the actual dynamics of these parties, that is how to model their behaviour. To do that, we introduce a calculus of contracting processes, which embeds our logic for contracts. This calculus belongs to the family of concurrent constraints calculi [33, 6], with the peculiarity that in ours the constraints are PCL formulae. A process can assert a constraint c (a PCL formula) through the primitive tell c. For instance, the following process models Xxxxx exposing her contract:

(x) tell b(x) ։ a(x)

Formally, this will add b(x) ։ a(x) to the set of constraints. The formal param- eter x will be bound to the identifier of the actual session established between Xxxxx and Xxx. As it happens for sessions centered calculi [36, 12], sessions are an important aspect also in our calculus, since they allow for distinguishing among different instantiations of the same contract. The outer (x) is a scope delimitation for the variable x, similarly to the Fusion calculus [28].

After having exposed her contract, Xxxxx will wait until finding that she has actually to lend her airplane to Bob. To discover that, Xxxxx uses the primitive fusex c as follows:

fusex a(x)

This is similar to the ask c primitive of concurrent constraints, which probes the constraints to see whether they entail the constraint c. Yet, our fuse has some crucial peculiarities. Besides probing the constraints to find whether they entail c, fusex c also binds the variable x to an actual session identifier, shared among all the parties involved in the contract. In other words, fusex c actually fuses all the processes agreeing on a given contract.

Summing up, we will model the behaviour of Xxxxx as the following process:

Xxxxx = (x) tell b(x) ։ a(x). fusex a(x). lendAirplane

where the process lendAirplane (no further specified) models the action of Xxxxx actually lending her airplane to Bob. The overall behaviour of Xxxxx is then as follows: (i) issue the contract; (ii) wait until discovering the duty of lending the airplane; (iii) finally, lend the airplane.

Dually, we model the behaviour of Bob as the following process in our cal- culus:

Bob = (y) tell a(y) ։ b(y). fusey b(y). lendBike

A possible interaction of Xxxxx and Xxx will then be the following, where n

stands for a fresh session identifier:

(n) lendAirplane

Xxxxx | Bob →∗ {n/x} | lendBike {n/y}

As expected, the resulting process shows Xxxxx and Xxx actually sharing their toys, in the session identified by n.

1.2 Contributions

We propose a unified framework for modelling distributed systems that base their interactions on contracts. Technically, our contribution consists of the following points:

• We devise a minimal set of properties which are desirable in any logical formalization of contracts.

• We define a logic to model contracts, and to infer the duties deriving from those. Our logic satisfies all the properties identified above as desirable. Further, we support the logic with several examples.

• We study the proof theory of our logic. In particular, we show that our logic is consistent and decidable.

• We define a calculus for contracting processes, which exploits the logic to drive synchronizations between processes.

• We show that our calculus is suitable for modelling complex interactions of contracting parties. We also show how to embed the π-calculus and graph rewriting in our calculus.

2 A Logic for Contracts

We now introduce our theory of contracts. We start in Sect. 2.1 by characterizing our logic through a set of properties that we would expect to be enjoyed by any logic for contracts. In Sect. 2.2 we present the syntax of PCL. In Sect. 2.3 we synthesize a minimal set of Xxxxxxx-style axioms for PCL that imply all the desirable properties, and we show the resulting logic consistent (Theorem 1). We then propose a sequent calculus for PCL, which is shown to be equivalent to the Xxxxxxx system (Theorem 2). The hard result is Theorem 3, where we establish cut elimination for our sequent calculus. Together with the subformula property (Theorem 4), this paves us the way to state decidability for PCL in Theorem 5. In Sect. 2.4 we give further details and examples about using the logic PCL to model a variety of contracts.

2.1 Desirable properties

We now characterize, with the help of some examples, the desirable properties of any logic for contracts.

As shown in the Sect. 1, a characterizing property of contractual implication is that of allowing two dual contracting parties to “handshake”, so to make their agreement effective. This is resumed by the following handshaking property:

⊢ (p ։ q) ∧ (q ։ p) → p ∧ q (1)

A generalisation of the above property to the case of n contracting parties is also desirable. It is a sort of “circular” handshaking, where the (i + 1)-th party, in order to promise some duty pi+1, relies on a promise pi made by the i-th party (in a circular fashion, the first party relies on the promise of the last one). In the case of n parties, we would expect the following:

⊢ (p1 ։ p2) ∧ · · · ∧ (pn−1 ։ pn) ∧ (pn ։ p1) → p1 ∧ · · · ∧ pn (2)

As a concrete example, consider an e-commerce scenario where a Buyer can buy items from a Seller, and pay them through a credit card. To mediate the interaction between the Buyer and the Seller, there is a Bank which manages payments. The contracts issued by the three parties could then be:

Buyer: I will click “pay” provided that the Seller will ship my item

Seller: I will ship your item provided that I get the money

Bank: I will transfer money to the Seller provided that the Buyer clicks “pay”.

Let the atomic propositions ship, clickpay, and pay denote respectively the facts “Seller ships item”, “Buyer clicks pay”, and “Bank transfers money”. The above contracts can then be modelled as:

Buyer = ship ։ clickpay Bank = clickpay ։ pay Seller = pay ։ ship

Then, by the handshaking property (2), we obtain a successful transaction:

⊢ Buyer ∧ Bank ∧ Seller → pay ∧ ship

Note that, in the special case that n equals 1, the above “circular” hand- shaking property turns into a particularly simple form:

⊢ (p ։ p) → p (3)

Intuitively, (3) can be interpreted as the fact that promising p provided that p, implies p (actually, also the converse holds, so that promise is equivalent to p). It also follows from (1) when p = q.

Another generalisation of the toy-exchange scenario of Sect. 1 to the case of n kids is also desirable. It is a sort of “greedy” handshaking property, because now a party promises pi only provided that all the other parties promise their duties, i.e. p1, . . . , pi−1, pi+1, . . . , pn. The greedy handshaking can be stated as:

⊢ i∈1..n (p1 ∧ . . . ∧ pi−1 ∧ pi+1 ∧ . . . ∧ pn) ։ pi → p1 ∧ · · · ∧ pn (4)

So far, we have devised some characterizing properties of handshakings. We will now focus on further logical properties of contractual implication. As shown by (1), a contract p ։ q becomes effective, i.e. implies the promise q, when it is matched by a dual contract q ։ p. Even more directly, p ։ q should be effective also in the case that the premise p is already true:

⊢ p ∧ (p ։ q) → q (5)

In other words, contractual implication should be stronger than standard impli- cation, i.e. we expect that the following is a theorem of any logic for contracts:

⊢ (p ։ q) → (p → q) (6)

On the other hand, we do not want that also the converse holds, since this would equate the two forms of implication: that is, /⊢ (p → q) → (p ։ q).

We want contractual implication to share with standard implication a num- ber of properties. We discuss some of them below. First, a contract that promises true (written ⊤) is always satisfied, regardless of the precondition. So, we expect the following tautology:

⊢ p ։ ⊤ (7)

However, differently from standard implication, we do not want that a con- tract with a false precondition (written ⊥) always holds, i.e. /⊢ ⊥ ։ p. To see why, assume that ⊥ ։ p is a tautology, for all p. Then, it would also be the case for p = ⊥, and so by (3) we would deduce a contradiction: (⊥ ։ ⊥) → ⊥.

Another property of implication that we want to preserve is transitivity:

⊢ (p ։ q) ∧ (q ։ r) → (p ։ r) (8)

Back to our previous example, transitivity would allow the promise of the Buyer (ship ։ clickpay) and the promise of the Bank (clickpay ։ pay) to be combined in the promise ship ։ pay.

Contractual implication should also enjoy a stronger form of transitivity. We illustrate it with the help of an example. Suppose an air-flight customer who wants to book a flight. To do that, she issues the following contract:

Customer : bookFlight ։ pay

This contract states that the customer promises to pay the required amount, provided that she obtains a flight reservation. Suppose now that an airline company starts a special offer, in the form of a free drink for each customer:

AirLine : pay ։ bookFlight ∧ freeDrink

Of course, the two contracts should give rise to an agreement, because the airline company is promising a better service than the one required by the customer contract. To achieve that, we expect to be able to “weaken” the contract of the airline company, to make it match the contract issued by the customer:

⊢ AirLine → (pay ։ bookFlight)

Alternatively, one could make the two contracts match by making stronger the precondition required by the customer, that is:

⊢ Customer → (bookFlight ∧ freeDrink ։ pay)

More in general, we want the following two properties hold for any logic for contracts. They say that the promise in a contract can be arbitrarily weak- ened (9), while the precondition can be arbitrarily strengthened (10).

⊢ (p ։ q) ∧ (q → q′) → (p ։ q′) (9)

⊢ (p′ → p) ∧ (p ։ q) → (p′ ։ q) (10)

Note that the properties (8), (9), (10) cover three of the four possible cases of transitivity properties which mix standard and contractual implication. Ob- serve, instead, that the fourth case would make standard and contractual im- plications equivalent, so it is not a desirable property.

Another property that should hold is that, if a promise q is already true, then it is also true any contract which promises q:

⊢ q → (p ։ q) (11)

Of course, we do not want the converse to hold: it is not always the case that a contract implies its promise: /⊢ (p ։ q) → q.

2.2 Syntax

The syntax of PCL extends that of IPC. It includes the standard logic connec- tives ¬, ∧, ∨, → and the contractual implication connective ։. We assume a de- numerable set {p, q, r, s, . . .} of prime (atomic) formulae. Arbitrary PCL formulae are denoted with the letters p, q, r, s, . . . (note that the font differs from that used for prime formulae). The precedence of IPC operators is the following, from highest to lowest: ¬, ∧, ∨, →. We stipulate that ։ has the same precedence as →.

Definition 1 The formulae of PCL are inductively defined as:

p ::= ⊥ | ⊤ | p | ¬p | p ∨ p | p ∧ p | p → p | p ։ p

We let p ↔ q be syntactic sugar for (p → q) ∧ (q → p).

2.3 Axiomatization

We now present an Xxxxxxx-style axiomatization for PCL.

Definition 2 The proof system of PCL comprises all the axioms of IPC, the Modus Ponens rule [Cut], and the following additional axioms.

⊤ ։ ⊤ [Zero]

(p ։ p) → p [Fix]

(p′ → p) → (p ։ q) → (q → q′) → (p′ ։ q′) [PrePost]

The above axioms are actually a subset of the properties discussed in Sect. 2.1. The axiom Zero is a subcase of (7), the axiom Fix is just (3), while the axiom PrePost combines (9) and (10). As expected, this set of axioms is actually sound and complete w.r.t. all the properties marked as desirable in Sect. 2.1.

Lemma 1 The properties (1)–(11) are theorems of PCL . Also, we have:

⊢ (p ։ q) ∧ (q ։ r) → (p ։ (q ∧ r))

⊢ (p ։ (q ∧ r)) → (p ։ q) ∧ (p ։ r)

⊢ (p ։ q) ∨ (p ։ r) → (p ։ (q ∨ r))

⊢ (p ։ q) → ((q → p) → q)

We present below some of the most significant results about our logic. For a more comprehensive account, including detailed proofs of all our results, see [3].

Theorem 1 PCL is consistent, i.e. /⊢ ⊥.

As expected, the following formulae are not tautologies of PCL :

/⊢ (p → q) → (p ։ q) /⊢ (p ։ q) → q

/⊢ ⊥ ։ p /⊢ ((q → p) → q) → (p ։ q)

Note that if we augment our logic with the axiom of excluded middle, then (p ։ q) ↔ q becomes a theorem, so making contractual implication trivial. For this reason we use IPC, instead of classical logic, as the basis of PCL .

Another main result about PCL is its decidability. To prove that, we have devised a Gentzen-style sequent calculus, which is equivalent to the Xxxxxxx-style axiomatisation. In particular, we have extended the sequent calculus for IPC presented in [30] with rules for the contractual implication connective ։.

Definition 3 The sequent calclus of PCL includes all the rules for IPC [3], and the following additional rules.

Γ ⊢ q

Γ ⊢ p ։ q

[Zero]

Γ, p ։ q, r ⊢ p

Γ, p ։ q, q ⊢ r

Γ, p ։ q ⊢ r

[Fix]

Γ, p ։ q, a ⊢ p

Γ, p ։ q, q ⊢ b

Γ, p ։ q ⊢ a ։ b

[PrePost]

We now establish the equivalence between the two logical systems of PCL. In the following theorem, we denote with ⊢H provability in the Xxxxxxx-style system, while ⊢G is used for Gentzen-style provability.

Theorem 2 For all PCL formulae p, we have that: ⊢H p ⇐⇒ ∅ ⊢G p.

Our sequent calculus enjoys cut elimination. The proof is non-trivial, since the rules for ։ are not dual, unlike e.g. left/right rules for ∧. Nevertheless, the structural approach of [30] can be adapted. Full details about proofs are in [3].

Theorem 3 (Cut Elimination) If p is provable in PCL , then there exists a proof of p which does not use the Cut rule.

The consistency result can be extended to negation-free formulae. This will be useful in Sect. 3, where we will define our calculus.

Lemma 2 If p is free from {⊥, ¬}, then /⊢ p → ⊥.

The subformula property holds in PCL. Cut-free proofs only involve subfor- mulae of the sequent at hand.

Theorem 4 (Subformula Property) If D is a cut-free proof of Γ ⊢ p, the formulae occurring in D are subformulae of those occurring in Γ and p.

Decidability then follows from theorems 3 and 4.

Theorem 5 The logic PCL is decidable.

As a further support to our logic, we have implemented a proof search algo- rithm, which decides whether any given formula is a tautology or not. Despite the problem being PSPACE complete [34], the performance of our tool is ac- ceptable for the examples presented in this paper. Our tool is available at [29].

We now establish some expressiveness results, relating PCL and IPC. More in detail, we consider whether sound and complete homomorphic encodings exist, that is, whether ։ can be regarded as syntactic sugar for some IPC context.

Definition 4 A homomorphic encoding m is a function from PCL formulae to IPC formulae such that: m is the identity on prime formulas, ⊤, and ⊥; it acts homomorphically on ∧, ∨, →, ¬; it satisfies m(p ։ q) = C[m(p), m(q)] for some fixed IPC context C(•, •).

Of course, each homomorphic encoding is uniquely determined by the con- text C. Several complete encodings exist:

Lemma 3 The following homomorphic encodings are complete, i.e. they satisfy

▶ p =⇒ ▶IPC mi(p). Moreover, they are pairwise non-equivalent in IPC.

m0(p ։ q) = m0(q) m1(p ։ q) = (m1(q) → m1(p)) → m1(q) m2(p ։ q) = ¬¬(m2(q) → m2(p)) → m2(q) m3(p ։ q) = ¬(m3(q) → m3(p)) ∨ m3(q) m4(p ։ q) = ((m4(q) → m4(p)) ∨ a) → m4(q)

where a is any prime formula.

However, there can be no sound encodings, so ։ is not just syntactic sugar.

Theorem 6 If m is a homomorphic encoding of PCL into IPC, then m is not sound, i.e. there exists a PCL formula p such that ▶IPC m(p) and /▶ p.

In [3] we have proved further properties of PCL, including some relations between PCL and IPC, the modal logic S4, and propositional lax logic. Also, we have explored there further properties and application scenarios for our logic.

2.4 Examples

Example 1 (Real Estate) We now exploit PCL to model a typical prelimi- nary contract for a real estate sale in Italy.

Assume a buyer who is interested in buying a new house from a given seller. Before stipulating the actual purchase contract, the buyer and the seller meet to stipulate a preliminary sale contract, that fixes the terms and conditions of the purchase. Typically, this contract will indicate the price and the date when the deed of sale will take place, and it will outline the obligations for the buyer and the seller. When the preliminary contract is signed by both parties, the buyer will pay a part of the sale price. By the Italian laws, if the seller decides not to sell the house after having signed the preliminary contract and collected the deposit, she must pay the buyer back twice the sum received. Similarly, if the buyer changes his mind and decides not to buy the house, he loses the whole deposited amount. We model the preliminary sale contract as two PCL formulae, one for the buyer and the other for the seller. The buyer will sign the preliminary contract (signB), provided that the seller will actually sell her house (sellS), or she refunds twice the sum received (refundS). Also, the buyer promises that if he signs the preliminary contract, than either he will pay the stipulated price (payB), or he will not pay and lose the deposit (refundB).

Buyer = ((sellS V refundS) ։ signB) Λ (signB ։ (payB V (чpayB Λ refundB)))

The seller promises to sign the preliminary contract (signS), provided that either the buyer promises to pay the stipulated amount, or he promises to lose the deposit. Also, the seller promises that if she signs the preliminary contract, then she will either sell her house, or will not sell and refund twice the sum received.

Seller = ((payB V refundB) ։ signS) Λ (signS ։ (sellS V (чsellS Λ refundS)))

A first consequence is that the two contracts lead to an agreement between the buyer and the seller, that is both parties will sign the preliminary contract:

▶ Buyer Λ Seller → signB Λ signS (12)

As a second consequence, if one of the parties does not finalize the final deed of sale, than that party will refund the other:

▶ Buyer Λ Seller Λ чpayB → refundB (13)

▶ Buyer Λ Seller Λ чsellS → refundS (14)

Example 2 (Online sale) We now describe a possible online sale between two parties. In order to buy an item, the buyer has to contact first the bank, to reserve from his account a specific amount of money for the transaction. When this happens, that amount is no longer available for anything else. We model this reservation with the formula lock. Then, the buyer has to make an offer to the seller: this is modelled with offer. The seller, when provided with an offer, evaluates it. If she thinks the offer is good, and the money has been reserved, then she will send the item (send). Otherwise, she cancels the transaction (abort). When the transaction is aborted, the bank cancels the money reservation, so that the buyer can use the amount for other transactions (unlock).

We now formalize this scenario. The buyer agrees to lock Λ offer, provided that either the item is sent, or the money reservation is cancelled. The seller agrees to evaluate the offer. The bank agrees to cancel the reservation when the transaction is aborted.

Buyer = (send V unlock) ։ (lock Λ offer) Seller = offer ։ ((lock → send) V abort) Bank = (lock Λ abort) ։ unlock

Under these assumptions, we can see that either the item is sent, or the transaction is aborted and the reservation cancelled.

▶ (Buyer Λ Seller Λ Bank ) → (send V (abort Λ unlock))

Example 3 (Dining retailers) Around a table, a group of n cutlery retailers is about to have dinner. At the center of the table, there is a large dish of food. Despite the food being delicious, the retailers cannot start eating right now. To do that, and follow the proper etiquette, each retailer needs to have a complete cutlery set, consisting of n pieces, each of a different kind. Each one of the n retailers owns a distinct set of n piece of cutlery, all of the same kind. The retailers start discussing about trading their cutlery, so that they can finally eat. We formalize this scenario as follows. We number the retailers r1, . . . , rn together with the kinds of pieces of cutlery, so that ri initially owns n pieces of kind number i. We then write gi,j for “ri gives a piece (of kind i) to rj”. Since retailers can use their own cVutlery, we assume gi,i to be true. Retailer ri can

start eating whVenever ei = j gj,i. Instead, he provides the cutlery to others

whenever pi =

x xx,x.

Suppose that r1 commits to a simple exchange with r2: they commit to g2,1 ։ g1,2 and g1,2 ։ g2,1, and the exchange takes place since g2,1Λg1,2 can be derived. While this seems a fair deal, it actually exposes r1 to a risk: if r3, . . . , rn perform

a similar exchange with r2, then we have g2,i Λ gi,2 for all i. In particular, gi,2 holds for all i, so r2 can start eating. This is however not necessarily the case for r1, since r3 has not committed to any exchange with r1.

A wise retailer would then never agree to a simple exchange g2,1 ։ g1,2.

Instead, the retailer r1 could commit to a safer contract:

e1 ։ p1 = g1,1 Λ g2,1 Λ · · · Λ gn,1 ։ g1,1 Λ g1,2 Λ · · · Λ g1,n

The idea is simple: r1 requires each piece of cutlery, that is, r1 requires to be able to start eating (e1). When this happens, r1 agrees to provide each other retailer with a piece of his cutlery (p1). Now, assume each retailer ri commits to the analogous contract. We then have the desired agreement (proof in [3]).

^ ^

▶ (ei ։ pi) → xx

x x

3 The Calculus

We now define our calculus of contracting processes.

3.1 Syntax

We use a denumerable set of names, ranged over by n, m, . . ., and a denumer- able set of variables, ranged over by x, y, Metavariables a, b range over both

names and variables. Intuitively, a name plays the same role as in the π-calculus, while variables roughly behave as names in the fusion calculus. That is, distinct names represent distinct concrete objects, each one with its own identity. In- stead, distinct variables can be bound to the same object, so they can be fused. When variable fusion happens, our calculus instantiates the involved variables to a specific name, as we will see.

We extend prime formulae of PCL with parameters: p(a, b). Note that we do not introduce quantifiers in PCL, which then remains a propositional logic. Indeed, the formula p(a, b) is still atomic from the point of view of the logic. We let letters c, d range over formulae, while letters u, v range over {⊥, ч}-free formulae. The syntax of our calculus follows.

P ::= u |

i∈I

πi.Pi | (P |P ) | (a)P | X(→a) (processes)

Processes P are mostlΣy standard, and include the active constraint u, the

sum of guarded processes i πi.Pi, the parallel composition P |P , and the scope

X (→x) = Pi

delimitation (a)P . We use a set of definitions { i . } with the provision

that each occurrence of Xj in Pk is guarded, i.e. it is behind some prefix.

We write 0 for the empty sum, and we use + to merge sums:

i∈I

πi.Pi +

i∈J

πi.Pi =

i∈I∪J

πi.Pi if I ∩ J = ∅

Xxxxxxxxx sums are simply written π.P .

Prefixes π include τ (the standard silent operation as in CCS), as well as ask , tell , check carrying the same meaning as in Concurrent Constraints [33]. The prefix ask c causes a process to stop until the formula c is deducible from the context. Dually, the prefix tell u augments the context with the formula u. Note that, since we only allow negation-free formulae u here, the context will always be consistent, by Lemma 2. The prefix check c checks if c is consistent with the context. The other prefixes fusex c and joinx c drive the fusion of the variable x. The prefix joinx c instantiates x to any known name, provided that after the instantiation the formula c is satisfied. The prefix fusex c fuses x with any other set of known variables, provided that, when all the fused variables are instantiated to a fresh name, the constraint c is satisfied. To avoid unnecessary fusion, the set of variables is required to be minimal. If we use names to model session identifiers, then the difference between joinx c and fusex c becomes evident: a joinx c is used to join an already initiated session, while a fusex c is used to initiate a new session.

Free variables and names of processes are defined as usual: they are free whenever they occur in a process not under a delimitation. Alpha conversion and substitutions are defined accordingly. As a special case, we let:

(fusex c){n/x} = (joinx c){n/x} = ask c

That is, when a variable x is instantiated to a name, the prefixes fusex c and

joinx c can no longer require the fusion of x, so they behave as a plain ask c.

3.2 Semantics

We now define the semantics of processes. Henceforth, we consider processes up-to alpha-conversion. The semantics is then given through a two-layered

transition system (Fig. 3.2). The bottom layer is an LTS −→α between processes,

which provides a compositional semantics. Actions α are as follows, where C

denotes a set of PCL formulae.

α ::= τ | C | C ▶ c | C ▶F c | C ▶J c | C /▶ ⊥ | (a)α (actions)

x x

The action τ represents an internal move. The action C is an advertisement of a set of active constraints. The action C ▶ c is a tentative action, generated by a process attempting to fire an ask c prefix. This action also carries a set C as the collection of active constraints discovered so far. Similarly for C ▶F c and

fusex c, for C ▶J

c and joinx

c, as well as for C /▶ ⊥ and check c. In the last

case, C also includes c. The delimitation in (a)α is for scope extrusion, as in

the labelled semantics of the π-calculus [32]. We write (→a)α to denote a set of distinct delimitations, neglecting their order, e.g. (ab) = (ba). We simply write (→a→b) for (→a ∪ →b).

The first three lines of the rules in Fig. 3.2 handle the base cases of our semantics. The rule Tau allows a τ prefix to fire. The rules Ask, Check, Fuse, and Join simply generate the corresponding actions. The rule Tell adds a con- straint to the environment, thus making it active. Active constraints can then signal their presence through the ConstrΣrule: each constraint generates its own

xxxxxxxxx. A sum of guarded processes π.P can instead signal that it is not

a constraint, by generating the empty set of constraints through IdleSum.

τ ∅⊢c τ

τ.P −→ P [Tau] ask c.P −−→ P [Ask] tell u.P −→ u|P [Tell]

{c}/⊢⊥

∅⊢x c

check c.P −−−−→ P [Check] fusex c.P −−−→ P [Fuse] joinx c.P −−−→ P [Join]

{u}

P ∅ P

u −−→ u [Constr]

i πi.Pi −→

i πi.Pi [IdleSum]

′

(→a)C

P −−−→ P

(→b)C′

Q −−−→ Q′

[ParConstr]

(→a)C

′

P −−−→ P

(→b)(C′⊢c)

Q −−−−−−→ Q′

[ParAsk]

(→a→b)(C∪C′ )

P |Q −−−−−−−→ P ′|Q′

(→a→b)(C∪C′⊢c)

P |Q −−−−−−−−−→ P ′|Q′

(→b)(C′ F

→ ′ J

′

(→a)C

P −−−→ P

⊢x c)

′

Q −−−−−−−→ Q

[ParFuse]

(→a)C

′

P −−−→ P

(b)(C ⊢x c)

Q −−−−−−−→ Q

[ParJoin]

(→a→b)(C∪C′ ⊢F c)

P |Q −−−−−−−−−−→ P ′|Q′

(→a→b)(C∪C′⊢J c)

P |Q −−−−−−−−−−→ P ′|Q′

′

(→a)C

P −−−→ P

(→b)(C′/⊢⊥)

Q −−−−−−→ Q′

P −→ P ′

(→a→b)(C∪C′/⊢⊥)

[ParCheck]

′ τ ′

[ParTau]

′

P |Q −−−−−−−−−→ P ′|Q′

P |Q

−→ P |Q

α ′ →a α ′

πj.Pj −→ P P { /x}→ −→ P .

i πi.Pi

−→α

[Sum]

P ′

if X(→x) = P [Def]

→

X(a→) −α P ′

P −→α P ′ P −→α P ′

(a)P −→ (a)P

if a /∈ α [Del]

′

(a)α

(a)P −−−→ P

[Open]

′

(→a)(C⊢c)

P −−−−−−→ P

(xn→a)(X X c)

′

⊢x

′

if C ⊢ c [CloseAsk] P −−−−−−−−→ P if

Cσ ⊢ cσ,

[CloseJoin]

τ ′ τ

′ σ = {n/x}

P −→ (→a)P P −→ (na)→ P σ

′

(x→y→a)(C⊢xc)

P −−−−−−−−→ P

C ⊢n c,

if x→y

[CloseFuse]

τ ′ n n fresh

P −→ (n→a)P { /x→y}

P −→ P ′

(→a)(C/⊢⊥)

′

P −−−−−−→ P

P ֌ P ′ [TopTau] P ֌ (→a)P ′ if C /⊢ ⊥ [TopCheck]

Figure 1: The transition system for our calculus. Symmetric rules for +, | are omitted. The rules Par* have the following no-capture side condition: →a is fresh in →b, C′, c, x, Q′, while →b is fresh in C, P ′.

The next three lines of rules handle parallel composition. The rule ParConstr merges the sets of constraints advertised by two parallel processes. The rule ParAsk allows for augmenting the constraints C in the tentative action C ▶ c generated by an Ask, by also accounting for the set of constraints advertised by the parallel process. Similarly for the rules ParFuse, ParJoin, ParCheck. The rule ParTau simply propagates τ actions of parallel processes. The Par* rules also merge the set of delimitations; variable and name captures are avoided through a side condition.

The rules Sum, Def are quite standard: they handle external choice and (possibly recursive) definitions, respectively. The rules Del, Open handle delim- itation. As usual, when a is not mentioned in an action, we can propagate the

action across a delimitation (a) using Del. The rule Open instead allows for scope extrusion. Note that Open has no side conditions: the checks needed for scope extrusion are already handled by the Par* rules.

The Close* rules are the crucial ones, since they provide the mechanism to finalize the actions generated by ask, join, and fuse. The rule CloseAsk is the simplest: if the collected constraints C entail c, the ask prefix can indeed fire. In that case, a silent action τ is generated, and the delimitations (→a) can be brought back to the process level, stopping the scope extrusion. The rule CloseJoin is similar to CloseAsk, except it also allows the variable x to be instantiated with a name n. To this purpose, we apply a substitution σ = {n/x} to the constraints

C, c before testing for entailment. If that holds, we apply σ to the residual process P ′ as well. Of course, we need to ensure that all the occurrences of x are substituted: this is done by requiring x to be present in the delimitations of the action in the premise, hence requiring the whole scope of x is at hand. Further, we constrain n in the same fashion, so that x can only be instantiated to an existing name. The rule CloseFuse also causes the instantiation of variables to names. Unlike CloseJoin, however, it cannot instantiate x to an existing name; rather, the name n here is a completely fresh one, introduced in the process through a delimitation. Note that CloseFuse may fuse several variables together, since n substitutes for the whole set x→y. The set →y of the variables to

xy→

be fused with x is chosen according to the local minimal fusion relation C ▶n c,

to be defined in a while (Def. 5).

Summing up, the LTS given by −→α

allows for the generation of tentative

actions for ask, join and fuse (rules Ask,Join,Fuse), which can then be converted

to −→τ

whenever enough constraints are discovered (rules Close*). Then, the τ

action can be propagated towards the top level (rule ParTau). A prefix check c, instead, cannot be handled in the same fashion, since it requires to check the consistency of c with respect to all the active constraints. To this aim, we

−→

use the reduction relation ֌, layered over the α relation. The reduction ֌

only includes internal moves −→τ (rule TopTau) and successful check moves (rule

TopCheck). This effectively discards tentative actions, filtering for the successful ones, only. Note that ֌ is only applied to the top level.

→z

Definition 5 (Local Minimal Fusion) The relation C ▶n c holds whenever:

∃C′ ⊆ C. C′{n/z→} ▶ c{n/z→} Λ ∄w→ Ç →z. C′{n/w→ } ▶ c{n/w→ }

We now briefly discuss the motivations behind this definition. First, we consider a subset C′ of C (locality restriction). Then, we require that C′ entails c when the variables →z are fused. The fusion must be minimal, that is fusing a proper subset of variables must not cause the entailment. The rationale for minimality is that we want to fuse those variables only which are actually involved in the entailment of c – not any arbitrary superset.

To understand the motivations underlying the locality restriction, note that a set of variables →z may be minimal w.r.t. a set of constraints C′, yet not minimal for a superset C ⊃ C′, as the following example shows. Let:

c = p(x) C′ = {q(y) , q(z) V s → p(y)} C = C′ ∪ {s}

To obtain C′ ▶ c, all the variables x, y, z must be fused. It is immediate to see that this fusion is minimal: to produce p(x) we must exploit the implication,

P |0 ≡ P P |Q ≡ Q|P P |(Q|R) ≡ (P |Q)|R

P + 0 ≡ P P + Q ≡ Q + P P + (Q + R) ≡ (P + Q) + R

(a)(P |Q) ≡ P |(a)Q if a /∈ free(P ) (a)(b)P ≡ (b)(a)Q Figure 2: Structural equivalence.

so fusing x with y is mandatory. Further, the hypothesis q(z) V s can only be discharged through q(y), and this forces the fusion of y and z. Instead, to obtain C ▶ c, we can simply fuse x with y; (and neglect z), because the hypothesis q(z) V s can now be discharged through s. So, in this case the set of variables x, y, z is not minimal. This phenomenon could, in principle, lead to unexpected behaviour. Consider, for instance:

P = (x)(y)(z)(fusex c.P | C′) | s

Q = (x)(y)(z)(fusex c.P | C′ | s)

where, with some abuse of notation, C′ stands for the parallel composition of its constraints. In P , when dealing with the process (x)(y)(z)(fusex c.P | C′), we can apply CloseFuse to fuse the variables x, y, z, because only C′ is known at this time, and the set of variables is minimal for C′. Instead, in Q the application of CloseFuse must be deferred until a delimitation (x) is found; at that time the

whole set of constraints C is known, so making the fusion x, y, z not minimal for C. Of course, this phenomenon clashes with our intuition that P and Q should be equivalent, since Q is obtained from P through a scope extrusion.

→z

The key issue here is that minimality is intrinsically non-compositional: dis- covering new constraints can break minimality. To recover compositionality, our definition of C ▶n c does not require →z to be minimal for C, but to be such for

xyz

any subset C′ of C. This allows, for instance, to have both C ▶n c and C ▶n c

in the example above. The intuition behind this is that it is not necessary to

(globally) explore the whole system to decide if a set of contracts leads to an agreement – inspecting any set of (locally) known contracts is enough. To a local observer, a set x, y, z of variables to fuse may appear minimal. To a more informed observer, the same set may appear to be non-minimal (the minimal one being x, y). Both choices for fusion are allowed by our semantics.

Our semantics does not make use of any structural equivalence relation. However, such a relation can be defined as the minimum equivalence satisfying the axioms of Fig. 2. This relation turns out to be a bisimulation.

Theorem 7 The relation ≡ is a bisimulation, i.e.

P ≡ Q −→α

Q′ =⇒ ∃P ′. P −→α

P ′ ≡ Q′

3.3 Examples

We illustrate the semantics through some examples.

Example 4 (Handshaking) Recall the handshaking example from Sect. 1.1:

Xxxxx = (x)

tell b(x) ։ a(x). fusex a(x). lendAirplane

Bob = (y)

tell a(y) ։ b(y). fusey b(y). lendBike

A possible trace is the following:

Xxxxx | Bob

−→τ (x)

b(x) ։ a(x) | fusex a(x). lendAirplane

|Bob

(y)

a(y) ։ b(y) | fusey b(y). lendBike

−→ (n)

−→τ (n)

b(n) ։ a(n) | lendAirplane {n/x}|

a(n) ։ b(n) | ask b(n). lendBike {n/y}

b(n) ։ a(n) | lendAirplane {n/x}|

a(n) ։ b(n) | lendBike {n/y}

In step one, we use Tell,ParTau,Del to fire the prefix tell b(x) ։ a(x). Dually, in step two, we fire the prefix tell a(y) ։ b(y) through the same rules. Step three is the crucial one. There, the prefix fusex a(x) is fired through rule Fuse. Through rules Constr,ParFuse, we discover the active constraint ca = b(x) ։ a(x). We use rule Open to obtain the action (x){ca} ▶ a(x) for the Xxxxx part. For the Bob part, we use rule Constr to discover cb = a(y) ։ b(y), which we then merge with the empty set of constraints obtained through rule Idle; we finally apply Open and obtain (y){cb}. At the top level, we can then apply ParFuse to deduce (x, y){ca, cb} ▶ a(x). Finally, rule CloseFuse here can be applied, fusing x and y by instantiating them to the fresh name n. It is easy to check that

x,y

{ca, cb} ▶n

a(x). Note that the instantiation causes fusey b(y) to transform

into ask b(n), so that it can be fired in the last step.

To better understand the role of contractual implication in this example, consider the following alternative handshaking which makes no use of ։.

Xxxxx′

= (x)

tell a(x). fusex b(x). lendAirplane

Bob′

= (y)

tell b(y). fusey a(y). lendBike

It is straightforward to see that P ′ = Xxxxx′ | Bob′ has analogous behaviour to P = Xxxxx | Bob, since the handshaking is still performed. However, the processes P and P ′ behave quite differently in the presence of a third kid, Xxxx.

Xxxx = (z) fusez a(z). 0

The system P ′ | Xxxx allows Xxxx to fire his own prefix, by fusing x with z. So, Xxxx will be allowed to play with Xxxxx’s airplane, even if Xxxxx is not given anything back. Indeed, after the instantiation, Xxxxx will be stuck on an ask b(n)

x,z

prefix. Technically, this happens because {a(x)} ▶n

a(z) holds. In this case,

Bob will be stuck as well: he can not play with Xxxxx’s airplane since Xxxx took it. By contrast, the system P | Xxxx does not allow Xxxx to play with the airplane. Indeed, Xxxxx specified in her contract that she will lend her airplane only if a bike is provided. Since Xxxx provides no bike, he is not allowed to use the airplane. Instead, Bob can successfully exchange his bike with Xxxxx’s airplane.

Example 5 (Dining retailers) We reuse the formulae of Ex. 3, augmenting each prime formula with a parameter x.

ei(x) = Λjgj,i(x) pi(x) = Λjgi,j(x)

Ri = (x) tell ei(x) ։ pi(x). fusex pi(x). ||x xxxxx,j

As discussed in Ex. 3, we have that Λiei(n) ։ pi(n) is enough to entail pi(n) for all i. So, all the fuse prefixes are fired, and all the givei,j continuations executed. Note that, as a process the above is actually no more complex than the simple handshaking of Ex. 4. Indeed, all the complexity ends up inside the contract, and not in the process code, as it should be.

Example 6 (Insured Sale) We model a seller S who will ship any order as long as she is is either paid upfront, or she receives an insurance from the insurance company I, which she trusts.

s(x) = order(x) Λ (pay(x) V insurance(x)) ։ ship(x)

S = (x)tell s(x).fusex ship(x).(S | doShip(x))

The process S above is recursive, so that many orders can me shipped. The exposed contract is straightforward. Below, we model the insurer. As for the seller, this is a recursive process. The contract used here is trivial: a premium must be paid upfront.

i(x) = premium(x) ։ insurance(x)

I = (x)tell i(x).fusex insurance(x).

I | τ.check чpay(x).(refundS (x) | debtCollect (x))

When an insurance is paid for, the insurer will wait for some time, modelled by the τ prefix. After that is fired, the insurer will check whether the buyer has not paid the shipped goods. In that case, the insurer will immediately indemnify the seller, and contact a debt collector to recover the money from the buyer.

Note that S and I can be specified without the need to explicitly mention a specific buyer. Indeed, the interaction between the parties is loosely specified, so that many scenarios are possible. For instance, the above S and I can interact with the following buyer, paying upfront:

b0(x) = ship(x) ։ order(x) Λ pay(x)

B0 = (x)tell b(x).receive (x)

A buyer can also pay later, if provides insurance:

b1(x) = ship(x) ։ order(x) Λ premium(x)

B1 = (x)tell b(x).(receive (x) | τ.tell pay(x))

Interaction is also possible with an “incautious” buyer which pays upfront with- out asking any shipping guarantees.

b2(x) = order(x) Λ pay(x) B2 = B0

Finally, interaction with a malicious buyer is possible:

b3(x) = order(x) Λ premium(x) B3 = B0

Here, the insurer will refund the seller, and start a debt collecting procedure. This is an example where a violated promise can be detected so to trigger a suitable recovery action. Summing up, note the role of the CloseFuse rule in these scenarios: the minimality requirement makes sure the insurer is involved only when actually needed.

Example 7 (Automated Judge) Consider an online market, where buyers and sellers trade items. The contract of a buyer is to pay for an item, provided that the seller promises to send it; dually, the contract of a seller is to send an item, provided that the buyer pays. A buyer first issues her contract, then waits until discovering she has to pay, and eventually proceeds with the process CheckOut. At this point, the buyer may either abort the transaction (process NoPay), or actually pay the item, by issuing the constraint paid(x). After the item has been paid, the buyer may wait for the item to be sent (ask sent(x)), or possibly open a dispute with the seller (tell dispute(x)).

Buyer = (x) tell send(x) ։ pay(x). fusex pay(x). CheckOut

CheckOut = τ.NoPay + τ. tell paid(x).(τ. tell dispute(x) + ask sent(x))

The behaviour of the seller is dual: issue the contract, wait until she has to send, and then proceed with the process Ship. There, either choose not to send, or send the item and then wait for the payment or open a dispute.

Seller = (y) tell pay(y) ։ send(y). fusey send(y). Ship

Ship = τ.NoSend + τ. tell sent(y).(τ. tell dispute(y) + ask pay(y))

To automatically resolve disputes, the process Judge may enter a session initi- ated between a buyer and a seller, provided that a dispute has been opened, and either the obligations pay or send have been inferred. This is done through the joinz primitive, which binds the variable z to the name of the session established between buyer and seller. If the obligation pay(z) is found, but the item has not been actually paid (i.e. check чpaid(z) passes), then the buyer is convicted (mod- elled by jailBuyer (z ), not further detailed). Similarly, if the obligation send(z) has not been supported by a corresponding sent(z), then the seller is convicted.

Judge = (z)

joinz (pay(z) Λ dispute(z)).check чpaid(z). jailBuyer (z ) |

joinz (send(z) Λ dispute(z)).check чsent(z). jailSeller (z )

A possible trace is the following:

Buyer | Seller | Judge

−→τ (x)

send(x) ։ pay(x) | fusex pay(x). CheckOut

| Seller | Judge

(y)

pay(y) ։ send(y) | fusey send(y). Ship

| Judge

−→ (n)

send(n) ։ pay(n) | CheckOut {n/x} |

pay(n) ։ send(n) | ask send(n). Ship{n/y}

| Judge

−→ (n)

send(n) ։ pay(n) | CheckOut {n/x} | pay(n) ։ send(n) | Ship{n/y}

| Judge

−→ (n)

−→τ (n)

send(n) ։ pay(n) | CheckOut {n/x} | pay(n) ։ send(n) | NoSend

send(n) ։ pay(n) | tell paid(n).(τ. tell dispute(n) + ask sent(n)) |

pay(n) ։ send(n) | NoSend | Judge

send(n) ։ pay(n) | paid(n) | τ. tell dispute(n) + ask sent(n) |

pay(n) ։ send(n) | NoSend | Judge

send(n) ։ pay(n) | paid(n) | tell dispute(n) + ask sent(n) |

pay(n) ։ send(n) | NoSend | Judge

| Judge

−→ (n)

−→τ (n)

send(n) ։ pay(n) | paid(n) | dispute(n) | pay(n) ։ send(n) | NoSend

| Judge

check чsent(n). jailSeller (n) | · · ·

−→τ (n)

jailSeller (n) | · · ·

Example 8 (All-you-can-eat) Consider a restaurant offering an all-you-can- eat buffet. Customers are allowed to have a single trip down the buffet linemeal, where they can pick anything they want. After the meal is over, they are no longer allowed to return to the buffet.

We model this scenario through the following processes:

Buffet = (x) (pasta(x) | chicken(x) | cheese(x) | fruit(x) | cake(x))

Bob = (x) fusex pasta(x) Λ chicken(x). SatiatedB Xxxx = (x) fusex pasta(x).fusex chicken(x). SatiatedC

The Buffet above can interact with either Bob or Xxxx, and make them sati- ated. Here, Bob eats both pasta and chicken in a single meal. By contrast, Xxxx eats the same dishes but in two different meals, thus violating the Buffet policy:

Buffet | Xxxx →∗ SatiatedC | P

Indeed, the Buffet should forbid Xxxx to eat the chicken, i.e. to fire the second fusex . To enforce the Buffet policy, we first define the auxiliary operator ⊕. Let (pi)i∈I be arbitrary PCL formulae. Take a fresh prime symbol r, a fresh name o, and fresh variables z, (zi)i∈I. Then,

i∈I

pi = (o)(z)(zi)i∈I (r(o, z) | ||i∈I r(o, zi) → pi)

To see how this works, consider the process ⊕i∈I pi|Q where Q fires a fusex which demands a subset of the constraints (pi)i∈J with J ⊆ I. To deduce pi we are forced to fuse zi with z (and x); otherwise we can not satisfy the premise r(o, zi). Therefore all the (zi)i∈J are fused, while minimality of fusion ensures that the (zi)i∈I\J are not. After fusion we then reach

(o)(m)

(zi)i∈I\J ( ||i∈I\J r(o, zi) → pi)| ||i∈J (r(o, m)|r(o, m) → pi)

| Q′

where m is a fresh name resulting from the fusion. Note that the (pi)i∈I\J can no longer be deduced through fusion, since the variable z was “consumed” by the first fusion. The rough result is that ⊕i pi allows a subset of the (pi)i∈I to be demanded through fusion, after which the rest is no longer available.

We can now exploit the ⊕ operator to redefine the Buffet as:

Buffet ′ = (x)(pasta(x) ⊕ chicken(x) ⊕ cheese(x) ⊕ fruit(x) ⊕ cake(x))

The new specification actually enforces the desired buffet policy:

Buffet ′ | Xxxx /→∗ SatiatedC | P

4 Expressive power

4.1 Semaphores

Semaphores admit a simple encoding in our calculus. Below, n is the name associated with the semaphore, while x is a fresh variable.

P (n).Q = (x)fusex p(n, x).Q V (n) = (x)tell p(n, x)

Each fusex p(n, x) instantiates a variable x such that p(n, x) holds. Of course, the same x can not be instantiated twice, so it is effectively consumed. New variables are furnished by V (n).

4.2 Memory cell

We model below a memory cell in our calculus. The cell at any time contains a name v as its value.

New (n, v).Q = (x)tell c(n, x) Λ d(x, v).Q

Get (n, y).Q = (w)fusew c(n, w).joiny d(w, y).New (n, y).Q

Set (n, v).Q = (w)fusex c(n, w).New (n, v).Q

Process New(n, v) initializes the cell having name n and initial value v. Process Get(n, y) recovers v by fusing it with y: the procedure is destructive so the cell is re-created. Process Set(n, v) destroys the current cell and creates a new one.

4.3 Xxxxx

Our calculus can model a tuple space, and implement the insertion and retrieval of tuples as in Xxxxx [22]. For illustration, we only consider p-tagged pairs here.

Out (w, y).Q = (x)tell p(x) Λ p1(x, w) Λ p2(x, y).Q

In(w, y).Q = (x)fusex p1(x, w) Λ p2(x, y).Q

In(?w, y).Q = (x)fusex p2(x, y).joinw p1(x, w).Q

In(w, ?y).Q = (x)fusex p1(x, w).joiny p2(x, y).Q

In(?w, ?y).Q = (x)fusex p(x).joinw p1(x, w).joiny p2(x, y).Q

Operation Out inserts a new pair in the tuple space. A fresh variable x is related to the pair components through suitable predicates. Operation In retrieves a pair through pattern matching. The pattern In(w, y) mandates an exact match, so we require that both components are as specified. Note that the fuse prefix will instantiate the variable x, effectively consuming the tuple. The pattern In(?w, y) requires to match only against the second component y. We do exactly that in the fuse prefix. Then, we use join to recover the first component of the pair, and bind it to variable w. Pattern In(w, ?y) is symmetric. Pattern In(?w, ?y) matches with any pair, so we specify a weak requirement for the fusion. Then we recover the pair components.

4.4 Synchronous π-calculus

We can easily encode the synchronous π-calculus in our calculus. Our encoding, shown below, preserves parallel composition, and maps name restriction to name delimitation, as one might desire.

[P |Q] = [P ]|[Q]

[(νn)P ] = (n)[P ]

[a¯⟨b⟩.P ] = (x) msg(x, b)|fusex in(a, x).[P ]

[a(z).Q] = (y) in(a, y)|(z)joinz msg(y, z).[Q]

[X(→a)] = X(→a)

. .

[X(→y) = P ] = X(→y) = [P ]

where x, y are fresh. The output can not proceed with P until x is fused with some y. Dually, the input can not proceed until y is instantiated to a name, that is until y is fused with some x — otherwise, there is no way to satisfy msg(y, z). The encoding above satisfies the requirements of [24]. It is compositional, mapping each π construct in a context of our calculus. Further, the encoding is name invariant and preserves termination, divergence and success. Finally it is

operationally corresponding since, writing →π for reduction in π,

P →∗ P ′ =⇒ [P ] ֌∗∼ [P ′]

[P ] ֌∗ Q =⇒ ∃P ′. Q ֌∗∼ [P ′] Λ P →∗ P ′

where ∼ is ֌-bisimilarity. For instance, note that

[(νm)(n⟨m⟩.P |n(z).Q)] ֌∗

(m)(o) msg(o, m)|[P ]|in(n, o)|[Q]{m/y}

∼ (m)[P |Q{m/y}]

since the name o is fresh and the constraints msg(o, m), in(n, o) do not affect the behaviour of P, Q. To see this, consider the inputs and outputs occurring in P, Q. Indeed, in the encoding of inputs, the fusex prefix will instantiate x to a fresh name, hence not with o. On the other hand, in the encoding of outputs, the joinz prefix can fire only after y has been fused with x, hence instantiated with a fresh name. The presence of msg(o, m) has no impact on this firing.

In our encoding above, we did not handle the choice operator. This is how- ever manageable through the very same technique we will use below to encode graph rewriting, where an operator ⊕ on contracts is defined to properly encode non-deterministic choices.

4.5 Graph rewriting

In the encoding of the π-calculus we have modelled a simple interaction pattern; namely, Xxxxxx-style synchronization. Our calculus is also able to model more sophisticated synchronization mechanisms, such as those employed in graph rewriting techniques [17]. Before dealing with the general case, we introduce our encoding through a simple example.

Example 9 Consider the following rewriting rule:

A2 A3 A4

B2 B3 B4

Above, A1 . . . A4 are processes, while bullets represent shared names. Whenever these processes are in a configuration matching the left side of the rule, a xxxx- sition is enabled leading to the right side. Processes change to B1 . . . B4, and a new name is created, which is shared among all of them, while the old names are forgotten. Modelling this kind of synchronization in, e.g., the π-calculus would be cumbersome, since a discovery protocol must be devised to allow processes to realize the transition is enabled. Note that no process is directly connected to the others, so this protocol is non-trivial.

Our calculus allows for an elegant, symmetric translation of the rule above, which is interpreted as an agreement among the processes A1 . . . A4. Intuitively, each process Ai promises to change into Bi, while adjusting the names, provided all the others perform the analogous action. Since each Ai shares two names with the others, we write it as Ai(n, m). We can now define the advertised contract: below, we denote addition and subtraction modulo four as ⊕ and ⊖, respectively.

ai(n, m, x) = fi⊕1(x, m) Λ si⊖1(x, n) ։ fi(x, n) Λ si(x, m) (15)

An intuitive interpretation of f, s is as follows: fi(x, n) states that n is the first name of some process Ai(n, −) which is about to apply the rule. Similarly for si(x, m) and the second name. The parameter x is a session ID, uniquely iden- tifying the current transition. The contract ai(n, m, x) states that Xx agrees to fire the rule provided both its neighbours do as well. The actual Ai process is as follows.

Ai(n, m) = (x)tell ai(n, m, x).fusex fi(x, n) Λ si(x, m). Bi(x)

Our PCL logic enables the wanted transition:

P = ||i Ai(ni, ni⊕1) ֌∗ (m)||i Bi(m)

Further, note that the above works even when nodes ni are shared among multiple parallel copies of the same processes. For instance, P |P will fire the rule twice, possibly mixing Ai components between the two P’s.

We now deal with the general case of a graph rewriting system.

Definition 6 An hypergraph G is a pair (VG, EG) where VG is a set of vertices and EG is a set of hyperedges. Each hyperedge e ∈ EGi has an associated tag tag(e) and an ordered tuple of vertices (e1, . . . , ek) where ej ∈ VGi . The tag tag(e) uniquely determines the arity k.

Definition 7 A graph rewriting system is a set of graph rewriting rules {Gi ⇒ Hi}i where Gi, Hi are the source and target hypergraphs, respectively. No rule is allowed to discard vertices, i.e. VGi ⊆ VHi . Without loss of generality, we require that the sets of hyperedges EGi are pairwise disjoint.

In Def. 8 below, we recall how to apply a rewriting rule G ⇒ H to a given graph J. The first step is to identify an embedding σ of G inside J. The embedding σ roughly maps H \ G to a “fresh extension” of J (i.e. to the part of the graph that is created by the rewriting). Finally, we replace σ(G) with σ(H).

Definition 8 Let {Gi ⇒ Hi}i be a graph rewriting system, and let J be a hypergraph. An embedding σ of Gi in J is a function such that:

• σ(v) ∈ VJ for each v ∈ VGi , and σ(v) /∈ VJ for each v ∈ VHi \ VGi

• σ(e) ∈ EJ for each e ∈ EGi , and σ(e) /∈ EJ for each e ∈ EHi \ EGi

• σ(v) = σ(v′) =⇒ v = v′ for each v, v′ ∈ VHi \ VGi

• σ(e) = σ(e′) =⇒ e = e′ for each e, e′ ∈ EGi ∪ EHi

• tag(e) = tag(σ(e)) for each e ∈ EGi ∪ EHi

• σ(e)h = σ(eh) for each e ∈ EGi ∪ EHi and 1 ≤ h ≤ k

The rewriting relation J → K holds iff, for some embedding σ, we have

VK = (VJ \ σ(VGi )) ∪ σ(VHi ) EK = (EJ \ σ(EGi )) ∪ σ(EHi )

Note that the assumption VGi ⊆ VHi of Def. 7 ensures that VJ ⊆ VK, so no dangling hyperedges are created through rewriting.

We now proceed to encode graph rewriting in our calculus. To simplify our encoding, we make a mild assumption: we require each Gi to be a connected hypergraph. Then, encoding a generic hypergraph J is performed in a compo- sitional way: we assign a unique name n to each vertex in VJ , and then build a parallel composition of processes Atag(e)(→n), one for each hyperedge e in EJ , where →n = (n1, . . . , nk) identifies the adjacent vertices. Note that since the be- haviour of an hyperedge e depends on its tag, only, we index A with t = tag(e).

Note that t might be the tag of several hyperedges in each source hypergraph Gi. We stress this point: tag t may occur in distinct source graphs Gi, and each of these may have multiple hyperedges tagged with t. The process At must then be able to play the role of any of these hyperedges. The willingness to play the role of such a hyperedge e relatively to a single node n is modelled by a formula pe,h(x, n) meaning “I agree to play the role of e in session x, and my h-th node is n”. The session variable x is exploited to “group” all the constraints related to the same rewriting. We use the formula pe,h(x, n) in the definition of At. The process At(→n) promises pe,1(x, n1), . . . , pe,k(x, nk) (roughly, “I agree to be rewritten as e”), provided that all the other hyperedges sharing a node nh agree to be rewritten according to their roles e¯. Formally, the contract related to e ∈ EGi is the following:

ae(x, →n) =

1 ≤ h ≤ k e¯ ∈ EGi e¯¯ = eh

pe¯,h¯ (x, nh) ։

1≤h≤k

pe,h(x, nh) (16)

Note that in the previous example we indeed followed this schema of con- tracts. There, the hypergraph J has four hyperedges e1, e2, e3, e4, each with a unique tag. The formulae fi and si in (15) are rendered as pei,1 and pei,2 in (16). Also the operators ⊕1 and ⊖1, used in (15) to choose neighbours, are generalized in (16) through the condition e¯h¯ = eh.

Back to the general case, the process At will advertise the contract ae for each e having tag t, and then will try to fuse variable x. Note that, since the neighbours are advertising the analogous contract, we can not derive any pe,h(x, nh) unless all the hyperedges in the connected component agree to be rewritten. Since Gi is connected by hypothesis, this means that we indeed require the whole graph to agree.

However, advertising the contracts ae using a simple parallel composition can lead to unwanted results when non-determinism is involved. Consider two unary hyperedges, which share a node n, and can be rewritten using two distinct

rules: G ⇒ H with e1, e2 ∈ EG, and G¯ ⇒ H¯

with e¯1, e¯2 ∈ EG¯. Let tag(e1) =

tag(e¯1) = t1 and tag(e¯2) = tag(e¯2) = t2. Each process thus advertises two contracts, for instance:

At1 = (x)(ae1(x, n)|ae¯1(x, n)|Fusiont1) At2 = (x)(ae2(x, n)|ae¯2(x, n)|Fusiont2)

Consider now At1|At2. After the fusion of x, it is crucial that both hyperedges agree on the rewriting rule that is being applied – that is either they play the roles of e1, e2 or those of e¯1, e¯2. However, only one Fusion process above will perform the fusion, say the first one:

(m)(ae1(m, n)|ae¯1(m, n)|Rewritee1|ae2(m, n)|ae¯2(m, n)|Fusiont2{m/x})

Above m is a fresh name. Note however that the process Fusiont2{m/x} can still proceed with the other rewriting, since the substitution above can not disable a prefix which was enabled before. So, we can end up with Rewritee¯2, leading to an inconsistent rewriting. Indeed, At1 was rewritten using G ⇒ H, while At2

according to G¯ ⇒ H¯ .

To avoid this, we resort to the construction ⊕ipi discussed in Ex. 8. We can then define At as follows.

At(→n) = (x)(

ae(x, →n)|

fusex

pe,n(x, nh).Be(x, →n))

tag(e)=t

1≤h≤k

In each At, the contracts ae are exposed under the ⊕. The consequences of these contracts are then demanded by a sum of fusex . We defer the definition of Be.

Consider now the behaviour of the encoding of a whole hypergraph: At(→n)| · · · |At′ (→n′).

If the hypergraph J contains an occurrence of G, where G ⇒ H is a rewriting

rule, each of the processes involved in the occurrence P1, . . . , Pl may fire a fusex prefix. Note that this prefix demands exactly one contract ae from each process inside of the occurrence of G. This is because, by construction, each ae under the same ⊕ involves distinct pe,n. This implies that, whenever a fusion is per- formed, the contracts which are not directly involved in the handshaking, but are present in the occurrence of G triggering the rewriting, are then effectively disabled. In other words, after a fusion the sums in the other involved processes have exactly one enabled branch, and so they are now committed to apply the rewriting coherently.

After the fusion Be(x, →n) is reached, where x has been instantiated with a fresh session name m which is common to all the participants to the rewriting. It is then easy to exploit this name m to reconfigure the graph. Each in- volved vertex (say, with name n) can be exposed to all the participants through

e.g. tell verth(m, n), and retrieved through the corresponding joiny verth(m, y). Since m is fresh, there is no risk of interference between parallel rewritings. New vertices (those in VH \ VG) can be spawned and broadcast in a similar fashion. Once all the names are shared, the target hypergraph H is formed by spawning its hyperedges EH through a simple parallel composition of At(→n) processes – each one with the relevant names. Note in passing that the processes At, where t ranges over all the tags, are mutually recursive.

Our encoding [−] satisfies operational correspondence:

J →∗ K =⇒ [J] ֌∗∼ [K]

[J] ֌∗ P =⇒ ∃K. J →∗ K Λ P ֌∗∼ [K]

where ∼ is ֌-bisimilarity. The encoding also preserves termination, divergence and success. Hence, it satisfies the criteria of [24], when the requirements on names are adapted to vertices.

5 Related Work

Various approaches to the problem of providing both clients and services with provable guarantees about each other’s functional behaviour have been studied over the last few years. Yet, at the present no widespread technology seems to give a general solution to this problem.

Recent research papers address the problem of defining contracts that specify the interaction patterns among (clients and) services [8, 9, 10, 27]. For instance, in [9] a contract is a process in a simplified CCS featuring only prefixing, internal and external choice. A client contract is compliant with a service contract if

any possible interaction between the client and the service will always succeed. There, a main problem is how to define (and decide) a subcontract relation, that allows for safely substituting services without affecting the compliance with their clients. Even assuming that services are trusted and respect the published contract, this approach provides the client with no provable guarantees, except that the interaction with the service will “succeed”, that is all the expected synchronizations will take place.

For instance, consider a simple buyer-seller scenario. In our vision, it is important to provide the buyer with the guarantee that, after the payment has been made, then either the payed goods are made available, or a full refund is issued. For the seller, it is important to be sure that a buyer will not repudiate a completed transaction, so to obtain for free the goods already delivered. This could be modelled by the following contracts, assuming a perfect duality between buyer and seller:

Buyer = (ship V refund) ։ pay Seller = pay ։ (ship V refund)

The above two contracts lead to an agreement, which allows the buyer for pay- ing, and the seller for shipping or issuing a refund.

Instead, in [9] the contracts of the buyer and of the seller would take a very different form, e.g.:

Buyer = pay. (ship + refund) Seller = pay. (ship ⊕ refund)

Intuitively, this means that the client will first output a payment, and then either receive the item, or receive a refund (at service discretion). Dually, the service will first input a payment, and then opt for shipping the item or issuing a refund. However, this is very distant from our notion of contracts.

First, the contracts exposed above are quite rigid, in that they precisely fix the order in which the actions must be performed. Even though in some cases this may be desirable, many real-world contracts seem to allow for a more liberal way of constraining the involved parties (e.g., “I will pay before the deadline”). Second, while the crucial notion if the contracts in [9] is compatibility, in our model we focus on the inferring the obligations that arise from a set of contracts. The key difference between the two notions is that, given a set of contracts, a compatibility check results in a yes/no output, while inferring the obligations provides a fine-grained quantification of the reached agreement. For instance, the obligations may identify who is responsible of each action mentioned in the contract. Our processes can then exploit this information to take some recovery

action against clients and services which do not respect their promises.

A lot of work addresses the problem of managing service failures in long- running business transactions, see e.g. [11, 4, 7, 5]. Since, in a long-lived trans- action, the standard rollback mechanism of database systems does not scale, the idea is to partition the long transaction into a sequence of smaller transactions, each of which is associated with a given compensation [19]. Compensations are recovery actions specified by the service designer, that will be run upon failures of the standard execution. For instance, we can model our buyer-seller scenario as follows in Compensating CSP [7]. The seller charges the buyer credit card, and then proceeds by shipping the ordered item. Simultaneously, the seller performs an availability check, to see whether the ordered item is in stock. If the item is not available, the service throws an exception, which triggers the

compensation refundAmount. This compensation restores the original state of the buyer account, so it will actually perform a transaction rollback:

Seller = [ availCheck; (ok; SKIPP notOk; THROWW )

|| (debitAmount ÷ refundAmount) ]; ship

Notice that the choice of the compensation is crucial; while “refundAmount” may be acceptable by any client, if the compensation was instead just a “15%Discount” on the next order, then not all the clients would have been perfectly happy. Ac- tually, our main criticism to long-running transactions is that clients have no control on the compensations provided by services.

In our vision, instead, clients have the right to select those services that offer the desired compensations. For instance, we may exploit our logic to model the contract of a buyer that will pay provided that, if the ordered item is unavailable, then she will obtain a full refund, as well as a 15% discount on the next order:

Buyer =

unavailable → (refund Λ 15%discount)

։ pay

Several logics for modelling contracts have been introduced over the years, taking inspiration and extending e.g. classical [15], modal [14, 1, 20], intuitionis-

tic [2], deontic [31, 21], default [23] and defeasible logics [25]. This flourishing of logics is justified by the many facets of contracts that arise when modelling real- world scenarios, e.g. principals, authorizations, duties, delegation, mandates, regulations, assume-guarantee specifications, etc. (see [3] for a more direct com- parison between these logics and PCL). We think none of these logics, including our PCL, captures all the facets of contracts. Actually, each of the aforemen- tioned logics is designed to represent some particular aspect of contracts, e.g. obligations, permissions and prohibitions in deontic logics, violation of contracts in default and defeasible logics, and agreement in PCL. We argue that, since these aspects are orthogonal, it is possible to extend PCL with features from some of these logics. Note that the key feature of PCL, i.e. the ability of discov- ering which obligations arise from any set of contracts, has allowed us to design the contract-based mechanism used in our calculus to establish sessions.

6 Research Directions

The main design goals for the logic and the calculus proposed in this paper have been minimality and decidability. We expect, however, that some useful constructs can be added to our framework, to make it suitable for modelling even more complex scenarios. Of course, preserving the decidability will be a major concern while considering these extensions, as it will require to revisit the proof of the cut elimination theorem. We discuss below some of the more promising research directions.

First order features. We plan to extend logic with predicates and quanti- fiers. This will allow us to model more accurately those scenarios where a party issues a “generic” contract that can be matched by many parties. While this first order extension shall force us to drop the decidability result, we expect to find interesting decidable fragments of the logic, yet expressive enough to model many relevant situations. For instance, consider an e-commerce scenario, where

a seller promises to ship the purchased item to a given address, provided that the customer will pay for that item. Aiming at generality, we make the seller contract parametric with respect to the item, customer and address. This can be modelled using a universal quantification over these three formal parameters:

Seller = ∀item, cust, addr :

pay(item, cust, addr ) ։ ship(item, addr )

(17)

Now, assume that a customer (say, Bob) promises that he will pay for a drill, provided that the seller will ship the item to his address. This will be modelled by the following contract issued by Bob, where the actual parameters remark that the payment is made by Bob, and that the destination address is Bob’s.

Bob = ship(drill, bobAddress) ։ pay(drill, Bob, bobAddress) Joining the two contracts above will yield the intended agreement:

Seller Λ Bob → pay(drill, Bob, bobAddress) Λ ship(drill, bobAddress)

Principals. We will consider extending our logic with a says modality, simi- larly to [20]. This will enable us to write, x.x. Xxxxx says (b ։ a) to represent the fact that Xxxxx has issued a contract where she promises to lend her airplane, provided that she borrows a bike (note that the binding between principals and contracts is represented outside the logic PCL). Contract agreements shall then come in a richer flavour, because of the binding between the contracting parties and their inferred duties, which is now revealed. Back to our first example of Sect. 1.1, one could expect an handshaking of the following form:

Xxxxx says (b ։ a) X Xxx says (a ։ b) → Xxxxx says a Λ Bob says b

from which it is clear that the duty of Xxxxx is that of lending her airplane, and the duty of Bob is that of lending his bike. This additional information can be exploited by a third party (a sort of “automated” judge) which has to investigate the responsibilities of various parties, in the unfortunate case that a contract is not respected. For instance, if our automated judge is given the evidence that Xxxxx’s airplane has never been lent to Bob, from the above he will infer that (Xxxxx says a) Λ чa. From this, our judge will be able to infer that Xxxxx has not respected her contract (and possibly punish her), which is modelled by the formula Xxxxx says ⊥.

This extension will have some additional benefits, especially when putting it at work in insecure environments populated by attackers. Indeed, an attacker could maliciously issue a “fake” contract, where he makes a promise that he can- not actually implement, e.g. because the promised duty can only be performed by another party. For instance, consider again the contract (17). Assume that an attacker wants to maliciously exploit the seller contract, in order to receive a free item, and make the unaware customer Bob pay for it. To do that, the attacker issues the following contract:

FakeBob = ship(10Kdiamond, fakeAddress) ։ pay(10Kdiamond, Bob, fakeAddress)

Joining the seller and the attacker contracts will then cause an unwelcome sit- uation for Bob, who is due to pay for a 10K diamond, which will be shipped to

the attacker’s address:

Seller Λ FakeBob → pay(10Kdiamond, Bob, fakeAddress) Λ

ship(10Kdiamond, fakeAddress)

To cope with this situation, we could require that each contract p is signed by the principal A who issues it, i.e. it has the form A says p. Revisiting our example with this trick, in the safe case that Bob himself has ordered the item, we would expect to deduce:

Seller Λ Bob → Bob says pay(drill, Bob, bobAddress)

In this case, we have a successful transaction, because Bob is stating that he will pay for his drill. Instead, joining the seller and the attacker contracts produces:

Seller Λ FakeBob → FakeBob says pay(10Kdiamond, Bob, fakeAddress)

Now, it is easy to realize that someone has attempted a fraud, because the principal who has signed the contract (FakeBob) is different from that who is due to pay (Bob).

To exploit this extension also in our calculus, it suffices e.g. to constrain the tell u prefix to formulae u of the form A says u′, where A is the name of the principal running the prefix.

Explicit time. Time is another useful feature that may arise while modelling real-world scenarios. For instance, in an e-commerce transaction, a contract may state that if the customer returns the purchased item within 10 days from the purchase date, then she will have a full refund within 21 days from then. We plan a temporal extension of our logic, so to reason about the obligations that arise when the deadlines expire. Back to our e-commerce example, we could imagine to express the seller contract as the following formula, where the parameter t in p(t) tells the point in time where the “event” p occurs:

Seller (t) = ∀t′ : (pay(t) Λ return(t′) Λ t′ < t + 10) ։ ∃t′′ < t′ + 21 : refund(t′′)

From the point of view of the buyer, the contract says that the buyer is willing to pay, provided that she can obtain a full refund (within 21 days from the date of payment), whenever she returns the item within 7 days from the date of payment:

∀ t < t + 21 : refund(t ) ։ pay(t)

Buyer (t) = t′ : return(t′) Λ t′ < t + 10 → ∃ ′′ ′ ′′

In the presence of an agreement (i.e. a completed e-commerce transaction) between the customer and the seller on (say) January the 1st, 2009, we expect our extended logic able to deduce that, if the customer has returned the pur- chased item on January the 5th, then the seller is required to issue a full refund to the customer within January, the 26th.

Buyer (1.1.09) Λ Seller (1.1.09) Λ return(5.1.09) → ∃t′′ < 26.1.09 : refund(t′′)

There are a number of techniques to explicitly represent time in logical systems, so we expect to be able to reuse some of them for extending PCL.

These techniques range from Temporal Logic [18], to more recent approaches on temporal extensions of authorization logics like [16].

Such a temporal extension to the logic demands for a timed semantics for our calculus. This will allow to check whether a promise is violated in a given trace (e.g. the deadline passed). Another key aspect is characterizing honest and timely processes, i.e. processes that always fulfill their duties on time.

Analysis techniques. We plan to develop analysis techniques to formally and automatically prove the correctness of a service infrastructure, i.e. that the contracts are always respected, without the need for resorting to third parties (e.g. legal offices) external to the model. We will investigate analysis techniques for services and contracts, in order to provide clients and service providers with provable assurances about the behaviour of services. To do that, we will consider a variety of properties, concerning both standalone services and aggregations of services. One of the primary goals of these analyses will be that of determin- ing whether a service actually respects the declared contract, i.e. if the facts promised by the service agree with its behaviour. It is highly desirable to verify a property of this kind before making a service available, because it prevents from the possibility of being legitimately charged for not having fulfilled a signed contract. We will analyse a variety of global properties about aggregations of cooperating services. For instance, we will study what happens when a service provider is not able to fulfill a contract because of an external service that does not deliver the negotiated functionalities. In such a scenario, the goal of our analysis will be that of exactly determining the liabilities of the involved parties, and to decide if it is always possible to compensate the client through suitable recovery actions. We will also focus on deciding if a party can always detect that a signed contract has not been fulfilled. This property is particularly relevant, because in the scenarios where it is respected, we can provide the offended party with the possibility of contesting a contract, by resorting to a third party that enforces its fulfillment.

Whenever the analysis techniques establish the compliance of a service with its own promises, one might wish to apply the techniques of [13] to derive an implementation which securely runs over an untrusted network.

Implementation issues. In our model of contracts we have abstracted from most of the implementation issues. For instance, in insecure environments pop- ulated by attackers, the operation of exchanging contracts requires particular care. Clearly, integrity of contracts is a main concern, so we expect that suitable mechanisms have to be applied to ensure that contracts are not tampered with. Further, establishing an agreement between participants in a distributed system with unreliable communications appears similar to establishing common knowledge among the stipulating parties [26], so an implementation has to cope with the related issues. For instance, the fusex prefix requires a fresh name to be delivered among all the contracting parties, so the implementation must ensure everyone agrees on that name. Also, it is important that participants can be coerced to respect their contracts after the stipulation: to this aim, the

implementation should at least ensure the non repudiation of contracts [37].

7 Conclusions

We have investigated the notion of contract from a logical perspective. To do that, we have first extended intuitionistic propositional logic with a new connective, that models contractual implication. We have provided the new connective with an Xxxxxxx-style axiomatisation, which has allowed us to show some interesting properties and application scenarios for our logic. The main result about our logic is its decidability. To prove that, we have devised a Gentzen-style sequent calculus for the logic, which is equivalent to the Xxxxxxx- style axiomatisation. Decidability then follows from the subformula property, which is enjoyed by our Gentzen rules, and by a cut elimination theorem, which we have proved in full details in [3]. We have implemented a proof search algorithm for PCL.

Our logic for contracts has served as a basic building block for designing a calculus of contracting processes. This is an extension of Concurrent Con- straints, featuring a peculiar mechanism for the fusion of variables, which well suites to formalise contract agreements. We have shown our calculus expressive enough to model a variety of typical scenarios, and to encode some common idioms for concurrency, among which the π-calculus and graph rewriting.

Acknowledgements. Work partially supported by EU-FETPI Global Com- puting Project IST-2005-16004 SENSORIA (Software Engineering for Service- Oriented Overlay Computers) and by the MIUR-PRIN project SOFT. (Tecniche Formali Orientate alla Sicurezza).

References

[1] Mart´ın Abadi, Xxxxxxx Xxxxxxx, Xxxxxx Xxxxxxx, and Xxxxxx Xxxxxxx. A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems, 4(15):706–734, 1993.

[2] Mart´ın Xxxxx and Xxxxxx X. Xxxxxxx. A logical view of composition. The- oretical Computer Science, 114(1):3–30, 1993.

[3] Xxxxxxx Xxxxxxxxxx and Xxxxxxx Xxxxxx. A logic for contracts. Technical Report DISI-09-034, DISI - Universit`a di Trento, 2009.

[4] Xxxxx Xxxxxx, Xxxxxx Xxxxxx, and Xxxxxxxxx Xxxxxxxxx. A calculus for long running transactions. In Proc. FMOODS, 2003.

[5] Xxxxxxx Xxxxx, Xxxx´an X. Xxxxxxxxx, and Xxx Xxxxxxxxx. Theoretical foundations for compensations in flow composition languages. In Proc. POPL, 2005.

[6] Xxxxx Xxxxxx Xxxxxxx and Xxx Xxxxxxxxx. CC-Pi: A constraint-based language for specifying service level agreements. In Proc. ESOP, 2007.

[7] Xxxxxxx X. Xxxxxx, X. X. X. Xxxxx, and Xxxxx Xxxxxxxx. A trace xxxxx- tics for long-running transactions. In 25 Years Communicating Sequential Processes, 2004.

[8] Xxxxxxx Xxxxxxxxx and Xxxxxx Xxxxxx. A basic contract language for web services. In Proc. ESOP, 2006.

[9] Xxxxxxxx Xxxxxxxx, Xxxx Xxxxxxx, and Xxxx Xxxxxxxx. A theory of con- tracts for web services. ACM Transactions on Programming Languages and Systems, 31(5), 2009.

[10] Xxxxxxxx Xxxxxxxx and Xxxx Xxxxxxxx. Contracts for mobile processes. In Proc. CONCUR, volume 5710 of Lecture Notes in Computer Science. Springer, 2009.

[11] Xxxxx Xxxxxxxx, Xxxxxxxxx Xxxxxxx, Xxxxx Xxxxx, Xxxxxxx X. Xxxxxx, Xxxxx Xxxxxxxx, and Xxxxx Xxxxxxxxx. Extending the concept of transaction com- pensation. IBM Systems Journal, 41(4):743–758, 2002.

[12] Xxxxx Xxxxx and Xxxxxxxxxxx Xxxxxx-Xxxxxxxxxxx. Structured communica- tions with concurrent constraints. In Proc. Trustworthy Global Computing (TGC), volume 5474 of Lecture Notes in Computer Science. Springer, 2008.

[13] Xxxxxxx Xxxxx, Xxxxxx-Xxxx Xxxxxxxxx, Xxxxxxx Xxxxxxx, Xxxxxxxxxxx Bhar- xxxxx, and Xxxxx X. Xxxxxx. A secure compiler for session abstractions. Journal of Computer Security, 16(5):573–636, 2008.

[14] Aspassia Daskalopulu and Xxx Xxxxxxx. Towards electronic contract performance. In Proc. 12th International Workshop on Database and Expert Systems Applications, 2001.

[15] Xxxxx Xxxxxxx, Xxxxxxx Xxxxx, and I.V. Xxxxxxxxxxxx. CTR-S: A logic for specifying contracts in semantic web services. In Proc. WWW04, 2004.

[16] Xxxxx XxXxxxx, Xxxxxx Xxxx, and Xxxxx Xxxxxxxx. An authorization logic with explicit time. In Proc. CSF, 2008.

[17] Xxxxxxx Xxxxx. Tutorial introduction to the algebraic approach of graph grammars. In Proc. of the Workshop on Graph-Grammars and Their Ap- plication to Computer Science, 1987.

[18] X. Xxxxx Xxxxxxx. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 995– 1072. North-Holland Pub. Co./MIT Press, 1990.

[19] Xxxxxx Xxxxxx-Xxxxxx and Xxxxxxx Xxxxx. Sagas. In SIGMOD Conference, 1987.

[20] Xxxxxx Xxxx and Mart´ın Abadi. A modal deconstruction of access control logics. In Proc. FoSSaCS, pages 216–230, 2008.

[21] Xxxxxxxx Xxxxxx, Xxxxxxxx Xxxxxx, Xxxxxxxx Xxxxxx, and Xxxxx Xxxxxxx- xxxx. Normative autonomy and normative co-ordination: Declarative power, representation, and mandate. Artificial Intelligence and Law, 12(1-2):53– 81, 2004.

[22] Xxxxx Xxxxxxxxx. Generative communication in Xxxxx. ACM Transactions on Programming Languages and Systems, 7(1):80–112, 1985.

[23] Xxxxxxxx X. Xxxxxxxxx and Xxxxxxxx Xxxxxxxxxxx. The representation of e-contracts as default theories. In New Trends in Applied Artificial Intelli- gence, 2007.

[24] Xxxxxxx Xxxxx. Towards a unified approach to encodability and separation results for process calculi. In Proc. CONCUR, 2008.

[25] Xxxxx Xxxxxxxxxxx. Representing business contracts in RuleML. Interna- tional Journal of Cooperative Information Systems, 14(2-3), 2005.

[26] Xxxxxx X. Xxxxxxx and Xxxxx Xxxxx. Knowledge and common knowledge in a distributed environment. J. ACM, 37(3):549–587, 1990.

[27] Xxxx Xxxxxxxx. Contract-based discovery and adaptation of web services. In SFM, 2009.

[28] Xxxxxxx Xxxxxx and Bj¨xxx Xxxxxx. The fusion calculus: Expressiveness and symmetry in mobile processes. In LICS, 1998.

[29] The PCL web site. xxxx://xxx.xxxx.xxxxx.xx/∼xxxxxx/PCL.

[30] Xxxxx Xxxxxxxx. Structural cut elimination - I. intuitionistic and classical logic. Information and Computation, 157(1/2):84–141, 2000.

[31] Xxxxxxxx Xxxxxxxxxx and Xxxxxxx Xxxxxxxxx. A formal language for electronic contracts. In Proc. FMOODS, 2007.

[32] Xxxxxx Xxxxxxxxx and Xxxxx Xxxxxx. The π-calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.

[33] Xxxxx Xxxxxxxx, Xxxxxxx Xxxxxxxxxx, and Xxxxxx Xxxxxx. Semantic foun- dations of concurrent constraint programming. In Proc. POPL, pages 333– 352. ACM, 1991.

[34] Xxxxxxx Xxxxxxx. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67–72, 1979.

[35] Xxxx Xxxxxxxxx and Xxxx xxx Xxxxx. Constructivism in Mathematics, vol.

1. North-Holland, 1988.

[36] Xxxxxx Xxxxxxx, Xxxxx Xx Xxxxxx, Xxxxxxx Xxxxxxx, Xxxxxxxx X. Xx¨lzl, Xxxxxxx Xxxxxx, Xxxxx Xxxxxxxxxx, and Xxxxxxxxx Xxxxxxxxx. Sensoria pro- cess calculi for service-oriented computing. In Proc. TGC, 2006.

[37] Xxxxxxxx Xxxx. Non-repudiation in Electronic Commerce. Artech House, 2001.

Document Metadata

Table of Contents

DIPARTIMENTO DI INGEGNERIA E SCIENZA DELL’INFORMAZIONE

Document Metadata