Bogdan Aman

Gabriel Ciobanu

Coordinating Parallel Mobile Ambients to Solve SAT Problem in Polynomial Number of Steps

In this paper we present a version of mobile ambients, called parMA, having a weak form of replication and a parallel semantics. We investigate how parMA can solve intractable problems in a polynomial number of computational steps. We use parMA to give a semiuniform solution to a well-known strong NP-complete problem, namely to the Boolean satisfiability problem (SAT).

Introduction

Ambient calculus is a formalism for describing distributed and mobile computing [START_REF] Cardelli | Mobile Ambients[END_REF]. In contrast with the π-calculus [START_REF] Milner | Communicating and Mobile Systems : the π-Calculus[END_REF] where mobility is expressed by communication, the ambient calculus uses an explicit notion of movement given by moving actions (in and out) together with an "opening" action and (local) communication. An ambient is a named location, and it represents the unit of movement. The authors of [START_REF] Cardelli | Mobile Ambients[END_REF] introduce the mobile ambients as "a paradigm of mobility where computational ambients are hierarchically structured, where agents are confined to ambients and where ambients move under the control of agents". Their initial goal was "to make mobile computation scale-up to widely distributed, intermittently connected and well administered computational environments". The resulting ambient model is elegant and powerful, well suited for expressing issues of mobile computations as working environment, allowing access to information or resources [START_REF] Aman | Timed Mobile Ambients for Network Protocols[END_REF][START_REF] Hirschkoff | Using Ambients to Control Resources[END_REF]. Many variants have been proposed; among them, we mention mobile safe ambients [START_REF] Levi | Mobile Safe Ambients[END_REF], push and pull ambient calculus [START_REF] Hirschkoff | Using Ambients to Control Resources[END_REF] and boxed ambients [START_REF] Bugliesi | Access Control for Mobile Agents: the Calculus of Boxed Ambients[END_REF]. Despite the fact that the initial motivation of mobile ambients assumes a high degree of parallelism in their evolution, the usual semantics of the proposed variants is the interleaving semantics.

Some results show that mobile ambients have the computational power of Turing machines by encoding into ambient calculus (or fragments of it) some formalisms known to be Turing complete: asynchronous π-calculus [START_REF] Cardelli | Mobile Ambients[END_REF][START_REF] Charatonik | Finite-control Mobile Ambients[END_REF], counter machines [START_REF] Busi | On the Expressive Power of Movement and Restriction in Pure Mobile Ambients[END_REF] and Turing machines [START_REF] Cardelli | Mobile Ambients[END_REF][START_REF] Maffeis | On the Computational Strength of Pure Ambient Calculi[END_REF]. A link between mobile ambients and π-calculus is established in [START_REF] Ciobanu | Encoding Mobile Ambients into the π-calculus[END_REF], where it is proven that pure mobile ambients can be embedded into a fragment of the π-calculus, namely in the localized sum-free synchronous monadic π-calculus with matching and mismatching. Other authors relate ambients to security issues and to system biology. Some simulators were also developed [START_REF] Fournet | An Asynchronous, Distributed Implementation of Mobile Ambients[END_REF] in which the evolution of mobile ambients can be observed easily (see http://www-sop.inria.fr/mimosa/ambicobjs/).

Many formal machine models (e.g., Turing machines) have an infinite number of memory locations. Mobile ambients are computing devices of finite size having a finite description with a fixed amount of initial resources (ambients and processes), that can evolve to a possibly infinite family of mobile ambients obtained by replication in order to solve a (decision) problem. A decision problem X is a pair (I X , θ X ) such that I X is a language over a finite alphabet (whose elements are called instances) and θ X is a total boolean function (that is, a predicate) over I X . Its solvability is defined through the recognition of the language associated with it. Let M be a Turing machine with the working alphabet Γ , L a language over Γ , and the result of any halting computation is yes or no. If M is a deterministic device, it recognizes or decides L whenever, for any string u over Γ , if u ∈ L, then M accepts u (the result on input u is yes), or M rejects u (the result on input u is no). If M is a non-deterministic device, it recognizes or decides L whenever, if for any string u over Γ , u ∈ L, and only if there exists a computation of M with input u such that the answer is yes.

According to [START_REF] Garey | Computers and Intractability. A Guide to the Theory of NP-Completeness[END_REF], the NP-complete problems are divided into weak (e.g., Knapsack) and strong (e.g., SAT) depending on the size of the input. We show how a parallel version of mobile ambients with a weak form of replication can solve NP-complete problems in a polynomial number of steps. We provide a semiuniform solution to the best known strong NP-complete problem (SAT) in a polynomial number of steps [START_REF] Papadimitriou | Computational Complexity[END_REF]. To give such a solution, we treat mobile ambients as "deciding devices" that respect the following conditions: (1) all computations halt, (2) two special names yes and no are used, and (3) in a halting configuration a channel ans is ready to output one of the names yes and no; the computation is accepting if yes is present in the halting configuration, and rejecting if no is present in the halting configuration on channel ans. Mobile ambients respect these conditions if we impose some constraints:

• We use a true concurrent semantics allowing processes to run in parallel.

The key rule is

P → P and Q → Q implies P | Q → P | Q .
This parallel semantics is natural if we recall that in [START_REF] Cardelli | Mobile Ambients[END_REF] a process is described as "running even when the surrounding ambient is moving", aspect which the interleaving semantics does not reflect properly. Other reasons to consider a parallel semantics are presented in [START_REF] Fournet | An Asynchronous, Distributed Implementation of Mobile Ambients[END_REF] where the authors present a distributed implementation of mobile ambients.

• A restricted form of replication is used by considering a weaker duplication operator which only doubles a process; this means that a reduction rule !P → P | P is used instead of the congruence rule !P ≡ P | !P or instead of the reduction rule !P → P | !P . This duplication rule is also used by R. Milner in [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF]. It helps in controlling all the computations to halt (and so fulfilling condition 1. of deciding devices). • We use a special symbol that helps in delimiting the computational steps.

is a purely technical device that is used in the subsequent for-malization of the structural operational semantics of parMA; intuitively, P specifies a process P which is temporarily stalled and so cannot execute any action. • We use two kinds of action rules: → and φ ⇒. The former is an execution of a set of actions, and the latter is used to remove all occurrences of (using a tree parsing algorithm) in order to start a new round of parallel actions.

The differences between parallel and interleaving semantics is underlined also in [START_REF] Boer | A Timed Linda Language and its Denotational Semantics[END_REF]: "The parallel construct is interpreted in terms of interleaving, as usual in many (timed) process algebras . . . . Alternatively one could adopt maximal parallelism, which means that at each moment every enabled process of the system is activated". In defining a parallel semantics, we follow the solution used also in [START_REF] Busi | On the Computational Power of the Mate/Bud/Drip Brane Calculus: Interleaving vs. Maximal Parallelism[END_REF] where such a semantic is defined in brane calculi [START_REF] Cardelli | Brane Calculi -Interactions of Biological Membranes[END_REF], a process algebra related to BioAmbients [START_REF] Regev | BioAmbients: An Abstraction for Biological Compartments[END_REF].

The paper is organised as follow. Section 2 defines the syntax and semantics of parallel mobile ambients (parMA). In Section 3 we give some notions of complexity, and show how to solve SAT problem in a polynomial number of steps. Section 4 illustrates how mobile ambients compute effectively by considering a SAT instance with three clauses and three variables as an example. Conclusion and references end the paper.

Parallel Mobile Ambients

In this section we present a variant of mobile ambients having a parallel semantics. Initially, mobility in ambient calculus involved the authorization to enter or exit certain domains in order to access information; the access to information is controlled at many levels: local computer, local area network, regional area network, wide-area intranet and internet. We consider a framework given by mobile ambients hierarchically structured inside a well-defined environment, where ambients move under the control of agents running inside them.

Syntax

Table 1 describes the syntax of parMA. The name Env represents the environment in which the mobile ambients reside, and can appear only once, at the top of the hierarchical structure. Process 0 is an inactive process (it does nothing). A movement M.P is provided by the capability M , followed by the execution of process P . An ambient a[P ] represents a bounded place labelled by a in which a process P is executed. P | Q is a parallel composition of processes P and Q. An output action c a .P releases a name a on channel c, and then behaves as process P . An input action c(x). P captures a name from channel c, and binds it to a variable x within the scope of process P .

A weak form of replication, namely the duplication of a process P (producing two parallel copies of process P ) is denoted by !P . The process P is used to state that process P is temporarily "stalled".

Operational Semantics

The first component of the operational semantics of parMA is the structural congruence ≡. It is the smallest congruence such that the equalities from Table 2 hold. Its role is to rearrange a process in order to apply the action rules given in Table 3. The axioms from Table 2 describe the commutativity and associativity of the parallel composition.

P | Q ≡ Q | P (P | Q) | R ≡ P | (Q | R) P | 0 ≡ P !0 ≡ 0
The set f n(P ) of free names of a process P is defined as:

f n(P )=                    ∅ if P = 0 f n(R) ∪ {a} if P = in a.R or P = out a.R or P = open a.R or P = a[R] f n(R) ∪ {a, c} if P = c a .R f n(R) ∪ {c} if P = c(x).R f n(R) ∪ f n(Q) if P = R | Q f n(R) if P =!R
Table 3 introduces two kinds of action rules: P → P and P φ ⇒ P . The former is an execution of a set of actions, and the latter is used to remove all occurrences of in order to start a new round of parallel actions. The first five rules of Table 3 are one-step reductions for in, out, open, communication and duplication. In rule (Com), by P {a/x} we denote the substitution by a of each free occurrence of variable x in process P . The next three rules propagate reductions across ambient nesting and parallel composition. In rule (Par2), by R → is denoted a process R that cannot evolve. Rule (Struct) allows the use of structural congruence during reduction. When no rule can be applied in Env, rule (Step) is used to delete all occurrences of in order to start a new round of transitions. It can be noticed that in rules (Par2) and (Step) we use negative premises: an activity is performed based on the absence of actions. This is due to the fact that sequencing the evolution can only be defined using negative premises, as done for sequencing processes [4, ?,21].

Table 3: Reduction Rules (In) a = Env b = Env a[in b. P | Q] | b[R] → b[a[ P | Q] | R] (Out) a = Env b = Env a[b[out a. P | Q] | R] → b[ P | Q] | a[R] (Open) a = Env open a. P | a[Q] → P | Q (Com) c a . P | c(x). P → P | P {a/x} (Dupl) !P → P | P (Amb) P → Q a[P ] → a[Q] (Par1) P → P Q → Q P | Q → P | Q (Par2) P → Q R → P | R → Q | R (Struct) P ≡ P, P → Q, Q ≡ Q P → Q (Step) Env[P ] → P φ ⇒ φ(P )
The rules of Table 3 define execution of processes. A complete computational step in mobile ambients is captured by a derivation of the form

Env[P ] → φ ⇒ Env[P ]
. This means that a derivation is a compressed representation of a sequence of individual actions followed by a reinitialization step (removing of all symbols).

Example

To illustrate the basic components of parMA, we use an example in which several students wish to move from the campus to the university and back, having the possibility to use either a tram or a bus. The scenario involves eight ambients and four processes.

Env[campus[student[P 1 | P 4 ] | student[P 1 | P 4 ] | tram[P 2 | P 4 ] | bus[P 3 | P 4 ]] | univ[student[P 1 | P 4 ]]]
The role of the ambients is suggested by their names. The processes are:

• P 1 = Q 1 | Q 2 Q 1 = in tram.c(x).c(x).c(x).out tram.Q 1 Q 2 = in bus.c(x)
.c(x).c(x).c(x).out bus.Q 2

• P 2 = c(x).out campus.c(x).in univ.P 2 P 2 = c(x).out univ.c(x).in campus.P 2 • P 3 = c(x).out campus.c(x).c(x).in univ.P 3 P 3 = c(x).out univ.c(x).c(x).in campus.P 3 • P 4 = c a .P 4

The communication on channel c, that takes place inside ambients, is used to model the fact that the tram, bus and students perform the following actions:

• the first c(x) from P 2 , P 2 , P 3 and P 3 represents the fact that the bus and tram, once inside the campus or univ, are willing to wait for students that intend to travel between campus and univ. • the others c(x) from P 2 , P 2 , P 3 and P 3 are used to model the fact that the movement of the tram and bus between campus and univ takes a number of steps (equal with the number of input actions on channel c). • all c(x) from Q 1 and Q 2 are used to prevent the students from getting out of the tram or bus before reaching the desired location.

It can be noticed that both students from campus can enter either the bus or the tram. Suppose both choose the tram. Then the mobile ambient

Env[campus[student[P 1 | P 4 ] | student[P 1 | P 4 ] | tram[P 2 | P 4 ] | bus[P 3 | P 4 ]] | univ[student[P 1 | P 4 ]]] evolves to Env[campus[tram[ out campus.c(x).in univ.P 2 | P 4 | student[ c(x).c(x).c(x).out tram.Q 1 | Q 2 | P 4 ] | student[ c(x).c(x).c(x).out tram.Q 1 | Q 2 | P 4 ]] | bus[ out campus.c(x).c(x).in univ.P 3 | P 4 ]] | univ[student[P 1 ]]]
The tram and the bus are still inside campus since they communicated on channel c in order to permit the willing students to get inside them. At this moment it can be noticed that only rule (Step) can be applied in order to eliminate the symbols , obtaining the mobile membrane Env[campus[tram[out campus.c(x).in univ.P

2 | P 4 | student[c(x).c(x).c(x).out tram.Q 1 | Q 2 | P 4 ] | student[c(x).c(x).c(x).out tram.Q 1 | Q 2 | P 4 ]] | bus[out campus.c(x).c(x).in univ.P 3 | P 4 ]] | univ[student[P 1 ]]]
After three steps, the tram is inside univ where it waits for the students to exit/enter it, while the bus is still between the two campus and univ, being ready to enter univ in the next step. Thus the next mobile ambient is obtained

Env[campus[ ] | bus[in univ.P 3 | P 4 ] | univ[tram[P 2 | P 4 | student[out tram.Q 1 | Q 2 | P 4 ] | student[out tram.Q 1 | Q 2 | P 4 ]] | student[P 1 ]]]
In the next step the two students from the tram get out inside univ, while the student that was waiting enters the tram in order to reach campus. The obtained mobile ambients is

Env[campus[ ] | univ[bus[P 3 | P 4 ] | tram[out univ.c(x).in campus.P 2 | P 4 | student[c(x).c(x).c(x).out tram.Q 1 | Q 2 | P 4 ]] | student[P 1 ] | student[P 1 ]]]
The mobile ambient continues to change, but we stop here since we have illustrated the expressive power of the proposed formalism.

Solving NP-Complete Problems in Polynomial Steps

As stated in the introduction, we use mobile ambients as deciding devices, in which all computation starting from the initial ambient agree on the result. A family MA, a collection of ambients, solves a decision problem if for each instance of the problem there is a member of the family able to decide on the instance. In order to define the notions of (semi)uniformity, we denote:

• for a suitable alphabet O, each instance of the decision problem is encoded as a string v over O; • V = {v 1 , . . .} -the language of encoded instances of the given problem;

• MA(v) -the member of MA which solves the instance v;

• MA n -the member of MA which solves all instances of length n. Inspired by the uniformity conditions applied to families of Boolean circuits [START_REF] Borodin | On Relating Time and Space to Size and Depth[END_REF], we imposed similar ones on families of processes. By imposing certain resource restrictions (on number of steps and space) to the function that constructs each member of the family MA, it can be ensured that the set of problems decided by the family does not increase. The function is called an

• uniformity condition if an instance size is mapped to a mobile ambient that decides all instances of that length; • semiuniformity condition if a single instance is mapped to a mobile ambient that decides that instance.

Definition 2. If we consider a set of problem instances V = {v 1 , v 2 , . . .}, two classes of functions E, F and a total function t : N → N, such that:

1. there exist a F -uniform family of mobile ambients MA = {MA 1 , . . .}; this means that there exist a function f ∈ F , f : MA is sound and complete with respect to V , then we say that the class of problems V is solved by an (E, F )-uniform family of mobile ambients MA, and denote the family by (E,F)-MA(t). The set of languages decided by a uniform family of mobile ambients in a polynomial number of steps is defined as (E,F)-PMA = k∈N (E,F)-MA(n k ).

{1} * → MA such that f (1 n ) = MA n ,
Semiuniformity is a generalization of uniformity, namely Definition 3. If we consider a set of problem instances V = {v 1 , v 2 , . . .}, a class of functions H and a total function t : N → N, such that:

1. there exist a H-semiuniform family of mobile ambients MA = {MA v1 , MA v2 , . . .}; namely, there exist a function h ∈ H, h :

V → MA such that h(v i ) = MA vi ; 2. MA is t-efficient: MA n halts in t(|v n |) steps; 3.
MA is sound and complete with respect to V , then we say that the class of problems V is solved by an (H)-semiuniform family of mobile ambients MA, and denote the family by (H)-MA(t). The set of languages decided by a semiuniform family of mobile ambients in a polynomial number of steps is defined as (H)-PMA = k∈N (H)-MA(n k ).

Boolean Satisfiability Problem

The SAT problem checks the satisfiability of a propositional logic formula in conjunctive normal form (CNF). Let {x 1 , x 2 , . . . , x n } be a set of Boolean variables. A formula in CNF is of the form

ϕ = C 1 ∧ C 2 ∧ • • • ∧ C m where each C i , 1 ≤ i ≤ m is a disjunction of the form C i = y 1 ∨ y 2 ∨ • • • ∨ y r (r ≤ n),
where each y j is either a variable x k or its negation ¬x k . In this section we show how, starting from a formula ϕ, to construct a process P that provides a semiuniform solution to the SAT problem by using mobile ambients with parallel semantics and duplication (for an instance of SAT we construct a mobile ambient which decides it). We start with the process P = P 1 | Q 1 in which P 1 is used to provide the answer to the problem when placed in parallel with Q 1 , a process that generates all possible assignments over the set {x 1 , x 2 , . . . , x n } of Boolean variables. In what follows we describe how each of these two processes are constructed starting from the ϕ formula.

process Q 1 is defined recursively using the processes

Q i (1 ≤ i < n) and Q n .
For each variable x i from the set {x 1 , x 2 , . . . , x n } of Boolean variables, we construct a process Q i defined as follows:

Q i = x i t i .x z .x z | x i f i .x z .x z | |!x i (y i ).(x(y).x(y).open k i | k i [Q i+1 ]), for 1 ≤ i < n Q n = x n t n | x n f n |!x n (y n ).A[x 1 y 1 | . . . | x n y n | y 1 a | . . . | y 1 a | . . . | y n a | . . . | y n a | Q]. where: • process Q contains terms of the form t k (b).in C j (if x k appears in C j ) or f k (b).in C j (if ¬x k appears in C j ). For example if we consider a 3CNF satisfiability problem with ϕ = C 1 ∧ C 2 ∧ C 3 and X = {x 1 , x 2 , x 3 }, C 1 = x 1 ∨ ¬x 3 , C 2 = ¬x 1 ∨ ¬x 2 and C 3 = x 2 we have Q = t 1 (b).in C 1 | f 3 (b).in C 1 | f 1 (b).in C 2 | f 2 (b).in C 2 | t 2 (b)
.in C 3 • each ambient A will contain a different assignment over the set {x 1 , x 2 , . . . , x n } of Boolean variables; after Q n is executed, there will be 2 n ambients A, obtained by using the duplication operator ! that proceeds the processes that generate an A ambient. • y j a | . . . | y j a stands for m parallel processes y j a , one for each disjunction, and, after all y j are instantiated, are used to communicate with the processes from Q. • x z .x z are used to introduce a delay that prevents that an ambient k i containing a Q i+1 is not opened to soon and cause unwanted evolutions. process P 1 has the form:

P 1 = C 1 [. . . [C m [J[x(y) . . . x(y) | x z . . . x z .K[out J]] | L[in A.ans yes | in K.ans no ]]
]] where:

• to each disjunction C i , 1 ≤ i ≤ m we associate an ambient C i ;

• the ambients C i , 1 ≤ i ≤ m are placed one inside the other, forming an ambient structure of depth m. The order in which these ambients are placed is not important (thus the construction is not unique), but for simplicity we consider the ambient

C 1 [. . . [C m [. . .]] . . .]
• the previous ambient is used to check if there exists an assignments over the set {x 1 , x 2 , . . . , x n } of Boolean variables that respects all these disjunctions. If such an assignment exists, this means that an ambient A containing this assignment, will eventually reach inside ambient C m (an ambient A enters an ambient C i if the assignment placed inside A respect the disjunction C i ) • x(y) . . . x(y) stands for a 2n + m + 1 sequence of capabilities x(y), and together with x z . . . x z that stands for a 2n + m + 1 sequence of capabilities x z , introduces a delay equal with the number of steps needed by an ambient A to get inside ambient C m , before the ambient K exits ambient J. It can be noticed that if an ambient A gets near the ambient L (inside ambient C m ), this ambient enters the ambient A, generates the yes answer and prevents K to generate the negative answer (the ambient K cannot interact with the ambient L inside the ambient A).

In what follows we explain how these two processes (P 1 and Q 1 ) once constructed from the ϕ formula, can generate an answer to the problem.

Starting from P 1 the evolution in the first 2n + 1 steps is given by the rule P i → φ ⇒ P i+1 , where P i+1 is obtained from P i by performing a communication on channel x. In parallel, starting from the process Q 1 , are generated 2 n ambients A that contain all possible assignments over the variables {x 1 , . . . , x n }, namely each assignment is contained inside an ambient A.

Next we describe in detail the evolution of Q 1 . We have two cases.

Case 1: For 1 ≤ i ≤ n -1, the evolution of each

Q i = x i t i .x z .x z | x i f i .x z .x z | !x i (y i ).(x(y).x(y).open k i | k i [Q i+1 ]
) from the 2 i-1 processes Q i running in parallel, starts with a duplication, because any other reduction is not possible. The process that duplicates is in fact the process containing the ambient labelled by k i in which the process Q i+1 is placed. This is done because the variables y 1 , . . . , y i-1 , i ≥ 2 are already instantiated in the process Q i+1 , and we want to create two new copies: one in which y i is replaced by t i , and one in which y i is replaced by f i , keeping also the already instantiated variables. We obtain the process:

Q 1 i = x i t i .x z .x z | x i f i .x z .x z | x i (y i ).(x(y).x(y).open k i | k i [Q i+1 ]) | x i (y i ).(x(y).x(y).open k i | k i [Q i+1 ]) At this moment Q 1
i has two input actions on channel x i , and two output actions on channel x i that are ready to communicate the values of t i and f i . This means that two (Comm) rules are applied in parallel, leading to:

Q 2 i = x z .x z | x z .x z | x(y).x(y).open k i | k i [Q i+1 {t i /y i }] | x(y).x(y).open k i | k i [Q i+1 {f i /y i }]
After the communications on channels x i are performed, the communication of t i+1 and f i+1 inside Q i+1 on channels x i+1 takes place in two steps. This motivates a delay in opening the ambients k i , such that the communication from all k i running in parallel does not get mixed up on channels x i+1 , leading to some unwanted assignments. The obtained process is:

Q 3 i = x z | x z | x(y).open k i | k i [Q 1 i+1 {t i /y i }] | x(y).open k i | k i [Q 1 i+1 {f i /y i }]
The channels x i+1 are ready to communicate inside the processes Q i+1 , and so the capabilities open k i are released in the next step.

Q 4 i = open k i | k i [Q 2 i+1 {t i /y i }] | open k i | k i [Q 2 i+1 {f i /y i }]
Once the communication inside ambients k i on channels x i+1 has finished, these ambients are opened, thus obtaining

Q 5 i = Q 3 i+1 {t i /y i } | Q 3 i+1 {f i /y i } Since the process Q 5
i does not contain any capabilities or replication operators, except the ones from Q 3 i+1 , it means that each Q i evolves for 5 steps, from which 3 steps are in parallel with the ones from Q i+1 .

• Alternatively, if after 2n + m + 1 steps there is no ambient A inside ambient C 3 , then ambient K exits ambient J, and so allowing the ambient L to enter ambient K and to release a no answer on channel ans.

Conclusion

There are a large number of process calculi used to model complex systems in which interactions and mobility are essential (e.g., [START_REF] Aman | Mobility in Process Calculi and Natural Computation[END_REF]). Following this research line, we have previously extended mobile ambients with timers [START_REF] Aman | Timed Mobile Ambients for Network Protocols[END_REF] and types [START_REF] Aman | Mobile Ambients with Timers and Types[END_REF] in order to study their ability of modelling complex systems in distributed networks.

In this paper we use mobile ambients with a parallel semantic (parMA) in order to study their complexity aspects. Thus we provide a semiuniform solution of the SAT problem in a polynomial number of steps by using mobile ambients with a weak form of replication which work according to a parallel semantics.

As far as we know, this is a first attempt to use mobile ambients with parallelism (as they were introduced initially) to create an algorithm that solves an NP-complete problem in a polynomial number of steps. In this way, we show how the mobile ambients can be coordinated to solve problems. There are several topics that could be investigated as further work, including finding other hard problems and complexity classes that can be solved using mobile ambients or related formalisms (process calculi).

Definition 1 .

 1 The family MA (i) decides V if for any string v ∈ O * , the mobile ambient MA(v) (or MA n for all instances v, |v| = n) generates an yes answer whenever v ∈ V and a no answer otherwise; (ii) is sound with respect to V when, for any string v ∈ O * , if there exists an accepting computation of MA(v) (MA n ), then v ∈ V ; (iii) is complete with respect to V when, for any string v ∈ O * , if v ∈ V , then every computation of MA(v) (MA n ) is accepting.

Table 1 :

 1 Parallel Mobile Ambients Syntax

	c	channel name	P, Q ::=	processes
	a, b, Env	ambient names	0	inactivity
	x, y	variables	M.P	movement
	M ::=	capabilities	a[P ]	ambient
	in a	can enter a	P | Q	composition
	out a	can exit a	c a .P	output action
	open a	can open a	c(x).P	input action
			!P	duplication
			P	stalled

Table 2 :

 2 Structural Congruence P ≡ P

  namely all instances v k of length n are solved by MA n , where MA n can be constructed by a function f ∈ F ; 2. there exists an encoding function e ∈ E such that e(v) is the input process of MA n , for |v| = n; 3. MA is t-efficient: MA n halts in t(n) steps (e.g., MA is polynomial efficient if t(n) is polynomial in n for all n); 4.

Acknowledgements

The work of Bogdan Aman and Gabriel Ciobanu was supported by a grant of the Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-II-ID-PCE-2011-3-0919.

from the 2 n-1 processes Q n running in parallel, starts with a duplication rule, obtaining

and after communications of t n or f n on channels x n :

Starting from P 1 | Q 1 , after 2n + 1 steps we obtain P 2n+2 | Q , where:

To illustrate how such a process Q looks, we give a small example in which n = m = 2, we have 2 2 = 4 ambients generated by Q 1 , and process Q is:

As it can be noticed, the four ambients A contain all the Boolean assignments over the variables {x 1 , x 2 }, namely {t 1 , t 2 }, {t 1 , f 2 }, {f 1 , t 2 }, {f 1 , f 2 }, and each possible assignment t i and f i is kept as an output value on channel x i .

After obtaining all possible assignments, we need to check which one satisfies all the clauses C j . To do this, we use the processes Q that contain either terms of the form t k (b).in C j meaning that x k appears in C j , or of the form f k (b).in C j meaning that ¬x k appears in C j . To be able to use the capability in C j , there should be a t k a , respectively a f k a inside the ambient A, both resulting from the instantiation of y k . All ambients that satisfy the clause C j enter in parallel the ambient C j . If there exist at least one ambient A that contains in C 1 | . . . | in C m , it means that this ambient can go inside ambient C m , and contains a solution to the SAT problem; in this case the ambient L enters the ambient A placed inside membrane C m , releasing the yes answer on channel ans (1 step). Otherwise, ambient K exits ambient J, and so ambient L enters K; thus the no answer is send on channel ans (2 steps).

We have a deterministic evolution of the mobile ambients, and so no interference (redex overlapping) exists in our solution of SAT problem. This motivates the use of mobile ambients rather than safe mobile ambients [START_REF] Levi | Mobile Safe Ambients[END_REF].

Analysis

If n is the number of variables (x 1 , . . . , x n ), and m is the number of clauses (C 1 , . . . , C m ), then the number of ambients, capabilities and duplication operators in the initial process is given by the sum of:

• 3 ambients and 4n + 2m + 7 capabilities in process P 1 ; • 10 capabilities, 1 ambient and 1 replication operator in each Q i , 1 ≤ i < n;

• n + 3 + mn capabilities, 1 ambient and 1 replication operator in Q n ;

• maximum 4m capabilities in Q.

Thus, the total size of the initial process is O(mn). The maximum number of computational steps performed in an execution is equal with 2n+m+3, a number determined by:

• 2n + 1 steps to generate all the possible Boolean assignments over a set of variable {x 1 , . . . , x n }; • m steps required by a solution to move inside ambient C m ;

• either 1 step to generate a yes answer on channel ans, or 2 steps to generate a no answer on channel ans.

It is straightforward to show that:

• sound and complete: P 1 | Q 1 says yes iff the given SAT instance is satisfiable;

• function H required for the above construction is in P.

Proposition 1. Using parMA, NP-complete problems can be solved in a polynomial number of steps.

An Example of How Mobile Ambients Solve 3CNF-SAT

To illustrate how mobility can "compute" and solve hard problems, we consider a 3CNF satisfiability problem with

In this case n = 3 and m = 3. We start with the mobile ambient:

The evolution of this term (by applying duplication and communication rules) leads in the first 2n + 1 = 2 * 3 + 1 = 7 steps to the generation of all the possible truth assignments over a set of variables {x 1 , x 2 , x 3 ). Since we have described in the previous section how Q 1 evolves to Q 5 1 , here we just enumerate the first five obtained ambients. In what follows we bold the capabilities and ambients involved actively in an evolution step.

and then we substitute Q 3 2 processes for obtaining

In the next step the communication on all channels x takes place in parallel, leading to all the possible assignments placed inside ambients A.

3 processes in order to see how the assignments look.

From this point forward, the performed steps are:

• Since all the possible assignments are generated, we open in parallel all ambients k 2 such that all ambients A become siblings with the ambient C 1 , ready to start the checking stage. Also all possible communications inside ambients A are performed, thus launching the in C j capabilities corresponding to the clauses C j . • In the next m = 3 steps, the solutions of ϕ should go inside ambient C 3 .

First, the solutions of C 1 go inside ambient C 1 in parallel. • Next, from the solutions of C 1 are selected the solutions of C 2 , namely the solutions are all moved inside ambient C 2 in parallel. • Finally, the solutions of C 3 are selected among the solutions of C 1 and C 2 , namely the solutions which move in parallel inside ambient C 3 . • Since we have an ambient A inside ambient C 3 , an yes answer is released on channel ans in the next step. In parallel, ambient K comes out of ambient J, but since ambient L is not present, the no answer cannot be sent on channel ans.


Massimo Bartoletti

Emilio Tuosto

Roberto Zunino

On the realizability of contracts in dishonest systems

We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon -unlike in traditional approaches based on behavioural types. We consider the contracts of [10], and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts.

Introduction

Contracts are abstract descriptions of the behaviour of services. They are used to compose services which are compliant according to some semantic property, e.g. the absence of deadlocks [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Carpineti | A basic contract language for web services[END_REF][START_REF] Castagna | A theory of contracts for web services[END_REF], the satisfacion of a set of constraints [START_REF] Buscemi | CC-Pi: A constraint-based language for specifying service level agreements[END_REF], or of some logical formula [START_REF] Artikis | Specifying norm-governed computational societies[END_REF][START_REF] Bartoletti | A calculus of contracting processes[END_REF][START_REF] Prisacariu | A formal language for electronic contracts[END_REF]. Most of the existing approaches tacitly assume that, once a set of compliant contracts has been found, then the services that advertised such contracts will behave accordingly. In other words, services are assumed to be honest, in that they always respect the promises made.

In open and dynamic systems, the assumption that all services are honest is not quite realistic. In fact, services have different individual goals, are made available by different providers, and possibly do not trust each other. What happens is that services agree upon some contracts, but may then violate them, either intentionally or not. Since this situation may repeatedly occur in practice, it should not be dealt with as the failure of the whole system. Instead, contract violations should be automatically detected and sanctioned by the service infrastructure.

The fact that violations may be sanctioned gives rise to a new kind of attacks, that exploit possible discrepancies between the promised and the runtime behaviour of services. If a service does not accurately behave as promised, an attacker can induce it to a situation where the service is sanctioned, while the attacker is reckoned honest. A crucial problem is then how to avoid that a service results culpable of a contract violation, despite of the honest intentions of its developer. More formally, the problem is that of deciding if a process realizes a contract: when this holds, the process is guaranteed to never be culpable w.r.t. the contract in all the possible execution contexts.

In this paper we develop a formal theory of contract-oriented systems that enjoys a sound criterion for establishing if a process always realizes its contracts. Our theory combines two basic ingredients: a calculus of contracts, and a calculus of processes that use contracts to interact. Contracts are used by distributed participants to reach agreements; once stipulated, participants can inspect them and decide what to do next.

Ideally, a honest participant is supposed to harmoniously evolve with her contracts; more realistically, our theory also encompasses computations of dishonest participants, which may violate at run-time some contracts they have stipulated. A remarkable result (Theorem 2) is that it is always possible to detect who is culpable of a contract violation at each state of a computation. Also, a participant can always exculpate herself by performing the needed actions (Theorems 1 and 3).

Notably, instead of defining an ad-hoc model, we have embedded the contract calculus in [START_REF] Castagna | A theory of contracts for web services[END_REF] within the process calculus CO 2 [START_REF] Bartoletti | Contracts in distributed systems[END_REF]. To do that, the contracts of [START_REF] Castagna | A theory of contracts for web services[END_REF] have been slightly adapted to define culpability, and CO 2 has been specialized to use these contracts. We have formalised when a participant realizes a contract in a given context, i.e. when she is never (irreparably) culpable in computations with that context, and when she is honest, i.e. when she realizes all her contracts, in all possible contexts. We have proved that the problem of deciding whether a participant is honest or not is undecidable (Theorem 4). Our main contribution (Theorem 6) is a sound criterion for detecting when a participant is honest. Technically this is achieved through a semantics of participants that abstracts away the behaviour of the context. Such semantics allows us to define when a participant always fulfills her contracts, even in the presence of dishonest participants.

Because of space constraints, we include the proofs of all our statements in a separated Technical Report [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF].

A calculus of contracts

We assume a finite set of participant names (ranged over by A, B, . . .) and a denumerable set of atoms (ranged over by a, b, . . .). We postulate an involution co(a), also written as ā, extended to sets of atoms in the natural way.

Def. 1 introduces the syntax of contracts, taking inspiration from [START_REF] Castagna | A theory of contracts for web services[END_REF]. We distinguish between (unilateral) contracts c, which model the promised behaviour of a single participant, and bilateral contracts γ, which combine the contracts of two participants.

A says (a ; c ⊕ c ′ ) | B says (ā . d + d ′ ) A says a -----→ → A says c | B says ready ā.d [INTEXT] A says (a ; c ⊕ c ′ ) | B says ā ; d A says a -----→ → A says c | B says ready ā.d [INTINT] A says (a . c + c ′ ) | B says (ā . d + d ′ ) A says a -----→ → A says c | B says ready ā.d [EXTEXT]
A says ready a. c | B says d Intuitively, the internal sum i∈I a i ; c i allows to choose one of the branches a i ; c i , to perform the action a i , and then behave according to c i . Dually, the external sum ∑ i∈I a i . c i constrains to wait for the other participant to choose one of the branches a i . c i , then to perform the corresponding a i and finally behave according to c i . Separators ; and . allow us to distinguish singleton internal sums (e.g., a ; c) from singleton external sums (e.g., a . c). The atom e (for "end") enables a participant to successfully terminate, similarly to [START_REF] Castagna | A theory of contracts for web services[END_REF]. This will be reflected in Def. 4. Hereafter, we shall always consider contracts with no free occurrences of recursion variables X. We shall use the binary operators to isolate a branch in a sum: e.g. (a ; c) ⊕ c ′ where c ′ is an internal sum. We let ; and . have higher precedence than ⊕ and +, e.g., a ; c

A says a -----→ → A says c | B says d [RDY] a ∈ co({b i } i∈I ) A says a ; c ⊕ c ′ | B says ∑ i∈I b i . d i A says a -----→ → A says E | B says 0 [INTEXTFAIL] {a} = co({b i } i∈I ) A says a ; c ⊕ c ′ | B says i∈I b i ; d i A says a -----→ → A says E | B says 0 [INTINTFAIL] ({a} ∪ {a i } i∈I ) ∩ co({b i } i∈J ) = / 0 A says (a . c + ∑ i∈I a i . c i ) | B says ∑ i∈J b i . d i A says a -----→ → A says E | B says 0 [EXTEXTFAIL]
⊕ b ; c ′ = (a ; c) ⊕ (b ; c ′ ).
The evolution of bilateral contracts is modelled by a labelled transition relation 1 and under the structural congruence relation ≡, defined as the least congruence which includes α-conversion of recursion variables, and satisfies rec X. c ≡ c{ rec X. c /X} and i∈ / 0 a i ; c i ≡ ∑ i∈ / 0 a i . c i . Accordingly, empty sums (either internal or external) will be denoted with 0. We will not omit trailing occurrences of 0. Hereafter we shall consider contracts up to ≡.

In the first three rules in Fig. 1, A and B expose complementary actions a, ā. In rule [INTEXT], participant A selects the branch a in an internal sum. Participant B is then forced to commit to the corresponding branch ā in his external sum: this is done by marking that branch with ready ā while discarding all the other branches. Participant B will then perform his action in the subsequent step, by rule [RDY]. In rule [INTINT], both participants make an internal choice; a reaction is possible only if one of the two is a singleton -B in the rule -namely he can only commit to his unique branch. Were B exposing multiple branches, the transition would not be allowed, to account for the fact that B could pick a conflicting internal choice w.r.t. that of A. In rule [EXTEXT], both participants expose external sums with complementary actions, and each of the two can choose a branch (unlike in the case [INTEXT], where the internal choice has to move first). In the [*FAIL] rules, the action chosen by A is not supported by B. Then, A will reach the success state E, while B will fall into the failure state 0.

Example 1. Let γ = A says (a ; c 1 ⊕ b ; c 2 ) | B says (ā . d 1 + c . d 2 )
. If the participant A internally chooses to perform a, then γ will take a transition to A says c 1 | B says ready ā.d 1 . Suppose instead that A chooses for perform b, which is not offered by B in his external choice. In this case, γ will take a transition to A says E | B says 0, where 0 indicates that B cannot proceed with the interaction. Coherently with [START_REF] Castagna | A theory of contracts for web services[END_REF], below we will characterise this behaviour by saying that the contracts of A and B are not compliant.

The following lemma states that bilateral contracts are never stuck unless both participants have contract 0. Actually, if none of the first four rules in Fig. 1 can be applied, the contract can make a transition with one of the [*FAIL] rules.

Lemma 1. A bilateral contract A says c | B says d is stuck iff c = d = 0.
Below we establish that contracts are deterministic. This is guaranteed by the requirement (ii) of Def. 1. Determinism is a very desirable property indeed, because it ensures that the duties of a participant at any given time are uniquely determined by the past actions. Note that the contracts in [START_REF] Castagna | A theory of contracts for web services[END_REF] satisfy distributivity laws like (a ; c) ⊕ (a ; d) = a ; (c ⊕ d), which allow for rewriting them so that (ii) in Def. 1 holds. Therefore, (ii) is not a real restriction w.r.t. [START_REF] Castagna | A theory of contracts for web services[END_REF].

Lemma 2 (Determinism). For all

γ, if γ µ - → → γ ′ and γ µ - → → γ ′′ , then γ ′ = γ ′′ .
Compliance. Below we define when two contracts are compliant, in a similar fashion to [START_REF] Castagna | A theory of contracts for web services[END_REF]. Intuitively, two contracts are compliant if whatever sets of choices they offer, there is at least one common option that can make the contracts progress. Differently from [START_REF] Castagna | A theory of contracts for web services[END_REF], our notion of compliance is symmetric, in that we do not discriminate between the participant roles as client and server. Consequently, we do not consider compliant two contracts where only one of the parties is willing to terminate. For example, the buyer contract ship ; E is not compliant with the seller contract ship . pay ; E, because the buyer should not be allowed to terminate if the seller still requires to be paid.

Similarly to [START_REF] Castagna | A theory of contracts for web services[END_REF], given two contracts we observe their ready sets (Def. 3) to detect when the enabled actions allow them to synchronise correctly.

Definition 3 (Compliance).

For all contracts c, we define the set of sets RS(c) as:

RS(0) = { / 0} RS(ready a.c) = {{ready }} RS(rec X. c) = RS(c) RS( i∈I a i ; c i ) = {{a i } | i ∈ I} if I = / 0 RS(∑ i∈I a i . c i ) = {{a i | i ∈ I}} if I = / 0
The relation ⊲⊳ between contracts is the largest relation such that, whenever c ⊲⊳ d: The following lemma provides an alternative characterization of compliance. Two contracts are compliant iff, when combined into a bilateral contract γ, no computation of γ reaches a state where one of the contracts is 0. Together with Lemma 1, we have that such γ will never get stuck. (Below, the Kleene * denotes reflexive transitive closure.)

(1) ∀X ∈ RS(c), Y ∈ RS(d). co(X ) ∩ Y = / 0 or ready ∈ (X ∪ Y ) \ (X ∩ Y ) 4 (2) A says c | B says d µ - → → A says c ′ | B says d ′ =⇒ c ′ ⊲⊳ d ′ When c ⊲⊳ d,

Lemma 3. For all bilateral contracts

γ = A says c | B says d: c ⊲⊳ d ⇐⇒ ∀c ′ , d ′ . γ - → → * A says c ′ | B says d ′ =⇒ c ′ = 0 and d ′ = 0
The following lemma guarantees, for all c not containing 0, the existence of a contract d compliant with c. Intuitively, we can construct d from c by turning internal choices into external ones (and viceversa), and by turning actions into co-actions. Lemma 4. For all 0-free contracts c, there exists d such that c ⊲⊳ d.

Culpability. We now tackle the problem of determining who is expected to make the next step for the fulfilment of a bilateral contract. We call a participant A culpable in γ if she is expected to perform some action so to make γ progress. Also, we consider A culpable when she is advertising the "failure" contract 0. This agrees with our [*FAIL] rules, which set A's contract to 0 when the other participant legitimately chooses an action not supported by A. Note that we do not consider A culpable when her contract has enabled e actions.

Definition 4. A participant A is culpable in

γ = A says c | B says d, written A ˙˙ γ, iff: c = 0 ∨ γ A says e ----→ → ∧ ∃a. γ A says a ----→ → When A is not culpable in γ we write A ˙˙ γ.
The following result states that a participant A is always able to recover from culpability by performing some of her duties. Furthermore, this requires at most two steps in an "A-solo" trace where no other participant intervenes.

Definition 5. Let -→ be an LTS with labels of the form

A i says (• • • ), for A i ranging over participants names. For all A, we say that a - →-trace η is A-solo iff η only contains labels of the form A says (• • • ). If η = (µ i ) i∈0..n , we will write η -→ for µ 0 -→ • • • µ n -→.

Theorem 1 (Contractual exculpation). For all

γ = A says c | B says d with 0-free c, there exists γ ′ and A-solo η with |η| ≤ 2 such that γ η -→ → γ ′ and A ˙˙ γ ′ .
commutative monoidal laws for | on processes and systems

u[(v)P] ≡ (v) u[P] if u = v Z | (u)Z ′ ≡ (u)(Z | Z ′ ) if u ∈ fv(Z) ∪ fn(Z) (u)(v)Z ≡ (v)(u)Z (u)Z ≡ Z if u ∈ fv(Z) ∪ fn(Z) A[K] | A[P] ≡ A[K | P] ↓ s c ≡ 0 ≡ fuse s . P Fig. 2.
Structural equivalence for CO 2 (Z, Z ′ range over systems or processes)

A crucial property of culpability is to ensure that either two participants are both succeeding, or it is possible to single out who has to make the next step. An external judge is therefore always able to detect who is violating the contracts agreed upon.

Theorem 2. For all c, d if c ⊲⊳ d and

A says c | B says d -→ → * γ = A says c ′ | B says d ′ , then either c ′ and d ′ succeed, or A ˙˙ γ, or B ˙˙ γ.
Example 3. A participant might be culpable even though her contract succeeds. For instance, let γ = A says c | B says d, where c = e + ā and d = a + b. By Def. 1 we have that c succeeds, but A is culpable in γ because she cannot fire e, while she can fire ā by rule [EXTEXT]. This makes quite sense, because A is saying that she is either willing to terminate or to perform ā, but the other participant is not allowing A to terminate. Note that also B is culpable, because he can fire a.

A Calculus of Contracting Processes

We now embed the contracts introduced in § 2 in a specialization of the parametric process calculus CO 2 [START_REF] Bartoletti | Contracts in distributed systems[END_REF]. Let V and N be two disjoint countably infinite sets of session variables (ranged over by x, y, . . .) and session names (ranged over by s,t, . . .). Let u, v, . . . range over V ∪ N . Definition 6. The abstract syntax of CO 2 is given by the following productions:

Systems S ::= 0 A[P] s[γ] S | S (u)S Processes P ::= ↓ u A says c ∑ i π i .P i P | P (u)P X( u) Prefixes π ::= τ tell A ↓ u c fuse u do u a ask u φ
The only binder for session variables and names is the delimitation ( u), both in systems and processes. Free variables/names are defined accordingly, and they are denoted by fv( ) and fn( ). A system or a process is closed when it has no free variables.

Systems are the parallel composition of participants A[P] and sessions s[γ].

A latent contract ↓ x A says c represents a contract c (advertised by A) which has not been stipulated yet; upon stipulation, x will be instantiated to a fresh session name. We impose that in a system A[P] | A[Q] | S, either P or Q is a parallel composition of latent contracts. Hereafter, K, K ′ , . . . are meta-variables for compositions of latent contracts. We allow prefix-guarded finite sums of processes, and write π 1 .P 1 + π 2 .P 2 for ∑ i=1,2 π i .P i , and 0 for ∑ / 0 P. Recursion is allowed only for processes; for this we stipulate that each process identifier X has a unique defining equation X(u 1 , . . . , u j ) def = P such that fv(P) ⊆ {u 1 , . . . , u j } ⊆ V and each occurrence of process identifiers in P is prefix-guarded. We shall take the liberty of omitting the arguments of X( u) when they are clear from the context. Prefixes include silent action τ, contract advertisement tell A ↓ u c, contract stipulation fuse u , action execution do u a, and contract query ask u φ. In each prefix π = τ, u refers to the target session involved in the execution of π. We omit trailing occurrences of 0.

A[τ.P + P ′ | Q] - → A[P | Q] [TAU] A[tell B ↓ x c.P + P ′ | Q] - → A[P | Q] | B[↓ x A says c] [TELL] K ⊲ σ x γ u = dom σ s = σ(x) fresh ( u)(A[fuse x .P + P ′ | K | Q] | S) - → (s)(A[P | Q]σ | s[γ] | Sσ) [FUSE] γ A says a -----→ → γ ′ s[γ] | A[do s a.P + P ′ | Q] - → s[γ ′ ] | A[P | Q] [DO] γ ⊢ φ A[ask s φ.P + P ′ | Q] | s[γ] - → A[P | Q] | s[γ] [ASK] X( u) def = P P{ v / u } - → P ′ X( v) - → P ′ [DEF] S - → S ′ S | S ′′ - → S ′ | S ′′ [PAR] S - → S ′ (u)S - → (u)S ′ [DEL]
Note that participants can only contain latent contracts, while sessions can only contain bilateral contracts, constructed from latent contracts upon reaching agreements.

The semantics of CO 2 is formalised by a reduction relation -→ on systems that relies on the structural congruence defined in Fig. 2, where the last law allows for collecting garbage terms possibly arising from variable substitutions.

Definition 7. The relation -

→ is the smallest relation closed under the rules of Fig. 3, defined over systems up to structural equivalence, as defined in Fig. 2. The relation

K ⊲ σ x γ holds iff (i) K has the form ↓ y A says c |↓ z B says d, (ii) c ⊲⊳ d, (iii) γ = A says c |
B says d, and (iv) σ = { s /x,y,z} maps all x, y, z ∈ V to s ∈ N .

Rule [TAU] simply fires a τ prefix as expected. Rule [TELL] advertises a latent contract ↓ x A says c, by putting it in parallel with the existing participants and sessions (the structural congruence laws in Fig. 2 allow for latent contracts to float in a system and, by the second last law, to move across the boxes of participants as appropriate). Rule [FUSE] finds agreements among the latent contracts K of A; an agreement is reached when K contains a bilateral contract γ whose unilater contracs are compliant (cf. Def. 7). Note that, once the agreement is reached, the compliant contracts start a fresh session containing γ. Rule [DO] allows a participant A to fulfill her contract γ, by performing the needed actions in the session containing γ (which, accordingly, evolves to γ ′ ). Rule [ASK] checks if a condition φ holds in a session. The actual nature of φ is almost immaterial in this paper: the reader may assume that φ is a formula in an LTL logic [13]. For closed γ and φ, γ ⊢ φ holds iff γ |= LT L φ according to the standard LTL semantics where, for a -→ →-trace η = (γ i µ i -→ → γ i+1 ) i from γ 0 = γ, we define η |= a ⇐⇒ ∃A. µ 0 = A says a. The last three rules are standard.

Hereafter it will be sometimes useful to record the prefix π fired by A by implicitly decorating the corresponding reduction step, as in

A : π --→.
The rest of this section is devoted to a few examples that highlight how bilateral contracts can be used in CO 2 .

Example 4. Consider an online store A with the following contract c A : buyers can add items to the shopping cart, and then either leave the store or pay with a credit card. Assume the store modelled as the CO 2 process P A = (x) (tell A ↓ x c A . X | fuse x ), where:

c A = rec Z. addToCart . Z + creditCard . (ok ⊕ no) + e X def = do x addToCart.X + do x creditCard.(τ.do x ok + τ.do x no)
Let B be a buyer with contract c B = addToCart ; creditCard ; (ok + no), and let:

P B = (y) tell A ↓ y c B .Y Y def = do y addToCart. do y creditCard. do y ok A possible, successful, computation of the system S = A[P A ] | B[P B ]
is the following:

S - → * (x, y) A[↓ x A says c A |↓ y B says c B | fuse x | X] | B[Y ] - → (s) A[X{ s /x}] | B[Y { s /y}] | s[A says c A | B says c B ] - → * (s) A[X{ s /x}] | B[do s creditCard. do y ok] | s[A says c A | B says creditCard ; (ok + no)] - → * (s) A[τ.do x ok + τ.do x no] | B[do y ok] | s[A says ok ⊕ no | B says ok + no] - → (s) A[do x ok] | B[do y ok] | s[A says ok ⊕ no | B says ok + no] - → * (s) A[0] | B[0] | s[A says E | B says E]
Example 5. An on-line store A offers buyers two options: clickPay or clickVoucher. If a buyer B chooses clickPay, A accepts the payment (pay) otherwise A checks the validity of the voucher with V, an electronic voucher distribution and management system. If V validates the voucher, B can use it (voucher), otherwise he will pay. The contracts c A = clickPay.pay + clickVoucher.(reject; pay ⊕ accept; voucher) and c ′ A = ok + no model the scenario above. A CO 2 process for A can be the following

P A = (x)(tell A ↓ x c A .(do x clickPay.do x pay + do x clickVoucher.((y)tell V ↓ y c ′ A .X))) X = do y ok.do x accept.do x voucher + do y no.do x reject.do x pay + τ.do x reject.do x pay Contract c A (resp. c ′ A ) is stipulated when (i) B (resp. V) advertises to A (resp. V) a contract d with c A ⊲⊳ d (resp. c ′ A ⊲⊳ d) and
(ii) a fuse z is executed in A (resp. V). Variables x and y in P A correspond to two separate sessions, where A respectively interacts with B and V. The semantics of CO 2 ensures that x and y will be instantiated to different session names (if at all).

The advertisement of c ′ A causally depends on the stipulation of the contracts of A and B, otherwise A cannot fire do x clickVoucher. Instead, A and B can interact regardless the presence of V since tell V ↓ y c ′ A is non blocking and the τ-branch of A in X is enabled (letting A to autonomously reject the voucher, e.g. because B is not entitled to use it).

Example 6. Consider a travel agency A which queries in parallel an airline ticket broker F and a hotel reservation service H in order to complete the organization of a trip. The travel agency service A[P] can be defined as follows: where the τ actions model timeouts used to ensure progress. The travel agency in process X starts buying a ticket, and commits to it only when the hotel reservation session y is started. Similarly for process Y .

P = (x, y)(tell F ↓ x ticket ; (commitF ⊕ abortF).X | tell H ↓ y hotel ; (commitH ⊕ abortH).Y ) X def =
The next example shows a peculiar use of ask whereby a participant inspects a stipulated contract to decide its future behaviour.

Example 7. An online store A can choose whether to abort a transaction (abort) or to commit to the payment (commit). In the latter case, the buyer has two options, either he pays by credit card (creditCard) or by bank transfer (bankTransfer). The contract of A is modelled as c = abort ⊕ commit; (creditCard + bankTransfer). the process

P A = (x)(tell A ↓ x c. (ask x φ. do x commit. do x creditCard + do x abort))
where φ = (commit → ¬ bankTransfer). The process P A first advertises c. Once a session s[γ] is initiated with γ = A says c | B says d, A tests γ through ask x φ before committing to the payment. If ask x φ detects that B has promised not to use the bank transfer option, then A commits to the payment, and then never offers B to perform a bank transfer. Otherwise, if d does not rule out the bank transfer, even if B might actually pay by credit card, A aborts the session. Note that in both cases A realizes her own contract, even if she is never performing the bank transfer. This notion of "realization of a contract" will be formalized in Def. 11.

On honesty

In this section we set out when a participant A is honest (Def. 11). Intuitively, we consider all the possible runs of all possible systems, and require that in every session A is not definitely culpable. To this aim, we first provide CO 2 with the counterpart of the (non)culpability relation introduced in Def. 4. Intuitively, we write A ˙˙ s S when, in the system S, if the participant A is involved in the session s, then she is not culpable w.r.t. the contract stipulated therein.

Definition 8. We write

A ˙˙ s S whenever ∀ u, γ, S ′ . S ≡ ( u)(s[γ] | S ′ ) =⇒ A ˙˙ γ .

We write A ˙˙ S whenever A ˙˙ s S for all session names s.

A technical issue is that a participant may not get a chance to act in all the traces. For instance, let S = A[do s pay] | B[X] | S ′ , where S ′ enables A's action and X def = τ.X; note that S generates the infinite trace S -→ S -→ S -→ • • • in which A never pays, despite her honest intention. To account for this fact, we will check the honesty of a participant in fair traces, only, i.e. those where persistent transitions are eventually followed.

∀i ∈ N, µ ∈ L . i ≤ |η| ∧ (∀ j ∈ N. i ≤ j ≤ |η| =⇒ P j µ -→) =⇒ ∃ j ≥ i. µ j = µ
A fair trace is a trace which is fair w.r.t. all the labels in the LTS.

Note that, by Def. 9, a fair trace is also a maximal one (w.r.t. L ). Indeed, if a fair trace is finite, the condition above guarantees that its final state has no L transitions enabled.

Finally, when checking the fairness of a trace, we shall implicitly assume that the labels µ in our LTSs of contracts and processes always distinguish between different occurrences of the same prefix. E.g., a -→-fair trace of A[X | X] where X def = τ.X is not allowed to only perform the τ's of the first X. Technically, labels µ always implicitly carry the syntactic address of the prefix which is being fired, in the spirit of the Enhanced Structured Operational Semantics [START_REF] Degano | Enhanced operational semantics[END_REF].

It is often useful to reason about how a specific session s evolves in a given trace. Technically, α-conversion allows the name s to be renamed at every step, making it hard to trace the identity of names. More concretely, α-conversion is only needed to make delimitations fresh when unfolding recursive processes. Accordingly, w.l.o.g. hereafter we shall often restrict α-conversion by considering stable traces, only, defined below. In this way, we ensure that s represents the same session throughout the whole trace.

Definition 10. A stable -→-trace is a trace ( u 0 )S 0 - → ( u 1 )S 1 - → ( u 2 )S 2 - → • • • in which (1)
all delimitations carry distinct names and variables, (2) delimitations have been brought to the top-level as much as possible (using ≡), and (3) no α-conversion is performed in the trace except when unfolding recursive processes.

Below, we define several notions of contract faithfulness for participants. We start by clarifying when a participant A realizes a contract (inside a session s) within a specific context. This happens when from any reachable system state S 0 , participant A will eventually perform actions to exculpate herself (in s). In this phase, A is protected from interference with other participants. Then, we say A honest in a system if she realizes every contract in that system. When A[P] is honest independently of the system, we simply say that A[P] is honest. In this last case, we rule out those systems carrying stipulated or latent contracts of A outside of A[P]; otherwise the system can trivially make A culpable: e.g., we disallow

A[P] | B[↓ x A says pay | • • •].

Definition 11 (Honesty). We say that:

-A realizes c at s in S iff whenever S = ( u)(s[A says c | B says d] | S ′ ), S - → * S 0 , and (S i ) i is a {A : π}-fair A-solo stable - →-trace then A ˙˙ s S j for some j ≥ 0; -A is honest in S iff

for all c and s, A realizes c at s in S; -A[P] is honest iff for all S with no

A says • • • nor A[• • •], A is honest in A[P] | S.
S - → * (s) A[τ.do x ok + τ.do x no] | B[do y ok] | s[A says ok ⊕ no | B says ok + no] - → (s) A[do x no] | B[do y ok] | s[A says ok ⊕ no | B says ok + no] - → (s) A[0] | B[do y ok] | s[γ]
where γ = A says E | B says ready no. The system is then stuck, because γ is not allowing the [DO] step. By Def. 4 we have A ˙˙ γ, B ˙˙ γ, so A is honest in S while B is not. Actually, B has violated the contract agreed upon, because he is waiting for a positive answer from the store, while in c B he also promised to accept a no. By Def. 11, B is not honest, while we will show in § 5 that A is honest (see Ex. 10).

P A def = tell A (↓ x a . E) . tell A (↓ y b ; E) . do x a . do y b P B def = (z) (tell A (↓ z b . E) . do z b) P C def = (w) (tell A (↓ w ā ; E) . 0)
Even though A might apparently look honest, she is not. Indeed, A cannot fulfill her contract with B, because the do x a is blocked due to the fact that C (dishonestly) does not perform his internal choice. Note that, if we considered honest a participant whose culpability only depends on the culpability of someone else, then a participant could cunningly have one of her contracts violated, so to avoid fulfilling another contract (e.g., to avoid paying one million euros to B, A stipulates a dummy contract "I ship one candy if you pay 1 cent", which is then violated by a colluding participant C).

We now define when a process enables a contract transition, independently from the context. To do that, first we define the set RD s (P) (after "ready do"), which collects all the atoms with an unguarded action do s in P. Definition 12. For all P and all s, we define the set of atoms RD s (P) as: RD s (P) = {a | ∃ u, P ′ , Q, R . P ≡ ( u) (do s a.P ′ + Q | R) and s ∈ u} Next, we check when a contract "unblocks" a set of atoms X : e.g., if X accounts for at least one branch of an internal choice, or for all the branches of an external choice.

Definition 13. For all sets of atoms X and for all c = 0, we say that c unblocks X iff:

∃Y ∈ RS(c).Y ⊆ X ∪ {e} or c = ready a.c ′ ∧ a ∈ X ∪ {e}

Lemma 5. For all P and for all

γ = A says c | B says d, if c unblocks RD s (P) and S = ( u)(A[P] | s[γ] | S ′ ), then either A ˙˙ γ or S A : do s a ----→.
The following theorem is the CO 2 counterpart of Theorem 1. It states that, when a session s is established between two participants A and B, A can always exculpate herself by performing (at most) two actions A : do -. Note that when the contracts used to establish s are compliant, then we deduce the stronger thesis A ˙˙ s S j .

Theorem 3 (Factual exculpation). Let (S i ) i be the following

A-solo stable -→-trace, with S i = ( u i ) A[Q i ] | s[A says c i | B says d i ] | S ′
i , and:

S 0 µ 0 -→ • • • µ i-2 --→ S i-1 A : do s a ----→ S i µ i -→ • • • µ j-2 --→ S j-1 A : do s b ----→ S j µ j -→ • • • where µ h = A : do s -for all h ∈ [i, j -2]. Then, either c j = 0 or A ˙˙ s S j . a ; c ⊕ c ′ a - → → ♯ c a . c + c ′ a - → → ♯ c ready a. c a - → → ♯ c a ; c ⊕ c ′ a -→ → ♯ E a . c + c ′ a - → → ♯ E a i ; c i 0 - → → ♯ 0 ∑ a i . c i 0 - → → ♯ 0 ∑ a i . c i ctx -→ → ♯ ready a n . c n a ; c ctx -→ → ♯ ready a. c c ctx -→ → ♯ c π.P + Q | R π -→ ♯    open(↓ x A says c | P | R) if π = tell A ↓ x c open(P | R)σ otherwise P ctx -→ ♯ ↓ x B says c | P if B = A P ctx -→ ♯ Pσ
open(P) = P ′ where P ≡ ( u i )P ′ and no delimitation of P ′ can be brought to the top level Fig. 4. Abstract LTSs for contracts and processes (σ :

V → N , name A in - → A ♯ is omitted).
The following theorem states the undecidability of honesty. Our proof reduces the halting problem to checking dishonesty.

Theorem 4. The problem of deciding whether a participant A[P]

is dishonest is recursively enumerable, but not recursive.

A criterion for honesty

In this section we devise a sufficient criterion for honesty. Actually, checking honesty is a challenging task: indeed, by Th. 4, it is not even decidable. We will then provide a semantics of contracts and processes, that focusses on the actions performed by a single participant A, while abstracting from those made by the context. Note that our abstract semantics assumes processes without top-level delimitations, in accordance with Def. 10 which lifts such delimitations outside participants. Further, we sometimes perform this lifting explicitly through the open(-) operator. Definition 14. For all participant names A, the abstract LTSs -→ → ♯ and -→ A ♯ on contracts and on processes, respectively, are defined by the rules in Fig. 4, where σ : V → N .

The intuition behind the abstract rules is provided by Lemma 6 and Lemma 7 below, which establish the soundness of the abstractions.

Lemma 6. For all bilateral contracts

γ = A says c | B says d: 1. γ A says a ----→ → A says c ′ | B says d ′ =⇒ c a -→ → ♯ c ′ ∧ (d ctx -→ → ♯ d ′ ∨ d 0 - → → ♯ d ′ ) 2. γ A says a ----→ → A says c ′ | B says d ′ ∧ c ⊲⊳ d =⇒ c a -→ → ♯ c ′ ∧ d ctx -→ → ♯ d ′

Lemma 7. For each (finite or infinite) stable

- →-trace (S i ) i , with S i = ( u i )(A[Q i ] | S ′ i ), there exists a - → ♯ -trace Q 0 µ 0 -→ ♯ Q 1 µ 1 -→ ♯ Q 2 µ 2 -→ ♯ • • • where µ i = π if S i A : π --→ S i+1
, and µ i = ctx otherwise. Moreover, if (S i ) i is fair, then (Q i ) i is {τ, tell }-fair.

In the above lemma, each step of the whole system might be due to either the process Q i or its context. If Q i fires a prefix π, then it changes according to the π -→ ♯ rule in Fig. 4. In particular, that accounts for tell Aadding further latent contracts to Q i , as well as fuse possibly instantiating variables. Newly exposed delimitations are removed using open(-): indeed, they already appear in u i , since the trace is stable.

We now define when a process P "♯-realizes" a contract c in a session s (written P |= s c), without making any assumptions about its context. Intuitively, P |= s c holds when (1) P eventually enables the do s actions mandated by c, and (2) in the abstract LTS -→ ♯ , the continuation of P after firing some do s must realize the continuation of c (under -→ → ♯ ). Note that P is not required to actually perform the relevant do s , because the context might prevent P from doing so. For instance, in the system A[P] | s[A says c | B says ready a.d] the process P can not fire any do s . Definition 15. Given a session s and a participant A, we define the relation |= A s ("♯-realizes") between processes and contracts as the largest relation such that, whenever P 0 |= A s c, then for each {τ, tell }-fair -→ A ♯ -trace (P i ) i without labels do s -, we have: Theorem 5 below establishes an invariant of system transitions. If a participant A[Q 0 ] ♯-realizes a stipulated contract c 0 , then in each evolution of the system the descendant of A[Q 0 ] still ♯-realizes the related descendant of c 0 . The theorem only assumes that c 0 is in a session with a compliant contract, as it is the case after firing a fuse.

1. ∃k. ∀i ≥ k. c unblocks RD s (P i ) 2. ∀i, a, P ′ , c ′ . P i do s a --→ ♯ P ′ ∧ c a - → → ♯ c ′ =⇒ P ′ |= A s c ′ Example 10.
Theorem 5. Let (S i ) i be a stable - →-trace with S i = ( u i )(A[Q i ] | s[A says c i | B says d i ] | S ′ i ) for all i. If c 0 ⊲⊳ d 0 and Q 0 |= A s c 0 , then Q i |= A s c
i for all i. We now define when a participant is ♯-honest. Intuitively, we classify as such a participant A[P] when, for all prefixes tell ↓ x c contained in P, the continuation Q of the prefix ♯-realizes c. We also require that the session variable x cannot be used by any process in parallel with Q, because such processes could potentially compromise the ability of Q to realise c (see Ex. 11).

Definition 16 (♯-honest participant).

A participant A[P] is ♯-honest iff P does not contain ↓ y A says c, and for all linear contexts C (•), x, c, Q, R, and s fresh in P

P = C (tell ↓ x c.Q + R) =⇒ open(Q{ s /x}) |= A s c ∧ C is x-safe where C (•) is x-safe iff ∃C ′ . C (•) = C ′ ((x)•) or C is free from do x -.
Example 11. Substitute Q = fuse x .do x creditCard for fuse x in the process P A from Ex. 4.

Then A[P A ] is not honest, because A cannot complete her contract if the do x within Q is performed. However, the modified A[P A ] violates x-safety, hence it is not ♯-honest.

The following lemma relates ♯-honesty with the abstract semantics of processes. If a ♯-honest process P abstractly fires a tell ↓ x c, then the continuation of P realises c (item 1). Also, ♯-honesty is preserved under abstract transitions (item 2). Lemma 8. For all ♯-honest participants A[P], such that P = open(P):

1. if P tell B ↓ x c ----→ ♯ P ′ , then P ′ { s /x} |= A
s c, for all s fresh in P.

if P-→

♯ P ′ , then A[P ′ ] is ♯-honest.
Our main result states that ♯-honesty suffices to ensure honesty. Note that while honesty, by Def. 11, considers all the (infinite) possible contexts, ♯-honesty does not. Hence, while verifying honesty can be unfeasible in the general case, it can also be ensured by establishing ♯-honesty, which is more amenable to verification. For instance, for finite control processes [START_REF] Dam | On the Decidability of Process Equivalences for the π-calculus[END_REF] it is possible to decide ♯-honesty e.g. through modelchecking. In fact, in these processes parallel composition cannot appear under recursion, hence their behaviour can be represented with finitely many states. Theorem 6. All ♯-honest participants are honest.

Noteworthily, by Theorem 6 we can establish that all the participants named A in Examples 4, 5, and 6 are honest. This is obtained by reasoning as in Example 10. Instead, participant A in Example 7 is honest but not ♯-honest.

Related Work and Conclusions

We have developed a formal model for reasoning about contract-oriented systems. Our approach departs from the common principle that contracts are always respected after they are agreed upon. We represent instead the more realistic situation where promises are not always kept. The process calculus CO 2 [START_REF] Bartoletti | Contracts in distributed systems[END_REF] allows participants to advertise contracts, to establish sessions with other participants with compliant contracts, and to fulfill them (or choose not to). Remarkably, instead of defining an ad-hoc contract model, we have embedded the contract theory of [START_REF] Castagna | A theory of contracts for web services[END_REF] within CO 2 . To do that, we have slightly adapted the contracts of [START_REF] Castagna | A theory of contracts for web services[END_REF] in order to define culpability, and we have specialized CO 2 accordingly at the system-level. The main technical contribution of this paper is a criterion for deciding when a participant is honest, i.e., always respects the advertised contracts in all possible contexts. This is not a trivial task, especially when multiple sessions are needed for realizing a contract (see e.g. Ex. 5 and 6) or when participants want to inspect the state of a contract to decide how to proceed next (see e.g. Ex. 7).

At the best of our knowledge, this is the first paper that addresses the problem of establishing when a participant is honest in a contract-based system populated by dishonest participants. Several papers investigated the use of contracts in concurrent systems; however, they typically focus on coupling processes which statically guarantee conformance to their contracts. This is achieved e.g. by typing [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF][START_REF] Carpineti | A basic contract language for web services[END_REF][START_REF] Castagna | A theory of contracts for web services[END_REF], by contractbased process synthesis [START_REF] Buscemi | Constraints for service contracts[END_REF], or by approaches based on behavioural preorders [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]. As future work, it may also be interesting to study weaker notions of honesty, e.g., by requiring participants to respect contracts in honest contexts, only.

The process calculus CO 2 has been introduced in [START_REF] Bartoletti | Contracts in distributed systems[END_REF] as a generic framework for relating different contract models; the variant in this paper has been obtained by instantiating it with the contracts of [START_REF] Castagna | A theory of contracts for web services[END_REF]. Some primitives, e.g. multiparty fuse, have been consequently simplified. In [START_REF] Bartoletti | Contracts in distributed systems[END_REF], a participant A is honest when A becomes not culpable from a certain execution step; here, we only require that, whenever A is culpable, then she can exculpate herself by performing some actions. This change reflects the fact that bilateral contracts à la [START_REF] Castagna | A theory of contracts for web services[END_REF] can describe endless interactions.

The notion of compliance in [START_REF] Castagna | A theory of contracts for web services[END_REF] is asymmetric. Namely, if c is the client contract and d is the server contract, then c and d are compliant if c always reaches a success state or engages d in an endless interaction. In our model instead compliance is symmetric: the server contract, too, has to agree on when a state is successful. The LTS semantics of unilateral contracts in [START_REF] Castagna | A theory of contracts for web services[END_REF] yields identical synchronization trees for internal and external choice; to differentiate them, one has to consider their ready sets. We instead give semantics to bilateral contracts, and distinguish between choices at the LTS level. Note that we do not allow for unguarded sums, unlike [START_REF] Castagna | A theory of contracts for web services[END_REF]. Were these be allowed, we would have to deal e.g. with a participant A with a contract of the form a ; c 0 ⊕ (b . c 1 + c . c 2 ). According to our intuition A should be culpable, because of the internal choice. If A legitimately chooses not to perform a, to exculpate herself she would have to wait for the other participant to choose (internally) between b and c. Therefore, A can exculpate herself only if the other participant permits her to. By contrast, by restricting to guarded sums our theory enjoys the nice feature that a culpable participant can always exculpate herself by performing some actions, which pass the buck to the other participant (Theorems 1 and 3).

Design-by-contract is transferred in [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] to distributed interactions modelled as (multiparty) asserted global types [START_REF] Honda | Multiparty asynchronous session types[END_REF]. The projection of asserted global types on local ones allows for the automatic generation of monitors whereby incoming messages are checked against the local contract. Such monitors have a "local" view of the computation, i.e. they can detect a violation but cannot, in general, single out the culpable component. In fact, a monitor cannot know if an expected message is not delivered because the partner is violating his contract, or because he is blocked on interactions with other participants. Conversely, in our approach we compose participants in a "bottom-up" fashion: a participant declares its contract independently of the others and then advertises it; the fuse primitive tries then to harmonise contracts by searching for a suitable agreement. Our notion of honesty out culpable components during the computation. An interesting problem would be to investigate how our notion of culpability could be attained within the approach in [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF]. In fact, this seems to be a non trivial problem, even if forbidding communication channels shared among more than two participants.

Contracts are rendered in [START_REF] Buscemi | CC-Pi: A constraint-based language for specifying service level agreements[END_REF][START_REF] Buscemi | Constraints for service contracts[END_REF] as soft constraints (values in a c-semiring) that allow for different levels of agreement between contracts. When matching a client with a service, the constraints are composed. This restricts the possible interactions to those acceptable (if any) to both parties. A technique is proposed in [START_REF] Buscemi | Constraints for service contracts[END_REF] for compiling clients and services so that, after matching, both actually behave according to the mutually acceptable interactions, and reach success without getting stuck. Our framework is focused instead on blaming participants, and on checking when a participant is honest, i.e. always able to avoid blame in all possible contexts. The use of soft constraints in a context where participants can be dishonest seems viable, e.g. by instantiating the abstract contract model of CO 2 with the contracts in [START_REF] Buscemi | Constraints for service contracts[END_REF]. A challenging task would be that of defining culpability in such setting.

Definition 1 .

 1 Unilateral contracts are defined by the following grammar: c, d ::= i∈I a i ; c i ∑ i∈I a i . c i ready a.c rec X. c X where (i) the index set I is finite; (ii) the atoms in {a i } i∈I are pairwise distinct; (iii) the ready prefix may appear at the top-level, only; (iv) recursion is guarded. Let e be a distinguished atom such that e = ē, and with continuation E = rec X. e ; X. We say that c succeeds iff either c = e ; E ⊕ d, or c = e . E + d, or c = ready e. E. We will omit trailing occurrences of E in contracts. Bilateral contracts are terms of the form A says c | B says d, where A = B and at most one occurrence of ready is present.

Fig. 1 .

 1 Fig. 1. Semantics of contracts (symmetric rules for B actions omitted)

  2), where labels µ = A says a model a participant A performing the action a. Definition 2. The relation µ -→ → on bilateral contracts is the smallest relation closed under the rules in Fig.

Example 2 .

 2 we say that the contracts c and d are compliant. Recall from Ex. 1 the contracts c = a ; c 1 ⊕ b ; c 2 and d = ā . d 1 + c . d 2 . We have that RS(c) = {{a}, {b}}, and RS(d) = {{ā, c}}, which do not respect item (1) of Def. 3 (take X = {b} and Y = {ā, c}). Therefore, c and d are not compliant.

Fig. 3 .

 3 Fig. 3. Reduction semantics of CO 2

  do x ticket. ((ask y true. do x commitF) + τ.do x abortF) Y def = do y hotel. ((ask x true. do y commitH) + τ.do y abortH)

Definition 9 .

 9 Given an LTS µ -→, we say that a (finite or infinite) trace η = (P i µ i -→ P i+1 ) i having length |η| ∈ N ∪ {∞} is fair w.r.t. a set of labels L if and only if

Example 8 .

 8 A computation of the store-buyer system S = A[P A ] | B[P B ] from Ex. 4 is:

Example 9 .

 9 Consider the system A[(x, y) (P A | fuse x | fuse y )] | B[P B ] | C[P C ], where:

Intuitively, a move

  of γ is caused by an action performed by one of its components c and d. If c moves, the a -→ → ♯ rules account for its continuation. This might make d commit to one of the branches of a sum, as shown in the ctx -→ → ♯ rules. Further, c can perform an action not supported by d, by using a [*FAIL] rule: accordingly, 0 -→ → ♯ transforms d into 0. The compliance between c and d ensures the absence of such failure moves.

  Recall the online store A from Ex.[START_REF] Bartoletti | A calculus of contracting processes[END_REF]. We show that X{ s /x} |= s c A . First note that transitions in {τ, tell }-fair -→ ♯ -traces without do s from X{ s /x} can only be labelled with ctx. Thus, each P i on such traces has the form X{ s /x} | K i , for some K i . We have RD s(P i ) = RD s (X{ s /x}) = {addToCart, creditCard}.Also, c A unblocks RD s (X{ s /x}) hence condition (1) of Def. 15 holds. For condition (2), if c A creditCard -----→ → ♯ c ′ = accept ⊕ reject and P i do s creditCard -------→ ♯ P ′ = τ.do s accept + τ.do s reject | K i then P ′ |= s c ′ . Actually, all processes on a {τ, tell }-fair -→ ♯ -traces without do s from P ′ have either the form do s accept | K or the form do s reject | K. For the recursive case, c A addToCart -----→ → ♯ c A and P i do s addToCart -------→ ♯ X{ s /x}, hence X{ s /x} |= s c A by coinduction. Note that the case c A e -→ → ♯ did not apply, because P i cannot take -→ ♯ -transitions labelled do s e.

Acknowledgments. This work has been partially supported by the Aut. Region of Sardinia under grants L.R.7/2007 CRP2-120 (Project TESLA) and CRP-17285 (Project TRICS), and by the Leverhulme Trust Programme Award "Tracing Networks".