Mario Bravetti

Gianluigi Zavattaro

Process Calculi as a Tool for Studying Coordination, Contracts and Session Types

Keywords: Coordination Primitives, Behavioural Contracts, Session Types

We recall techniques, mainly based on the theory of process calculi, that we used to prove results in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how such techniques recently contributed to the clarification of aspects that were unclear about session types, in particular, asynchronous session subtyping that was considered decidable since 2009, while it was proved to be undecidable in 2017.

Introduction

Shared dataspaces and the so-called generative communication paradigm [START_REF] Gelernter | Generative communication in linda[END_REF] attracted a lot of attention since the initial years of research about foundations of coordination models and languages. Linda [START_REF] Carriero | The s/net's linda kernel[END_REF], probably the most popular language based on this coordination model, is based on the idea that concurrent processes interact via a shared dataspace, the so-called Tuple Space (TS for short), where the information needed to coordinate the activities are introduced and retrieved. After its insertion in the TS, a datum becomes equally accessible to all processes, but it is bound to none. In this way, the interaction among concurrent processes is decoupled in space and time, principles useful in the development of modular and scalable concurrent and distributed systems.

Concerning foundational studies on Linda-like coordination languages, it appeared immediately clear that techniques borrowed from the tradition of concurrency theory could be naturally applied. At the first two editions of the Coordination conference, two process calculi based on Linda were proposed by De Nicola and Pugliese [START_REF] De Nicola | A process algebra based on LINDA[END_REF] and by Busi, Gorrieri and Zavattaro [START_REF] Busi | Three semantics of the output operation for generative communication[END_REF]. In particular, the latter started a line of research on the expressiveness of Linda-like coordination primitives that exploited, besides process calculi, also Petri nets. For instance, Petri nets were used in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF], to prove that a Linda process calculus with input, output and test-for-absence is not Turing complete if the semantics for output is unordered, i.e., there is an unpredictable delay between the execution of an output and the actual availability of the emitted datum in the TS. It is interesting to recall that, on the other hand, the same calculus is Turing complete if an ordered semantics is considered, i.e. an emitted datum is immediately available in the TS after the corresponding output is executed. Turing completeness was proved by showing an encoding of a Turing powerful formalism, namely Random Access Machines (RAMs), which is a computational model based on registers that can be incremented, decremented and tested for emptiness.

The success of the Linda coordination model was witnessed by the development, at the end of the 90s, of Linda-based middlewares from main ICT vendors like IBM and Sun Microsystem, which proposed T-Spaces and JavaSpaces, respectively. The basic Linda coordination model was extended with primitives for event notification, time-out based data expiration, and transactions. The techniques for evaluating the expressive power of Linda languages had to become more sophisticated to cope with these additional primitives. In particular, Petri nets with transfer and reset arcs [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF] were adopted to cope also with the new coordination mechanisms for event notification [START_REF] Busi | On the expressiveness of event notification in datadriven coordination languages[END_REF] and for temporary data [START_REF] Busi | Temporary data in shared dataspace coordination languages[END_REF].

During the initial years of the new millennium, Service-Oriented Computing (SOC) emerged as an alternative model for developing communication-based distributed systems. In particular, the large diffusion of Web Services called for the development of new languages and techniques for service composition (see e.g. [START_REF] Bravetti | Replicating web services for scalability[END_REF]). In SOC, the coordination model significantly changes w.r.t. Linda: services reciprocally exchange messages sending them directly to the expected receiver, instead of exploiting a shared dataspace.

The idea, at the basis of SOC, is to conceive an ecosystem of services that expose operations that can be combined to realize new applications. To support this idea, it is necessary for the services to be equipped with an interface that, besides describing the offered operations and the format of the exchanged messages, defines the conversation protocols, i.e., the expected flow of invocations of the operations. These interfaces, in particular the specification of the conversation protocol, are also called behavioural contracts.

Process calculi contributed to the development of theories for behavioural contracts. This line of research was initiated by Carpineti, Castagna, Laneve and Padovani [START_REF] Carpineti | A formal account of contracts for web services[END_REF], for the case of client-server composition, and by Bravetti and Zavattaro [START_REF] Bravetti | Contract based multi-party service composition[END_REF], for multiparty service compositions. The latter is particularly significant for the so-called service choreographies, i.e., systems in which there exists no central orchestrator, responsible for invoking all the other services in the system, because services reciprocally interact. Behavioural contract theories focused mainly on the investigation of appropriate notions of correctness for service compositions (i.e., define when a system based on services is free from communication errors) and on the characterization of notions of compatibility between services and behavioural contracts (i.e., define when a service conforms to a given behavioural contract).

For multiparty composition, a fairness based notion of correctness, called compliance, was proposed for the first time in [START_REF] Bravetti | Contract based multi-party service composition[END_REF]: a system is correct if, whatever state can be reached, there exists a continuation of the computation that yields a final state in which all services have successfully completed. Given the notion of compliance, it is possible to define also a natural notion of refinement for behavioural contracts: a refinement is a relation among contracts such that, given a set of compliant contracts C 1 , • • • , C n , each contract C i can be independently replaced by any of its possible refinements C i , and the overall system obtained by composition of C 1 , • • • , C n is still compliant. Contract refinement can then be used to check whether a service conforms with a behavioural contract: it is sufficient to verify if the communication behaviour of the service refines the behavioural contract. This, in fact, implies that such service can be safely used wherever a service is expected with the behaviour specified by the contract.

A negative result in the theory of behavioural contracts is that, in general, the union of two refinement relations is not guaranteed to be itself a refinement. This implies the impossibility to define a maximal notion of refinement. For this reason, most of the effort in the line of research on behavioural contracts initiated in [START_REF] Bravetti | Contract based multi-party service composition[END_REF] has been dedicated to the identification of interesting subclasses of contracts for which the maximal refinement exists. Such classes are: contracts with output persistence [START_REF] Bravetti | Contract based multi-party service composition[END_REF] (i.e. output actions cannot be avoided when a state is entered in which they are ready to be executed), contract refinement preserving strong compliance [START_REF] Bravetti | A theory for strong service compliance[END_REF] (i.e. as soon as an output is ready to be executed, a receiver is guaranteed to be ready to receive it), and asynchronously communicating contracts [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF] (i.e. communication is mediated by fifo buffers). In the first two of these three cases, it has been also possible to provide a sound algorithmic characterization of the corresponding maximal refinements.

To the best of our knowledge, characterizing algorithmically the maximal contract refinement in case of asynchronous communication is still an open problem. The main source of difficulty derives from the fact that, due to the presence of unbounded communication buffers, systems of asynchronously communicating contracts are infinite-state, even if contracts are finite-state. In the light of this difficulty, we tried to take inspiration from work on session types, where asynchronous communication has been investigated since the seminal work by Honda, Yoshida and Carbone [START_REF] Honda | Multiparty asynchronous session types[END_REF] (recipient of the most influential POPL'08 paper award). Session types can be seen as a simplification of contracts obtained by imposing some limitations: there are only two possible choices, internal choice among distinct outputs and external choice among distinct inputs.

The counterpart of contract refinement in the context of session types is subtyping [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]. If we consider asynchronous communication, both contract refinement and session subtyping can admit a refinement/subtype to perform the communication actions in a different order. For instance, given a contract/type that performs an input followed by an output, a refinement/subtype can anticipate the output before the input, because such output can be buffered and actually received afterwards. Asynchronous session subtyping was already studied by Mostrous, Yoshida, and Honda in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], where also an algorithm for checking subtyping was presented. Upon studying this algorithm we noticed an error in its proof of termination: if, while checking subtyping, the buffer grows unboundedly, the proposed procedure does not terminate. Subsequently, Bravetti, Carbone and Zavattaro [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF] and Lange and Yoshida [START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] independently proved that asynchronous session subtyping is actually undecidable. Our experience in the modeling of Turing complete formalism (see the above discussion about encoding RAMs in the Linda process calculus) helped in finding an appropriate Turing powerful model to be encoded in terms of asynchronous session subtyping. In particular, we were able to present a translation from a Queue Machine M (a computational model similar to pushdown automata, but with a queue instead of a stack) to a pair of session types that are in asynchronous subtyping relation if and only if M does not terminate. Then, undecidability of asynchronous session subtyping directly follows from the undecidability of the halting problem for Queue Machines.

These negative results opened the problem of identifying significant classes of session types for which asynchronous subtyping can be decided. Currently, the most interesting fragments have been identified in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] and [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. In the former, an algorithm is presented for the case in which one of the two types is completely deterministic, i.e. all choices -both internal and external-have one branch only. In the latter, we have considered single-out (and single-in) session types, meaning that in both types to be checked all internal choices (resp. external choices) have one branch only. In the design of our algorithm we have been inspired by our expertise in the analysis of the expressiveness of Linda process calculi. In particular, the analysis techniques in Petri nets with transfer and reset arcs (our tools to prove decidability results) are based on the notion of well quasi ordering (wqo): while generating an infinite sequence of elements, it is guaranteed to eventually generate an element that is greater -with respect to the wqo-of an already generated element. Similarly to the procedure in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], our algorithm checks a sequence of judgements, but differently from [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], termination is guaranteed because there exists a wqo on judgements, and the algorithm can terminate when a judgement greater than an already checked one is considered.

Structure of the paper

The remainder of this paper is divided in three parts.

In Section 2 we recall the techniques used to investigate the expressive power of the Linda coordination model: the formalization of Linda-like process calculi, the proof of Turing completeness of the calculi by reduction from Random Access Machines (RAMs), and the identification of fragments that, on the contrary, are not Turing complete. The non Turing completeness results are obtained by proving the decidability of reachability properties; these decidability results are proved by resorting to Well Structured Transition Systems (WSTS).

In Section 3 we recall the main results concerning behavioural contracts: their formalization as process calculi, the notion of correct contract composition, the definition of contract refinement, and its algorithmic characterization. We consider both synchronous and asynchronous communication, excluding the algorithmic characterization which is available only for the synchronous case.

Finally, in Section 4 we move to the analysis of asynchronous communication in the simplified context of session types. In [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] it is stated that subtyping, which is the counterpart of contract refinement, is decidable; recently it has been proved that, on the contrary, it is undecidable. Here, we report the undecidability proof in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF]. Finally, we present the fragment of single-out session types, for which subtyping turns out to be decidable [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. The techniques for these (un)decidability results can be seen as improvements of those developed for Linda process calculi: reduction from more adequate Turing complete computational models (queue machines instead of RAMs), and application of the notion of wqo (at the basis of WSTS) to (a variant of) the subtyping algorithm prposed in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] that, differently from what stated therein, does not terminate in some specific cases.

A Linda process calculus

In this section we present the syntax and the semantics of a calculus for processes that interacts following the Linda coordination model. The calculus is original, even if inspired by calculi such as those presented at the first editions of the Coordination conference [START_REF] De Nicola | A process algebra based on LINDA[END_REF][START_REF] Busi | Three semantics of the output operation for generative communication[END_REF]. The main novelty deals with the management of names which is inspired by the π-calculus [START_REF] Milner | A Calculus of Mobile Processes, I/II[END_REF]: processes can generated new names and pass them to other processes, simply by including such new names inside tuples that are inserted in the shared dataspace. Communication is based on message emission and consumption. The operation out(ã) emits a message consisting of the tuple of names ã. A consumption operation in(η)P is based on a pattern η, which is a sequence of free and bound names: the bound names are those in parentheses (i.e., a is free while (a) is bound). The scope of bound names is the process

P . A pattern η 1 , • • • , η n matches message a 1 , • • • , a n if η i free implies η i = a i .
In this case, we write η[ a j / b j ] j∈J = ã, with J the set of the indexes of bound names in η, and b j such that η j = (b j ) for every j ∈ J. Upon consumption of the tuple ã, the free occurrences of b j in P are replaced by the corresponding a j names (substitution denoted with P [ a j / b j ] j∈J ).

The term 1 denotes the process ready to terminate. The operator (νa)P binds name a in P ; intuitively, the notation (νa) can be seen as the generation of a fresh name that is initially known by P only. The sum construct + is used to make choice between the summands, parallel composition | is used to run parallel programs, while ; executes first the left operand and then the right one. The term P * is used to denote a process that can repeat the execution of P an arbitrary amount of times (possibly zero times). As usual, we admit α conversion of bound names, and we use fn(P ) to denote the set of free names occurring in P .

Example 2.1. As an example of a simple system modeled with our Linda calculus, consider a sensor and a gateway that work in the following way. The sensor periodically wakes up and starts a measuring session; in such a session it measures temperature and the humidity, and communicate them to the gateway. Having no memory, the sensor communicates the measured temperature and the humidity in two separate messages; such messages are inserted in a common dataspace. The gateway reads the measured temperatures and humidities from the dataspace, and combines them in oder to produce pairs of measures taken from the sensor in the same session.

The main problem in this simple system is how to guarantee that the gateway correctly combines temperature and humidity measured in the same session. We assume this problem is solved by enriching the temperature and humidity messages with a session identifier. Following this approach, the behaviour of the sensor can be modeled as follows:

Sensor = (νk)( out(T, t, k); out(H, h, k) ) *
where k is the session identifier which is freshly generated at the beginning of each iteration; T (resp. H) is a constant indicating that the generated tuple contains a measured temperature (resp. humidity); and t and h are the measured temperature and humidity. 1The gateway must combine measures that share the same session identifier. Following this approach, the behaviour of the gateway can be modeled as follows: Gateway = in(T, (x), (s)) in(H, (y), s)( out(x, y) ) * Notice that s is received when the first input of a temperature is executed, and then it is used in the second operation to ensure that the corresponding humidity is consumed from the dataspace. After consumption, a new message that combines the paired temperature/humidity is placed in the dataspace.

The calculus assumes that processes are enriched with a shared dataspace where tuples are stored and consumed.

Definition 2.2 (Systems).

A system is a pair P, S where P is a process and S is a multiset over Message.

We are now ready to define the operational semantics of systems; we first define a labeled transition system on processes which indicates the possible input and output actions, and then we define a transition relation on systems which indicates the effect of process actions execution. Due to the presence of the sequential composition operator P ; Q, we need to explicitly deal with process completion, because Q can start executing only when P completes.

Process completion is denoted by a dedicated transition P √ -→ P . We need an auxiliary process 0 that we use as the target of the termination transition from the process 1, i.e., 1 √ -→ 0. Definition 2.3 (Process semantics). The semantics of processes is defined by a labeled transition system on processes using three kinds of labels α: the actions ãb indicating the emission of the message ã extruding the bound names b, the action η[ a j / b j ] j∈J indicating the consumption of a message ([ a j / b j ] j∈J is the substitution concerning the bound names in η), and the label √ for termination transitions. The transition system is the least one satisfying the axioms and rules in Table 1 (plus the symmetric rules of PAR and SUM), where we use λ to denote labels different from √ , n(α) to denote the names occurring in the label α, and bn(α) to denote the bound names in the label α. Namely, bn(ã b) contains the names in b while bn(α) is empty in all other cases.

Notice that we use two similar notations: η[ a j / b j ] j∈J and P [ a j / b j ]. In the first case, [ a j / b j ] j∈J is to be interpreted as a tuple of pairs of names [ a j / b j ], with b j occurring bound in η and a j denoting the corresponding name expected to be retrieved from the dataspace. In the second case, P [ a j / b j ] is the term obtained by applying the substitutions [ a j / b j ] to P .

The OUT axiom allows for the execution of an output operation; notice the initial label ãε where ε (the empty sequence) indicates that all the names in ã are free. The IN axiom, on the other hand, deals with input operations; the substitution [ a j / b j ] j∈J is guessed, following the so-called early approach, and indicates the names a j that are expected to be present in the consumed message in the positions of the template corresponding with the bound names (b j ). As discussed above, the END axiom deals with the termination transition for the process 1. Rule ENDP states that a parallel process terminates only when both its subprocesses terminates. PAR and SUM are the usual rules for the parallel and choice operators, where the additional condition in PAR checks that if the action α contains bound names, these do not occur free in Q (hence, they cannot be captured). An action can traverse (νa) only if the involved names are different from a (see RES), excluding the case of output actions including a, but in this case the extruded name is added to the tuple of bound names in the label (see OPEN). Rule SEQ1 allows the first process in a sequence to proceed2 , SEQ2 allows the second one to start assuming the first one has completed. The last two rules deal with iterations: rule ITER starts one iteration while axiom ENDI specifies the possibility for iterations to conclude, simply by performing a termination transition. This rule is necessary, for instance, to allow a process P * ; Q to activate Q after an arbitrary amount of executions of process P . Notice that the termination transition of P * , labeled with √ , is always provided by axiom ENDI, so it is not necessary for rule ITER to deal with such transitions.

OUT : out(ã) ãε -→ 1 IN : in(η)P η[ aj / bj ] j∈J -→ P [ a j / b j ] END : 1 √ -→ 0 ENDP : P √ -→ P Q √ -→ Q P |Q √ -→ P |Q PAR : P λ -→ P bn(λ) ∩ fn(Q) = ∅ P |Q λ -→ P |Q SUM : P α -→ P P + Q α -→ P RES : P α -→ P a ∈ n(α) (νa)P α -→ (νa)P OPEN : P ãb -→ P a ∈ ã (νa)P ãb •a -→ P SEQ1 : P λ -→ P bn(λ) ∩ fn(Q) = ∅ P ; Q λ -→ P ; Q SEQ2 : P √ -→ P Q α -→ Q P ; Q α -→ Q ITER : P λ -→ P P * λ -→ P ; P * ENDI : P * √ -→ 0
We can now complete the definition of the operational semantics.

Definition 2.4 (System semantics). The semantics of systems is defined by the minimal transition system satisfying the rules in Table 2.

The transition system → simply allow processes to consume and introduce messages to/from the dataspace; the third rule, on the other hand, allows terminating processes to perform their final √ transition. In case of output action extruding names, it is necessary to check that the bound names are actually fresh in the dataspace. In the following, we use → * to denote the reflexive and transitive closure of →.

Example 2.2. In Example 2.1 we have introduced two processes, Sensor and Gateway. We now consider the following system Sensor |Gateway, ∅ , representing an initial state with an instance of Sensor in parallel with an instance of Gateway, with no message in the dataspace. According to our semantics, we have that the following sequence of transitions are possible:

Sensor | Gateway , ∅ → out(H, h, k); Sensor | Gateway , { T, t, k } → Sensor | Gateway , { T, t, k , H, h, k } → out(H, h, k ); Sensor | Gateway , { T, t, k , H, h, k , T, t, k }
in which the sensor produces its first three messages. Notice that the name k, bound inside Sensor by the binder (k), must be renamed in the second iteration.

In fact, the label T, t, k corresponding to the execution of the action out(T, t, k) which is under the scope of the binder (k), becomes T, t, k k when it traverses such a binder. At the time the third message is produced, the name k is already in the dataspace, hence the premises of the second rule of Table 2 are not satisfied in that k occurs bound in the label and free in the dataspace. By α-converting k in k , the label of the transition becomes T, t, k k , the premises are now satisfied, and the corresponding message can be introduced in the dataspace. Suppose now that, after the above transitions, the Gateway starts consuming the last message that was produced by the Sensor :

out(H, h, k ); Sensor | Gateway , { T, t, k , H, h, k , T, t, k } → out(H, h, k ); Sensor | in(H, (y), k )( out(t, y) ); Gateway , { T, t, k , H, h, k }
Notice that in this last state, the Gateway cannot wrongly consume the message H, h, k as it is willing to access a humidity message with session identifier k , where k was received by consuming T, t, k , and bound to the name s in the definition of Gateway (see Definition 2.1).

As discussed in the Introduction, the aim of this section is to recall techniques that were used to investigate the expressive power of the Linda coordination primitives. More precisely, such techniques were adopted to prove the decidability, or undecidability, of relevant properties for the considered calculi. In order to discuss such techniques, we define two analysis problems for the new Linda calculus presented above.

Informally, we consider the problem of checking whether a given initial system can reach a target state in which the dataspace contains certain messages.

In one case, namely reachability, we are interested in the dataspace to have a precisely predefined content, in the second case, namely coverability, we want the dataspace to contain at least some given messages. Definition 2.5 (Reachability and Coverability problems). Let P, S be an initial system and let T be a multiset over Message containing only names that occur free in the process P or in the dataspace S. We say that P, S reaches T , written P, S ↓ T , if there exists P such that P, S → * P , T (assuming that no name in T is freshly generated during the computation). We say that P, S covers T , written P, S ⇓ T , if there exists P and S such that P, S → * P , T S (assuming that no name in T is freshly generated during the computation).

Typical safety properties can be seen as instances of coverability problems. Consider a system P, S where internal errors are communicated by placing in the dataspace a specific error message error . We have that such system is not safe (i.e. it is not error-free) if and only if P, S ⇓ { error }. Reachability problems, on the other hand, coincide with stronger properties. Consider, for instance, a system in which the generation of the error message is not problematic if there exists also a solution message in the dataspace. The above property P, S ⇓ { error } holds even if the dataspace { error , solution } is reached. This is not the case if we consider the stronger property P, S ↓ { error } that requires the only message error to be present in the reached dataspace.

In the remainder of this section we prove the following decidability and undecidability results of reachability/coverability on fragments of the calculus:

• if we remove the name generation operator (νa)P from the calculus both coverability and reachability are decidable;

• for the full calculus both coverability and reachability are undecidable;

• if we consider a fragment of the calculus (that we call the local fragment) in which received names cannot be used in input actions, but only in outputs, coverability is decidable while reachability is not.

The above three results allow us to formally postulate expressiveness results about the three considered fragments: it is not possible to define a translation from the full calculus to the local fragment that preserves coverability, and it is not possible to define a translation from the local fragment (hence also from the full calculus) to the fragment without name generation that preserves reachability.

Decidability results without name generation

In this subsection we consider processes that do not include name generation (i.e. do not contain the (νa) operator) and we show that in this case we can encode our systems into standard Place/Transition Petri nets. Standard reachability analysis techniques for Petri nets can then be applied to solve both our reachability and coverability problems. This proof technique, i.e., translate a Linda calculus into Petri nets, has been investigated for the first time by Nadia Busi et al. in [START_REF] Busi | On the Turing equivalence of Linda coordination primitives[END_REF].

We start by recalling some preliminaries about Petri nets. A Petri net is a tuple N = (P, T, m 0 ), where P and T are finite sets of places and transitions, respectively. A finite multiset over the set P of places is called a marking, and m 0 is the initial marking. Given a marking m and a place p, we say that the place p contains a number of tokens equal to the number of instances of p in m. A transition t ∈ T is a pair of markings denoted with • t and t • . A transition t can fire in the marking m if • t ⊆ m (where ⊆ is multiset inclusion); upon transition firing the new marking of the net becomes n = (m \ • t) t • (where \ and are the difference and union operators for multisets, respectively). This is written as m → n. We use → * to denote the reflexive and transitive closure of →. We say that m is reachable from m if m → * m . We say that m is coverable from m if m → * m with m ⊆ m . Analysis techniques exist for both reachability [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF] and coverability [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF].

Our encoding of systems into Petri nets is based on the observation that if no names can be freshly generated then the set of processes that can be reached is finite, as well as the possible messages that can be ever produced. This result holds under the assumption that α conversion is not considered, otherwise the number of α convertible processes is clearly infinite. Disallowing α conversion in this fragment is not restrictive; indeed the unique bound names are those that can occur inside input operations, and in this case it is sufficient to assume that they are different from any other free name in the initial process and the initial dataspace to avoid name captures.

We define a Petri net with two kinds of places: places Q corresponding to reachable processes, and places ã corresponding to tuples (with a predefined maximal length) of names occurring in the initial process or in the initial dataspace. The transitions in the Petri net correspond to the execution of actions: they consume one token from a place Q and produces a token in Q if there exists a transition Q α -→ Q , and if α = ã then also a token is produced in the place ã, while if α = η[ aj / bj ] j∈J a token is required to be consumed from the corresponding place ã (such that η[ a j / b j ] j∈J = ã) in order for the transition to be fired.

Formally, we first define the set of derivatives of a process P with initial multiset of messages S. Definition 2.6. Let P be a process without name generation. We denote with Der(P, S) the minimal set of processes including P and closed with respect to the process labeled transition system under the assumption that in a label η[ aj / bj ] j∈J all the names a j occur free in P or in S.

The first result that we prove is that the set of derivatives of a process P , with initial dataspace S, is always finite. Lemma 2.1. Let P be a process without name generation and let S be a multiset of messages. Then the set of its derivatives Der(P, S) is finite.

Proof. First of all, let n be the maximal number of bound parameters in an in operation. Moreover, let d be the number of names occurring free in P or in S. By induction on the structure of P is immediate to see that size(P ), defined as follows, is an upper bound to the cardinality of Der(P, S).

size(1) = 2 size(out(ã)) = 3 size(in(η)P ) = 1 + n × d × size(P ) size(P |Q) = size(P ) × size(Q) size(P * ) = size(P ) + 2 size(P + Q) = size(P ; Q) = 1 + size(P ) + size(Q)
We now define the Petri net encoding and formalise its correctness. Definition 2.7. Let P, S be a system with P without name generation. Let n be the maximal length of tuples of names in P or in S. We define the Petri Net P T ( P, S ) = (Der(P,

S) {ã | len(ã) ≤ n ∧ a i ∈ fn(P ) ∪ n(S)}, T, {P } S)
where n(S) is the set of names occurring in S and T is the following set of transitions:

{t | • t = {Q}, t • = {Q , ã}, Q ã -→ Q } ∪ {t | • t = {Q, ã}, t • = {Q }, Q η[ aj / bj ] j∈J -→ Q , η[ aj / bj ] j∈J = ã} ∪ {t | • t = {Q}, t • = {Q }, Q √ -→ Q }
Note that the Petri net P T ( P, S ) is well defined as its sets of places and transitions are both finite in consequence of Lemma 2.1 Proposition 2.1. Let P, S be a system with P without name generation and let P T ( P, S ) be its corresponding Petri net. We have that P, S → * P , S if and only if the marking {P } S is reachable in P T ( P, S ).

Proof. It is sufficient to proceed by induction on the length of the sequence of transitions in P, S → • • • → P , S .

We can now conclude that both reachability problems are decidable for the fragment without name creation.

Theorem 2.1. Let P, S be a system with P without name generation, and let T be a target multiset of names. Then both P, S ↓ T and P, S ⇓ T are decidable.

Proof. As a consequence of Proposition 2.1 it is sufficient to consider the Petri net P T ( P, S ) and check whether one of the markings {Q} T is reachable (or coverable) for any of the processes Q ∈ Der(P, S). The decidability result follows from the decidability of reachability and coverability in Petri nets.

Undecidability results in the full calculus

We prove the undecidability of reachability and coverability for the full calculus by reduction from the halting problem in Random Access Machines (RAMs). The idea of exploiting RAMs to prove expressiveness results on Linda process calculi traces back to [START_REF] Busi | Three semantics of the output operation for generative communication[END_REF]. A RAM [START_REF] Shepherdson | Computability of recursive functions[END_REF], denoted in the following with R, is a computational model composed of a finite set of registers r 1 , . . . , r n , that can hold arbitrary large natural numbers, and by a program composed by indexed instructions (1 : I 1 ), . . . , (m : I m ), that is a sequence of simple numbered instructions, like arithmetical operations (on the contents of registers) or conditional jumps. An internal state of a RAM is given by (i, c 1 , . . . , c n ) where i is the program counter indicating the next instruction to be executed, and c 1 , . . . , c n are the current contents of the registers r 1 , . . . , r n , respectively.

Without loss of generality, we assume that the registers contain the value 0 at the beginning and at the end of the computation, and that the execution of the program begins with the first instruction (1 : I 1 ). In other words, the initial configuration is (1, 0, . . . , 0). The computation continues by executing the other instructions in sequence, unless a jump instruction is encountered. The execution stops when the instruction Halt is reached. More formally, we indicate by (i, c 1 , . . . , c n ) → R (i , c 1 , . . . , c n ) the fact that the configuration of the RAM R changes from (i, c 1 , . . . , c n ) to (i , c 1 , . . . , c n ) after the execution of the i-th instruction.

In [START_REF] Minsky | Computation: finite and infinite machines[END_REF] it is shown that the following two instructions are sufficient to model every recursive function:

• (i : Succ(r j )): adds 1 to the content of register r j ;

• (i : DecJ(r j , s)): if the contents of register r j is not zero then decreases it by 1 and go to the next instruction, otherwise jumps to instruction s.

We now discuss how to model RAMs in our calculus. The basic idea deals with the representation of the natural numbers in registers: in order to model number c we use a list of concatenated names of corresponding length:

x c , x c-1 , x c-1 , x c-2 , • • • x 1 , x 0 , x 0 .
The entry point of the list for r j is stored inside a message r j , x c . The initial empty lists, one for each register r 1 , . . . , r n , are generated by a bootstrap process

BootStrap = (νx 1 0 ) out(r 1 , x 1 0 ); out(x 1 0 ) ; • • • (νx n 0 ) out(r n , x n 0 ); out(x n 0 ) ; out(p 1 )
that also generates the message p 1 that will trigger the program execution starting from the first instruction.

The program instructions are modeled as follows: an increment simply adds a new pair in front of the list representing the register content, a decrement by removing the initial pair, and a test-for-zero by checking whether the entry point of the list corresponds with the ending tuple x i 0 . More precisely, we model the program instructions as follows:

[[(i :

Succ(r j ))]] = in(p i ); in(r j , (x)) (νy)out(r j , y); out(y, x) ; out(p i+1 ) * [[(i : DecJ(r j , s))]] = in(p i ); in(r j , (x)) in(x)(out(x); out(r j , x)); out(p s ) + in(x, (y))out(r j , y); out(p i+1 ) * [[(i : Halt)]] = in(p i ); in(r1, (x 1 ))in(x 1 ); • • • in(r n , (x n ))in(x n ); out(h)
The i-th instruction is modeled by a process that can repeatedly consume a program counter datum p i , require the execution of a register action (either increment, decrement or test for zero), and finally produce the subsequent program counter p i+1 (or p s in case of jump to the s-th instruction). In case of increment, it simply adds a pair to the list corresponding to the register to increment. In case of decrement or jump instruction, the process checks whether the list is empty or not: in the first case the empty register is re-produced and p s produced, in the second one the first pair of the list is removed and p i+1 produced. A final Halt instruction removes the registers from the encoding and produce the datum h, that will remain the unique message in the dataspace at the end of the computation. In this case, we use the assumption that registers are empty at the end of the computation.

We complete with the full definition of our encoding of a RAM R:

[[R]] = BootStrap | 1≤i≤m [[(i : I i )]]
We can now state the correctness of our encoding.

Theorem 2.2. Let R be a RAM. We have that R terminates if and only if

[[R]], ∅ ⇓ { h }. Moreover, [[R]], ∅ ⇓ { h } if and only if [[R]], ∅ ↓ { h }.
Proof. The encoding proceeds deterministically by reproducing faithfully the corresponding RAM instructions. When a Halt instruction is reached, according with the assumption that the registers will be empty at the end of the computation, we can assume that the register lists will be removed and the tuple h will be produced. Moreover, as the lists have been removed, the tuple h will be the unique datum inside the dataspace.

As a corollary we have the undecidability of both reachability and coverability for our calculus.

The local fragment

In this subsection we identify an intermediary fragment of the calculus for which reachability is undecidable while coverability is decidable. The technique used in undecidability proof is still by encoding RAMs in the calculus, but in this case the encoding in nondeterministic: there are several computations that can be executed by the encoding, but all wrong computations either block before reaching the Halt instruction or leave in the dataspace some "garbage" messages. On the other hand, the decidability proof exploits techniques borrowed from the theory of Well Structured Transition Systems (WSTSs) [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. To the best of our knowledge, one of the first applications of WSTS to calculi based on the notion of shared dataspace, is by Busi and Zavattaro who proved decidability results for the Mobile Ambients calculus [START_REF] Busi | On the expressiveness of movement in pure mobile ambients[END_REF]. Mobile Ambients can be seen as an extension of Linda with multiple nested dataspaces and mobility primitives that can be used to dynamically modify the dataspace nesting topology: one dataspace can enter in a sibling space, one dataspace can exit from an enclosing space, a dataspace can open an enclosed dataspace to acquire its contents.

We first characterize the fragment of the calculus considered in this subsection, then we prove the undecidability of reachability, and then the decidability of coverability, for such fragment.

The idea behind the definition of the fragment is to limit the use of names that are received from the dataspace. When a name is received by means of a bound name in the input pattern, then such name can be used only in output. Formally, given a term in(η)P , for every (b) ∈ η, we impose that b cannot occur free in input operations of P . Under this restriction, we have that even if fresh names can be passed around, these cannot be used to specify new input patterns. We call this the local fragment of the calculus because new names can be used in input patterns only locally, in the initial scope of the name. In the remainder of this section we will consider only processes of the local fragment.

Notice, for instance, that the process Gateway of the Example 2.1 does not belong to the local fragment of the calculus. In fact, it receives a session identifier while reading a temperature message, and then it uses such an identifier in the subsequent input, in order to be sure to consume the corresponding humidity message.

Undecidability of reachability for the local fragment

Also in this case, the proof is by reduction from the halting problem in RAMs.

We start by presenting the encoding of program instructions:

[[(i : Succ(r j ))]] : in(p i ); out(inc j ); in(ack); out(p i+1 ) * [[(i : DecJ(r j , s))]] : in(p i ); out(dec j ); in(ack); out(p i+1 ) + in(p i ); out(zero j ); in(ack); out(p s ) * [[(i : Halt)]] : in(p i ); out(h)
Also in this case, we use a program counter datum p i that triggers the execution of the i-th instruction. Differently, in this case the instructions request the execution of a register action (either increment, decrement or test for zero) to other processes (that we will describe in the following), wait for an acknowledgement about the actual execution of the register action, and finally produce the subsequent program counter p i+1 or p s . Notice that in the case of a DecJ(r j , s) instruction, the process non deterministically selects whether to decrement or test for zero the register r j . In case of a Halt instruction the program counter is not produced thus program execution is terminated (termination is notified also in this case by producing h).

We now consider the modeling of registers:

[[r j ]] : in(nr j ); out(ack); (νu) in(inc j ); out(u); out(ack) * | in(dec j ); in(u); out(ack) * | in(zero j ); out(nr j ) *
Each register r j is activated by a request nr j whose effect is (after generation of the acknowledgement) to generate a private name u used to represent the register contents. Namely, the content c j of the register r j is represented by c j instances of the private datum u. Being private, the messages u do not generate interferences among the encodings of the different registers (i.e. it is not possible to wrongly consider a datum u associated to a register different from the one for which it was generated). An instance of u is produced when an increment request is received, and it is consumed in case of decrement operations. It is worth noticing that it could happen that a decrement request is received when the register is empty. In this case the computation blocks because the in(u) action cannot be executed. Notice also that when a test for zero request is received, a new local name u is generated by emitting nr j whose effect is to reset the register. If a non empty register is reset, instances of the previous private datum u will indefinitely remain in the dataspace.

The full definition of our encoding of a RAM R is as follows:

[[R]] = 1≤i≤m [[(i : I i )]] | 1≤j≤n [[r j ]] | out(nr 1 ); in(ack); • • • ; out(nr n ); in(ack); out(p 1 )
Besides the processes modeling the instructions and the registers we need a bootstrap process that activates the registers and then produces the initial program counter datum p 1 .

We can now conclude by stating the correctness of our encoding.

Theorem 2.3. Let R be a RAM. We have that R terminates if and only if

[[R]], ∅ ↓ {h}.
Proof. We start with the only if part. Assume R terminates. The system [[R]], ∅ can faithfully reproduce the same sequence of increment, decrement and test for zero actions until the Halt instruction is reached. In the finally reached system the dataspace will contain the h datum only, as we have assumed RAMs that starts and ends with all the registers empty. We now consider the if part. Assume that [[R]], ∅ reaches a system in which the dataspace contains only h. The presence of h indicates that the last executed instruction is Halt. The absence of data different from h guarantees not only that the registers are empty at the end of the computation, but also that the sequence of executed register actions is correct. In fact, as observed above, the encoding [[R]] could wrongly simulate DecJ instructions, by deciding to decrement a register when it is empty, or test it for zero when it is not empty. The first kind of error cannot occur because otherwise the computation blocks (hence no datum h could be produced). The second kind of error cannot occur because otherwise some private data u will remain in the dataspace (representing the non empty content of the register at the time a wrong test for zero is executed).

As a corollary, from the undecidability of the halting problem for RAMs, we can conclude the undecidability of reachability for our calculus.

Decidability of coverability for the local fragment

As mentioned above, the proof of decidability of coverability for the local fragment exploits results taken from the theory of WSTS. We now recall the main concepts of WSTS that are useful in our proof.

We start by recalling the notion of well quasi ordering (see, e.g., [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]).

Definition 2.8. A reflexive and transitive relation on a set X is called quasi ordering. A well quasi ordering (wqo) is a quasi ordering (X, ≤) such that, for every infinite sequence x 1 , x 2 , • • • , there exist i < j with x i ≤ x j .

In the following we will use the following well known results for wqo:

• The identity on a finite set is a wqo.

• Consider a finite set S and the set of its multisets M(S). We have that multiset inclusion is a well quasi ordering for the latter, namely (M(S), ⊆) is a wqo, where ⊆ denotes multiset inclusion.

• Consider k well quasi orderings (X 1 , ≤ 1 ), • • • , (X k , ≤ k ). Let Π be the cartesian product X 1 × • • • × X k and ≤ k be the natural extension of the orderings ≤ 1 , • • • , ≤ k to Π, i.e., (x 1 , • • • , x k ) ≤ k (y 1 , • • • , y k ) if and only if x 1 ≤ 1 y 1 , • • • , x k ≤ k y k . We have that (Π, ≤ k ) is a wqo.
We now recall, taking it from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], the notion of compatibility3 of a transition system w.r.t. an ordering. Definition 2.9. A transition system (X, →) is compatible with respect to an ordering (X, ≤) if, given two states s, t ∈ X of the transition system such that s < t and s → s for some s , then there exists t such that s ≤ t and t → t .

In transition systems compatible w.r.t. a wqo, the coverability problem can be solved by applying a backward algorithm; this is possible under the additional assumption that given a state t it is possible to compute its pred basis, i.e., a finite characterization of the possible predecessors of states covering t, that is, those states s such that s → t with t above t (i.e., t ≤ t ). Definition 2.10. Consider a transition system (X, →) and a corresponding ordering (X, ≤). Given t ∈ X and T ⊆ X we define P red(t) = {s|s → t}, P red(T ) = ∪ t∈T P red(t), ↑ t = {t |t ≤ t } and ↑ T = ∪ t∈T ↑ t. A pred basis of state t is a finite set of states T such that ↑ T = ↑ P red(↑ T ).

We now recall the main decidability result for WSTSs that we will use in the following Theorem 2.4 (Theorem 3.6 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]). Let (X, →) be a transition system compatible w.r.t. a wqo (X, ≤) and with effective pred basis (i.e. given a state it is possible to compute its pred basis). Given an initial state s and a target state t, the existence of a computation starting from s and reaching any state t , such that t ≤ t , is decidable.

To exploit this result, we need to define a wqo on systems of our calculus which is compatible for the transition system defining the system semantics. Concerning the dataspaces, which are multisets of messages, one could think of using the above result stating that multiset inclusion, over multisets with a finite domain, is a wqo. Unfortunately, due to the presence of the new name generation operator (νa)P , unboundedly many different messages can be generated, hence the domain of such multisets is not finite. Also for processes, the new name generation mechanism allows for the generation of unboundedly many distinct processes. This difficulty in applying WSTS theory directly on the calculus can be overtaken by introducing an alternative semantics for the local fragment. Such alternative semantics has the following property: the set of used names is finite as well as the set of possible processes.

An alternative semantics for the local fragment

We now define an alternative semantics for the local fragment of our calculus in which the active names are finite. By active, we mean a name which occurs free in input actions. The number of active names turns out to be bound by the initial number of free names plus the number of occurrences of the (νa) operator in the initial process. In fact, when an instance of the (νa) operator inside a cyclic process generates a new name, the name it generated at the previous cycle is no longer active. The alternative semantics that we define, instead of generating always fresh names, re-use the same name considered at the previous cycle. Namely, each time an instance of (νa) requires the generation of a new name, we always use a corresponding name a . When a must be re-generated inside a new cycle, the instances of a left in the dataspace or in other processes are all renamed with a dummy name •, to indicate that they are no longer active. In this way, only active names are faithfully represented while the names that are no-longer active are all represented with the same dummy name •.

This specific discipline in the re-use of names has also another effect: it is no longer necessary to use α-conversion under the assumption that all the names a used by (νa) occurring in the initial process are pairwise distinct and different from the initial free names. Definition 2.11 (Alternative semantics). Let P be a process: without loss of generality we assume that all the names occurring in binders are pairwise distinct and different from the free names in P . Moreover, for each a in a (νa) operator occurring in P , consider a fresh name a . Consider now the labeled transition system for processes α =⇒ defined as the one in Definition 2.3, but without considering α-conversion. The alternative system reduction relation ⇒ is defined as in Definition 2.4 where α =⇒ is used instead of α -→ and the second rule of Table 2 is replaced by the following one:

P ba 1 •••an =⇒ P P, S ⇒ (P [ • / a i ] i=1•••n )[ a i/ a i ] i=1•••n , S[ • / a i ] i=1•••n b[ a i/ a i ] i=1•••n
where the substitutions are used to replace all previous instances of names a i with •, and the fresh instances of a i with a i .

We now formalize the correspondence between the alternative and the standard semantics. We consider two distinct propositions, one showing how standard transitions are mimicked by the alternative semantics, and another one for the vice versa. In these propositions we apply renaming functions to processes and messages in the dataspace: Proposition 2.2. Let P, S be a system with P such that all the names occurring in binders are pairwise distinct and different from the free names in P and from those in S. If P, S → * P , S then there exists a renaming function f such that P, S ⇒ * P [f ], S [f ] with f identity for the free names in the initial configuration P, S and injective on the free names occurring in input actions in P .

P [f ] (resp. S[f ])
Proof. The proof is by induction on the length of the sequence of transitions P, S → * P , S . The base case is trivial. In the inductive case we have P, S → * P , S → P , S with P, S ⇒ * P [f ], S [f ] for some function f identity for the free names in P, S and injective for the free names occurring in input actions in P . We proceed with a case analysis on the transition P α -→ P used to infer the last transition P , S → P , S .

We start from the simplest case: P √ -→ P . The possibility to terminate, i.e., perform a √ transition, is independent from the actually used names because the terminating processes are 1 and P * (and combinations of them).

Hence we simply observe that also

P [f ] √ =⇒ P [f ]. This implies the thesis P [f ], S [f ] ⇒ P [f ], S [f ] . Consider now P η[ aj / bj ] j∈J -→ P .
In this case we have the corresponding tran-

sition P [f ] f (η [ aj / bj ] j∈J ) =⇒ P [f ], from which P [f ], S [f ] ⇒ P [f ], S [
f ] holds because f renames the processes as well as the dataspace. Hence, a message that could be consumed by an input operation before renaming, could be consumed also after application of the renaming. We have that f continue to be the identity for the free names in P, S and injective for the free names occurring in input actions in P . In fact, the names received by the executed input, i.e. {f (b j ) | j ∈ J}, cannot replace parameters of input operations. This follows from the restrictions imposed in the local fragment.

The last case is for P

ãb 1 •••bn -→ P .
In this case we have the corresponding

transition P [f ] f (ã b 1 •••bn ) =⇒ P [f ], from which P [f ], S [f ] ⇒ P [f ], S [f ]
for a renaming f defined as follows. Let a i be the names to which b i is mapped by f (i.e. f (b i ) = a i ). According to the alternative semantics, a i is the name used in the instance (νa i ) occurring in the initial process P which is α-renamed to (νb i ) in P . In the alternative semantics, (νa i ) is not α-renamed, but the corresponding name a i is used instead of b i ; hence the renaming function f must map b i to a i (i.e. f (b i ) = a i ). Moreover, in P [f ], S [f ] , if there are free occurrences of a i , these are renamed to • by the transition

P [f ], S [f ] ⇒ P [f ], S [f ] . Let b i be the corresponding names in P , S (i.e. f (b i ) = a i ); the new renaming function f must map b i to • (i.e. f (b i ) = •).
This new renaming f continue to be injective on names that occur in input actions. This follows from the fact that the names b i which are all mapped to • by f cannot indeed occur in input positions. In fact, these correspond to new names generated by the corresponding operators (νa i ). In the local fragment of the calculus, these names can be used in input actions only inside the scope of the binder (νa i ). But, if this operator generates a new name, this means that it is inside a repetition P * , and the previous execution of the repetition has been already completed. Hence also the scope of the previous (νa i ) instance has been completed.

Similarly, we have that all the sequences of transitions in the alternative semantics, have corresponding computations in the standard semantics. Proposition 2.3. Let P, S be a system with P such that all the names occurring in binders are pairwise distinct and different from the free names in P and from those in S. If P, S ⇒ * P , S then there exists P, S → * Q, T and a renaming f identity for the free names in the initial configuration P, S and injective on the free names occurring in input actions in

Q such that Q[f ] = P and T [f ] = S .
We can finally prove that the alternative semantics preserves the coverability problem for the local fragment.

Theorem 2.5. Let P, S be a system with P such that all the names occurring in bonders are pairwise distinct and different from the free names in P and from those in S. Given T a multiset over Message containing only names that occur free in the process P or in the dataspace S, we have that P, S ⇓ T if and only if P, S ⇒ * P , S with T ⊆ S .

Proof. The only-if part follows from Proposition 2.2. If P, S ⇓ T then there exists a system P , S such that P, S → * P , S with T ⊆ S . By Proposition 2.2 there exists P , S such that P, S ⇒ * P , S with S = S [f ] with f identity for the free names in the initial configuration. Being T composed of only names free in the initial configuration, we have also that T ⊆ S .

The if part follows from Proposition 2.3. Assume P, S ⇒ * P , S with T ⊆ S . By Proposition 2.3 there exists P , S such that P, S → * P , S and a renaming f , identity for the free names in the initial configuration P, S , such that S [f ] = S . Being T composed of only names free in the initial configuration, we have also that T ⊆ S , hence also P, S ⇓ T .

Resorting to the theory of WSTS

We now move to the proof of decidability of coverability for the alternative semantics of the local fragment. The first step is to define a wqo for the alternative transition system: this is now possible because the number of reachable processes is finite, as well as the names used in the dataspace. This finiteness result follows from the re-use, of the predefined names a , when new names are needed.

Proposition 2.4. Let P 0 , S 0 be a system with P 0 such that all the names occurring in binders are pairwise distinct and different from the free names in P 0 and from those in S 0 . Let Der P and Der S be the reachable processes and the reachable dataspaces, i.e., Der P = {P | P 0 , S 0 ⇒ * P, S } and Der S = {S| P 0 , S 0 ⇒ * P, S }. We have that Der P is finite while Der S contains multisets of messages taken from a finite domain.

Proof. We start by showing that Der S contains messages taken from a finite domain. Messages are tuples of names; the length of the tuples in the reachable dataspaces is bound by max , where max is the greatest value between the maximal length of the tuples in the initial dataspace S 0 and the maximal number of parameters in an out operation. Moreoveor, the names occuring in such tuples are taken from the following finite set: fn(P )∪n(S 0 )∪{a | (νa) occurs in P }∪• where n(S 0 ) are the names occurring in S 0 . Obviously, the possible tuples of bound length, containing names taken from a finite set, are finite as well.

Concerning Der P , as in the proof of Lemma 2.1, we prove by induction on the structure of P that a function size a (P ) returns an upper bound to the cardinality of Der P .

size a (1) = 2 size a (out(ã)) = 3 size a (in(η)P ) = 1 + n × d × size a (P )
size a ((νa)P ) = size a (P ) size a (P |Q) = size a (P ) × size a (Q) size a (P * ) = size a (P ) + 2 size a (P + Q) = size a (P ; Q) = 1 + size a (P ) + size a (Q) where, in this case, n is the maximal number of bound parameters in an in operation, and d is the cardinality of the set of possible names fn(P ) ∪ n(S 0 ) ∪ {a | (νa) occurs in P } ∪ • discussed above.

We are now ready to define an ordering on systems which is a wqo when applied to the systems that can be reached from an initial one: P, S ≤ S P , S ⇔ P = P ∧ S ⊆ S Notice that the ordering ≤ S simply combines the identity on processes and multiset inclusion on dataspaces.

Proposition 2.5. Let S 0 = P 0 , S 0 be a system with P 0 such that all the names occurring in binders are pairwise distinct and different from the free names in P 0 and from those in S 0 . Let Sys be the set of systems that are reachable from P 0 , S 0 according to the alternative semantics, i.e., Sys = { P, S | P 0 , S 0 ⇒ * P, S }. We have that (Sys, ≤ S ) is a wqo, and that (Sys, ⇒) is compatible with (Sys, ≤ S ).

Proof. The ordering (Sys, ≤ S ) is a wqo as a direct consequence of Proposition 2.4 and of the three well known results about wqo recalled after Definition 2.8: in fact ≤ S simply combines two orderings, the identity on the reachable processes (that are finite) and multiset inclusion on the reachable dataspaces (that are multisets on a finite domain).

We now consider the compatibility of (Sys, ⇒) w.r.t. the ordering ≤ S . Consider P 1 , S 1 ≤ S P 2 , S 2 and P 1 , S 1 ⇒ P 1 , S 1 . Being P 1 , S 1 ≤ S P 2 , S 2 , we have that P 1 = P 2 and S 1 ⊆ S 2 . It is easy to see that the process transition used to infer P 1 , S 1 ⇒ P 1 , S 1 can be used to infer also P 1 , S 2 ⇒ P 1 , S 2 , with S 1 ⊆ S 2 . Hence, we have that P 1 , S 1 ≤ S P 1 , S 2 .

We are finally ready to prove the decidability of coverability for the local fragment.

Theorem 2.6. Let P, S be a system of the local fragment and let T be a target multiset of messages. Then P, S ⇓ T is decidable.

Proof. It is not restrictive to assume P such that all the names occurring in (νa) operators are pairwise distinct and different from the free names in P 0 and from those in S 0 ; in fact, if this is not the case, it is sufficiente to apply appropriate α-conversions. 4By Theorem 2.5 we have that P, S ⇓ T if and only if P, S ⇒ * P , S with T ⊆ S . We now prove that the latter is decidable by applying the results for WSTS to the transition system (Sys, ⇒) defined as in Proposition 2.5, i.e., Sys = { P , S | P, S ⇒ * P , S }.

By Proposition 2.5 we know that (Sys, ≤ S ) is a wqo, and that (Sys, ⇒) is compatible with (Sys, ≤ S ). We now show that it is possible to algorithmically decide whether P, S ⇒ * P , S with T ⊆ S , by resorting to the decidability result of WSTS recalled in Theorem 2.4. By Proposition 2.4, we have that the possible processes P in Sys are finite; let Der P be such finite set of processes. Moreover, T ⊆ S implies that, for every P , P , T ≤ S P , S . Hence, our problem consists of checking, if there exists at least one P , taken from the finite set Der P , such that P, S ⇒ * P , S with P , T ≤ S P , S . By Theorem 2.4 we have that the latter is decidable under the assumption that it is possible to compute the so-called pred basis for each state of the transition system (Sys, ⇒). We complete the proof by showing that this actually holds.

Let Q, U ∈ Sys; we now show how to compute its corresponding pred basis First of all let Q = {Q ∈ Der P |Q α =⇒ Q}: this set is finite (and computable) as Der P is finite. For each process Q ∈ Q, depending on the kind of process transition Q α =⇒ Q, we add a predecessor system Q , U Q to the pred basis. There are three kinds of transition: those corresponding to an input (i.e., Q

η[ aj / bj ] j∈J =⇒ Q), to an output (i.e., Q ba 1 •••an =⇒ Q),
=⇒ Q).
In the first case, the input action consumes from the dataspace the tuple ã = η[ a j / b j ] j∈J ; in this case we consider the predecessor system Q , U {ã} . In the second case, the emitted message is b; in this case we consider the predecessor system Q , U \ { b} . In the third case, we have that the process transition does not modify the dataspace, hence we consider the predecessor system Q , U . The set containing all such predecessors (computable because finite) is a pred basis for Q, U .

Behavioural Contracts

Behavioural contracts are used to describe the message-passing behaviour of services. The adoption of process calculi for the specification and analysis of behavioural contracts was initiated by Fournet et al. [START_REF] Fournet | Stuck-free conformance[END_REF], who proposed to specify contracts with a calculus inspired by CCS [START_REF] Milner | Communication and concurrency[END_REF]. They also defined a notion of conformance between processes and contracts following a substitution principle: a process conforms to a contract if it can replace it in any context without adding additional stuck behaviour. Contract have been subsequently studied in the context of service oriented computing: contracts for client-service interaction have been proposed by Carpineti et al. [START_REF] Carpineti | A formal account of contracts for web services[END_REF] and then independently extended along different directions by, e.g., Bravetti and Zavattaro (see e.g. [START_REF] Bravetti | Contract based multi-party service composition[END_REF][START_REF] Bravetti | A theory for strong service compliance[END_REF][START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]) by Laneve and Padovani [START_REF] Laneve | The Must preorder revisited[END_REF], by Castagna et al. [START_REF] Castagna | A theory of contracts for web services[END_REF], and Barbanera and de'Liguoro [START_REF] Barbanera | Two notions of sub-behaviour for sessionbased client/server systems[END_REF].

All such theories of contracts introduce, under different assumptions, notions of contract refinements that can be seen as generalizations of the notion of conformance initially studied in [START_REF] Fournet | Stuck-free conformance[END_REF]: a contract refines another one if it can safely replace it in any possible context. To give to the reader an idea of such techniques, here we report the contract theory discussed in [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Bravetti | A Foundational Theory of Contracts for Multiparty Service Composition[END_REF], for synchronous communication, and [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF], for the asynchronous case. In particular, the latter represents the unique contract theory, to the best of our knowledge, specifically tailored to asynchronous communication.

More precisely, the contract theory that we present is based on the following ingredients: the notion of correct contract composition, the definition of contract refinement, and its algorithmic characterization. The theory considers both synchronous and asynchronous communication, excluding the algorithmic characterization which is available only for the synchronous case.

The Service Calculus

We start by presenting the formal definition of services following the approach of [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Bravetti | A Foundational Theory of Contracts for Multiparty Service Composition[END_REF]. Services are assumed to reside at a certain location over the network. They are denoted by representing service behaviour with essentially the same syntax as the Linda calculus of the previous Section 2, but considering channel based (instead of tuple based) communication actions/operations as in the context of Service Oriented Computing. We assume a denumerable set of action names N , ranged over by a, b, c, . . . and a denumerable set Loc of location names, ranged over by l, l , l 1 , • • • . We use τ / ∈ N to denote an internal (unsynchronizable) service computation. Moreover, we use a and a l , with a ∈ N , to denote service input and output messages, respectively, where a destination location (identifying the service to which the message is sent) is specified for outputs. Finally, we represent inner service communication, modeling, e.g., internal process message exchange: we use a * and a * , with a ∈ N , to denote internal service input and output messages, where processes executing a * and a * must synchronize in order to proceed (as in CCS [START_REF] Milner | Communication and concurrency[END_REF] synchronization). In the process algebra we use, as for the Linda calculus of Section 2: the choice + , parallel | , sequential ; , and repetition * operators and "1" denoting (successful) termination. 5 Notice that a term S represents the behavior of a single service: the parallel | operator is used to represent its internal processes. Subsequently we will introduce systems, where communication among several services (residing at different locations over the network) is modeled, considering both the case of synchronous and asynchronous communication.

The operational semantics of services is defined in terms of a transition system labeled over {a, a l , a * , a * , τ, √ | a ∈ N , l ∈ Loc}, ranged over by λ, λ , . . . , obtained by the rules in Table 3 (plus symmetric rules). As in the previous section, in the operational semantics we use an auxiliary process "0" as the target of the termination transitions √ . Semantic rules are the standard ones: choice + , parallel | , sequential ; , and repetition * operators and "1"

1 √ -→ 0 α α -→ 1 S 1 λ -→ S 1 S 1 +S 2 λ -→ S 1 S 1 λ -→ S 1 λ = √ S 1 ;S 2 λ -→ S 1 ;S 2 S 1 √ -→ 0 S 2 λ -→ S 2 S 1 ;S 2 λ -→ S 2 S 1 a * -→ S 1 S 2 a * -→ S 2 S 1 |S 2 τ -→ S 1 |S 2 S 1 √ -→ 0 S 2 √ -→ 0 S 1 |S 2 √ -→ 0 S 1 λ -→ S 1 λ = √ S 1 |S 2 λ -→ S 1 |S 2 S * 1 √ -→ 0 S 1 λ -→ S 1 λ = √ S * 1 λ -→ S 1 ; S * 1
Table 3: Semantic rules for services (symmetric rules omitted).

are dealt with as for the Linda calculus of Section 2. In particular a * and a * synchronize over parallel as for CCS [START_REF] Milner | Communication and concurrency[END_REF]. Given a (possibly empty) sequence of labels

w = λ 1 λ 2 • • • λ n-1 λ n , we use S w -→ S to denote a sequence of transitions S λ1 -→ S 1 λ2 -→ • • • λn-1 -→ S n-1 λn -→ S (in case of w = ε we have S = S, i.e., S ε -→ S).
As in [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Bravetti | A Foundational Theory of Contracts for Multiparty Service Composition[END_REF], the semantics of a service S yields a finite-state labeled transition system whose states are terms S reachable from S, i.e. ∃w : S w -→ S .

Example 3.1. (Authentication Server)

We now present a simple example of an authentication server that repeatedly performs two kinds of task: (i) the authentication of clients by receiving their username and password, and (ii) the request to an external account service for update of the list of the registered users.

( username; password; (accepted client + f ailed client ) + updateAccounts accountServer ; newAccounts ) *

The service indicates a repeated choice between the two possible tasks. The first task is activated by the reception of an invocation on username. In this case, a password should subsequently be received and then two possible answers are sent back to the client: either accepted or failed . The second task is activated by sending a request for update to the accountServer. In this case, the newAccounts are subsequently received. parallel requests: to airplane and hotel reservation services. Then it spawns two internal processes that wait in parallel for the replies of each of the two reservation services. The first process, that waits for the reply of the airplain reservation service, internally communicates to the other process, using local names okF light * and koF light * , whether a satisfactory flight is available: the okF light * message is sent if a list of available fights is received and one of them is deemed to be satisfactory (based, e.g., on times/prices), otherwise koF light * is used to explicitely communicate that no satisfactory flight has been found. The second process, that waits for the reply of the hotel reservation service, keeps actively querying such a service (e.g. trying with different hotels/nearby locations) until an available room is found; then it replies to the initial client's reservation request: based on the local message received from the other process either sends a travel plan or provides a negative answer.

Contract-based Service Discovery

We now define the notion of behavioural contract, as it appears in [START_REF] Boreale | Advanced mechanisms for service composition, query and discovery, in: Rigorous Software Engineering for Service-Oriented Systems -Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing[END_REF], which will allow us to reason about service compliance and retrieval independently of the language used for implementing service behaviour.

Contracts are defined as labeled transition systems, representing the communicating behavior of a service, standing at a certain location over the network, with respect to its environment (the other services). Thus, formally, as actions in their transition labels we just use τ for internal computations/synchronizations and a and a l for inputs/outputs (where the outputs, as for the service calculus, are directed to a destination location l ∈ Loc). We first define the class of labeled transition systems of interest for defining contracts.

Definition 3.2. (Finite Connected LTS with Termination Transitions)

A finite connected labeled transition system (LTS) with termination transitions is a tuple T = (S, L, -→, s h , s 0 ) where S is a finite set of states, L is a set of labels, the transition relation -→ is a finite subset of (S -{s h }) × (L ∪ { √ }) × S such that (s, √ , s ) ∈-→ implies s = s h , s h represents a halt state, s 0 ∈ S represents the initial state, and it holds that every state in S is reachable (according to -→) from s 0 .

As in the semantics of services, in a finite connected LTS with termination transitions we use √ transitions (leading to the halt state s h ) to represent successful termination. On the contrary, if we get (via a transition different from

√

) into a state with no outgoing transitions (like, e.g., s h ) then we intend to represent an internal failure or a deadlock. Definition 3.3. (Behavioural Contracts) A behavioural contract is a finite connected LTS with termination transitions, that is a tuple T = (S, L, -→, s h , s 0 ), where L = {a, a l , τ | a ∈ N ∧ l ∈ Loc}.

Services S give rise to a behavioral contract as the labeled transition system obtained by their semantics, where a * and a * labeled transitions (representing potential internal communications that did not actually take place) are disregarded. More precisely, the obtained behavioural contract is (S, L, -→, s h , s 0 ) where: the initial state s 0 is S, the halt state s h is 0, the set of states S includes, besides 0, the terms S such that ∃w : S w -→ S ∧ a * , a * / ∈ w (i.e., both a * and a * do not belong to the label sequence w) and the transition relation -→ is the set of trasitions S λ -→ S such that S , S ∈ S and λ / ∈ {a * , a * }.

Behavioural Contracts as Terms

We now introduce a process algebraic representation for behavioural contracts by using basic CCS [START_REF] Milner | A complete axiomatisation for observational congruence of finite-state behaviors[END_REF] over L prefixes extended with successful termination "1", whereas the traditional null process "0" is the halt state and denotes a failure or a deadlock, if not reached by a √ transition (see the discussion above about the halt state). Representing contracts as terms will be useful when developing their theory.

C ::= 0 | 1 | α.C | C +C | X | recX.C α ::= τ | a | a l
where recX. is a binder for the process variable X denoting recursive definition of processes. We assume that in a contract C all process variables are bound.

In the following we will omit trailing " .1" when writing contracts. 6Notice that, even if we represent contract LTSes as terms, we preserve their language independent nature (they are just a syntactical representation of LTSes).

The operational semantics of contracts C is defined in terms of a transition system labeled over {a, a l , τ, √ | a ∈ N , l ∈ Loc}, ranged over by λ, λ , . . . , obtained by the rules in Table 5 (plus a symmetric rule for choice). We use the notation C{ / } to denote syntactic replacement. Semantic rules are the standard ones, apart from that of term 1, which performs a √ transition denoting successful termination. We use C w -→ C to denote a sequence of transitions from C to C labeled according to the label sequence w (formally the definition is the same as for service terms S).

1 √ -→ 0 α.C α -→ C C λ -→ C C +D λ -→ C C{recX.C/X} λ -→ C recX.C λ -→ C
The semantics of a behavioural contract term C gives rise to a finite7 connected LTS with termination transitions (S, L, -→, 0, C), i.e. indeed a contract according to Definition 3.3, where S includes, besides 0, the set of states C reachable from C, i.e. such that ∃w : C w -→ C , and -→ includes only transitions between states of S. In [START_REF] Bravetti | Contract-based discovery and composition of web services[END_REF] we formalize the correspondence between contracts T = (S, L, -→, s h , s 0 ) and their representation as terms C by showing how to obtain from a contract T a corresponding C with the same behaviour.

Example 3.3. (Authentication Server Contract)

We now present the contract for authentication service that we introduced in Example 3.1. In this simple case the contract is very similar to the service description itself: recX.( username.password.(accepted client .X + f ailed client .X) + updateAccounts accountServer .newAccounts.X + 1 )

We just have that sequencing ";" is turned into prefix ".", that repetition via " * " is expressed by using recursion "recX" and that "1" is used to represent successful termination.

Example 3.4. (Travel Agency Contract)

We also present, in Table 6, the contract for the travel agency service presented in Example 3.2 (see Table 4). This example shows how contracts are just a syntactical representation of LTSes and abstract from the service language; in particular from the internal structure (e.g. internal processes) and internal communications of services: what in the service was internally communicated via okF light * and koF light * messages is now simply seen as a τ prefix. Notice that in Table 6, for clarity of presentation, parts of the the contract for the travel agency service have been separately defined, i.e. contracts: C X , representing the status of the service after that the two initial concurrent requests have been sent; C Y , representing the status after that an "AvailF lights" message has been received, but no room as been found yet; and C Z , representing the status after that a "N oF lights" message has been received, but no room has been found yet.

In order to show how a contract with 0 (representing failure or deadlock) is generated, we consider a variant of the travel agency service presented in Table 4, where we take (okF light * ; T ravelP lan client + koF light * ; N oAvail client ) to be replaced by okF light * ; T ravelP lan client that is the service programmer "forgot" to consider the case in which the koF light * message is internally transmitted. In this case, whenever a "N oF lights" message is received, the subsequent internal koF light * communication cannot be completed and a deadlock is originated. The obtained contract is as that shown in Table 6, but for the two occurrences of (τ.T ravelP lan client + τ.N oAvail client )

being replaced by τ.T ravelP lan client and the two occurrences of "τ.N oAvail client " being replaced by " 0". The obtained contract, thus, shows that a deadlock is reached whenever the "N oF lights" message is received (from the flight reservation service).

Output persistence property

In the following we will study independent contract refinement. As already anticipated in the Introduction under synchronous communication a maximal independent contract refinement that preserves compliance does not exist. In [START_REF] Bravetti | Contract based multi-party service composition[END_REF] we showed that this is a consequence of the symmetry between input and output actions and that a possible solution, for synchronous communication, is to resort to output persistent contracts; thus breaking such a symmetry. The output persistence property states that once a contract decides to execute an output, its actual execution is mandatory in order to successfully complete the execution of the contract. This property typically holds in languages for the description of service orchestrations (see e.g. WS-BPEL [START_REF]Web Services Business Process Execution Language Version 2.0 OASIS Standard[END_REF]) in which output actions cannot be used as guards in external choices (see e.g. the pick operator of WS-BPEL which is an external choice guarded on input actions).

Example 3.5. It is easy to see that, while the travel agency contract of Example 3.4 is output persistent, the authentication server contract of Example 3.3 is not. However, the following modified version of the latter can be considered, to be used in a synchronous setting: recX.( username.password.(τ.accepted client .X + τ.f ailed client .X) + τ.updateAccounts accountServer .newAccounts.X + 1 )

Notice that, in this new version of the authentication server, we have simply added an internal action τ in front of outputs occurring in choices. This guarantees that, at the moment the choice is to be resolved, the output action is not yet ready to be executed: it becomes available only after the τ and, then, its eventual execution is mandatory. As a consequence we have that the output persistence property is satisfied.

As observed in [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF], a syntactical condition on the service calculus of Definition 3.1, which guarantees that output persistent contracts are always obtained, is: each output "a l " must always occur in sequence with a preceding "τ ", i.e. syntactically occur as "τ ; a l ". For instance, if in the service of Example 3.1 we replace each output "a l " with "τ ; a l " we obtain the output persistent contract presented in the Example 3.5 above. 8In the remainder, when we consider synchronous communication, we will restrict to output persistent contracts.

Synchronous Contract Composition

Synchronous systems are formed by the parallel composition of contracts. Definition 3.6 (Synchronous Systems). The syntax of synchronous systems is defined by the following grammar

P ::= [C] l | P ||P
We assume systems to be such that: (i) every contract subterm [C] l occurs in P at a different location l and (ii) no output action with destination l is syntactically included inside a contract subterm occurring in P at the same location l, i.e. actions a l cannot occur inside a subterm [C] l of P .

A contract located at location l is denoted with [C] l . Located contracts can be combined in parallel with the operator P ||P .

Example 3.6. We consider a synchronous system in which we combine the output persistent contract for the authentication server presented in Example 3.5, here denoted with C AuthServer and located at "authServer" location, with a "client" contract and an "accountServer" contract, which interact, respectively, with the two tasks of the authentication server:

[C AuthServer ] authServer || [username authServer .password authServer .(accepted + f ailed)] client || [updateAccounts.newAccounts authServer ] accountServer
System operational semantics is defined by the rules in Table 7 plus symmetric rules. Transition system labels, still ranged over by λ, λ , • • • , are now taken from the set {a sr , a sr , τ, √ | a ∈ N ; s, r ∈ Loc}, where: a sr (a sr , resp.) denotes a potential output (input, resp.) with the sender being at location s and the receiver at location r, τ denotes a synchronization or a move performed internally by one contract in the system and √ denotes successful termination.

C ar -→ C [C] s asr -→ [C ] s C a -→ C [C] r asr -→ [C ] r C λ -→ C [C] l λ -→ [C ] l λ ∈ {τ, √ } P λ -→ P P ||Q λ -→ P ||Q λ = √ P asr -→ P Q asr -→ Q P ||Q τ -→ P ||Q P √ -→ P Q √ -→ Q P ||Q √ -→ P ||Q

Asynchronous Contract Composition

In asynchronous systems contracts are equipped with an input message queue. Definition 3.7 (Asynchronous Systems). The syntax of asynchronous systems is defined by the following grammar

P ::= [C, Q] l | P ||P Q ::= | a l :: Q
We assume asynchronous systems to be such that: (i) and (ii) of Definition 3.6 (with

[C, Q] l replacing [C] l ) hold true.
Terms Q denote message queues. They are sequences of messages, each one denoted with a l where a is the action name and l is the location of the sender. We use " " to denote the empty message queue. Trailing are usually left implicit, and we use "::" also as an operator over the syntax: if Q and Q are -terminated queues, according to the syntax above, then Q :: Q means appending the two queues into a single -terminated list. Therefore, if Q is a queue, then :: Q, Q :: , and Q are syntactically equal. In the following, when we talk about asynchronous contract systems, we will use the shorthand [C] l to stand for [C, ] l .

Example 3.7. We consider an asynchronous system in which we combine the contract for the travel agency defined in Table 6, here denoted with C T ravelAgency and located at "travelAgency" location, with a "client" contract, an airplane reservation contract "airRes" and an hotel reservation contract "hotelRes":

.X) + 1)] hotelRes C ar -→ C [C, Q] s asr -→ [C , Q] s [C, Q] r asr -→ [C, Q :: a s ] r C √ -→ C [C, ] l √ -→ [C , ] l C τ -→ C [C, Q] s τ -→ [C , Q] s C a -→ C b l ∈ Q ⇒ b = a [C, Q :: a s :: Q ] r τ -→ [C , Q :: Q ] r
Table 8: Asynchronous system semantics (rules for parallel omitted).

Asynchronous system operational semantics is defined by the rules in Table 8 plus the rules for the parallel operator of Table 7. In Table 8 we assume that b l ∈ Q holds true if and only if b l syntactically occurs inside Q. This notation is used in the premise of the novel τ synchronization rule that represents the consumption of an a message from the queue by removal of the oldest a one.

As an example consider the system: [a s .b s ] r || [b.a] s . After executing the two outputs, the system evolves to [START_REF] Gelernter | Generative communication in linda[END_REF] r || [b.a, a r :: b r ] s . The receiver is now ready to consume the two messages stored in the queue, thus reaching [START_REF] Gelernter | Generative communication in linda[END_REF] r || [START_REF] Gelernter | Generative communication in linda[END_REF] s . Notice that the two messages are consumed in the opposite order of reception.

This means that the information about the sender attached to queue messages is actually not used by the operational semantic rules in Table 8: even if omitted we would have obtained the same transitions. Nevertheless, we decided to use the same queue syntax as in [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF] to be more adherent to reality, where messages can be distinguished e.g. depending on the sender. As a matter of fact, in [START_REF] Bravetti | Contract compliance and choreography conformance in the presence of message queues[END_REF], this information is used to produce, instead of τ actions, more informative labels that include denotation of the sender-receiver (this makes it possible to establish conformance w.r.t. a given choreographical specification).

Contract Refinement

We now recall the formal definition of independent contract refinement that preserves correct composition of contracts in both the synchronous and asynchronous cases. With P τ -→ * P we denote the existence of a (possibly empty) sequence of τ -labeled transitions starting from the system P and leading to P . Intuitively, a system composed of contracts is correct if any possible computation may guarantee completion, i.e. it can be extended to reach a successfully terminated computation (in the asynchronous case this means that all queues are empty). In this case, such contracts are called compliant. An example of contract composition that is correct (both in the synchronous and asynchronous

case) is [a l3 ] l1 || [b l3 ] l2 || [a.b] l3 . Another example is [a s .b s ] r || [b.a] s
considered above, which is correct in the asychronous case only.

Example 3.8. As larger examples, consider the sychronous and asychronous systems of Examples 3.6 and 3.7. While the latter is a correct contract composition, the former is surely not correct because the contract of the authServer can internally decide to invoke the update task twice, while the contract of the accountServer is able to reply only once. This problem is solved if we, instead, consider an accountServer with the following recursive contract: recX.(updateAccounts.newAccounts authServer .X + 1)

After replacement of the accountServer contract with the one above, it is easy to see that the contract composition turns out to be correct: the system can always successfully complete after having performed (in every possible order) one authentication task and an arbitrary number of update tasks. A version in which also the authentication task can be performed arbitrarily many times can be obtained by considering a client with the following contract: recX.(username authServer .password authServer .(accepted.X + f ailed.X) + 1)

Notice that the discussion above is valid also under asychronous communication.

We are now ready to define the notion of contract refinement. Given a contract C, we use oloc(C) to denote the set of locations used as destinations in all the output actions occurring inside C. Definition 3.9 (Independent Refinement). A pre-order ≤ over contracts is an independent refinement if, for any n ≥ 1, contracts C 1 , . . . , C n and C 1 , . . . , C n such that ∀i. C i ≤ C i , and distinguished location names l 1 , . . . , l n ∈ Loc such that ∀i. oloc(C i ) ∪ oloc(C i ) ⊆ {l j | 1 ≤ j ≤ n ∧ j = i}, we have:

([C 1 ] l1 || . . . || [C n ] ln ) ↓ ⇒ ([C 1 ] l1 || . . . || [C n ] ln ) ↓
An independent refinement pre-order formalizes the possibility to replace in a correct contract composition every contract with one of its refinements, with the guarantee that the new system is still correct. In [START_REF] Bravetti | Contract based multi-party service composition[END_REF] it is shown that in the synchronous case, in the absence of the output persistence assumption, it could happen that given two independent refinement pre-orders, their union is no longer an independent refinement pre-order. In other words, there exists no maximal independent refinement pre-order.

On the contrary, if we restrict to output persistent contracts or we consider asynchronous communication, we have that the maximal independent refinement pre-order exists: it can be achieved by considering a coarser form of refinement in which, given any system composed of a set of contracts, refinement is applied to one contract only (thus leaving the others unchanged). This form of refinement, that we call compliance testing [START_REF] Bravetti | Choreographies and behavioural contracts on the way to dynamic updates[END_REF], is a form of testing where both the test and the system under test must reach success. Given a system P , we use loc(P ) to denote the subset of Loc of the locations of contracts syntactically occurring inside P . Definition 3.10 (Refinement Relation). A contract C is a refinement of a contract C denoted C C, if and only if for all l ∈ Loc and system P such that l / ∈ loc(P ) and l / ∈ oloc(C) ∪ oloc(C ) ⊆ loc(P ), we have:

([C] l ||P ) ↓ ⇒ ([C ] l ||P ) ↓
In the following, whenever C C we will also say that C is a subcontract of C (or equivalently that C is a supercontract of C ).

Theorem 3.1 (Maximal Independent Refinement). There exists a maximal independent refinement ≤ pre-order and it corresponds to the (compliance testing based) refinement relation " ".

Properties of Contract Refinement

We now discuss some properties of contract refinement and also show a sound characterization that is decidable for the synchronous case. We use I(C) (O(C), resp.) to stand for the set of names a (located names a l , resp.) of input actions a (output actions a l , resp.) syntactically occurring in C. Given N ⊆ {a l | a ∈ N ∧ l ∈ Loc}, we assume N to stand for {a l | a l ∈ N }.

We first observe that the refinement relation allows input on new names (and unreachable outputs on new names) to be added in refined contracts.

C {0/α.C | α ∈ I(C ) -I(C)} ≺ C ⇔ C ≺ C C {T /α.C | α ∈ O(C ) -O(C)} ≺ C ⇔ C ≺ C
where T is: 0 in the synchronous case, τ.0 in the asynchronous case.

This theorem is a direct consequence of queue based communication (in the asynchronous case) and output persistence (in the synchronous case): concerning its second statement, it follows from the fact that a subcontract C cannot have reachable outputs that were not included in the potential outputs of the supercontract C; concerning its first statement, it follows from similarly observing that a compliant test P of a contract [C] l cannot have reachable outputs directed to l that C cannot receive (e.g. in the asynchronous case [a] l ||[a l + b l ] l is not a correct contract composition). From the first statement of this theorem we can derive a fundamental property of the maximal independent refinement pre-order, which holds both in synchronous and asynchronous cases: external choices on inputs can be extended, e.g. a + b a. Concerning outputs, we instead have that a l a l + b l in the asynchronous case only and τ.a l τ.a l + τ.b l in both synchronous and asynchronous cases, i.e. internal choices on outputs can be reduced. This because the lefthand term is more deterministic (typical property in testing).

Example 3.9. As a larger example, consider the contract C T ravelAgency in Table 6 We now focus on determining an algorithmic sound characterization of the synchronous contract refinement relation. This is achieved by resorting to the theory of fair testing, called should-testing [START_REF] Rensink | Fair testing[END_REF].

Should-testing is a fair variant of must testing [START_REF] De Nicola | Testing equivalences for processes[END_REF] where successful tests are defined as follows: process B passes test t iff every finite execution of B||t (the process subjected to the test, where " || " denotes parallel execution of two processes, synchronized on all observable actions) has passed through or can be extended to pass through a successful state of t.

As a side result we also have that the refinement relation is coarser than fair testing preorder. We denote with test the should-testing pre-order defined in [START_REF] Rensink | Fair testing[END_REF] where we consider √ to be included in the set of actions of terms under testing as any other action ( √ is treated as a normal action and not as the special action representing success of tests in [START_REF] Rensink | Fair testing[END_REF]). In order to resort to the theory should-testing, we define a normal form for contracts C, denoted with N F(C), that corresponds to terms of the language in [START_REF] Rensink | Fair testing[END_REF] (mainly a matter of replacing 1 with a √ action, see [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF] for details).

Theorem 3.3 (Resorting to Fair Testing). Let C, C be contracts. We have

N F(C {0/α.C | α ∈ I(C ) -I(C)}) test N F(C) ⇒ C C
The opposite implication does not hold in general. This can be easily seen by considering uncontrollable contracts, i.e. contracts for which there is no compliant test. For instance the contract 0, any other contract a.b.0 or c.d.0 or more complex examples like a + a.b. These contracts are all equivalent according to our refinement relation, but of course not according to fair testing. Notice that such uncontrollable contracts have completely different traces: this means that trace pre-order is not coarser than our refinement relation.

Session Types

In this section we move to session types, in particular we report about our study of asynchronous session subtyping. Session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] are types for controlling the communication behaviour of processes over channels. In a very simple but effective way, they express the pattern of sends and receives that a process must perform. They are, therefore, similar to behavioural contracts, but more constrained in the kind of behaviours they can express. Since they can guarantee freedom from some basic programming errors, session types are becoming popular with many main stream language implementations, e.g., Haskell [START_REF] Lindley | Embedding session types in haskell[END_REF], Go [START_REF] Ng | Static deadlock detection for concurrent go by global session graph synthesis[END_REF] or Rust [START_REF] Jespersen | Session types for Rust[END_REF]. In [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] session subtyping is introduced for asynchronous communication and it is also stated that it is decidable. Recently it has been proven that, on the contrary, it is undecidable. Here we present such an undecidability result [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF] and the decidability result in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF], where the largest known decidable fragment is introduced. In particular, we recall the basic definitions of session types and synchronous and asynchronous session subtyping. We then report the undecidability proof in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF]. Finally, we present the fragment of single-out (and single-in) session types, for which we show asynchronous subtyping to be decidable [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. The techniques for these (un)decidability results can be seen as improvements of those developed for Linda process calculi: reduction from Turing complete computational models and exploitation of well quasi orderings.

Session Subtyping

Session subtyping, which is the counterpart for session types of refinement for behavioural contracts, was first introduced by Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] for a sessionbased π-calculus where communication is synchronous. Session subtyping of [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] is endowed with covariant/contravariant properties that correspond to those we observed on behavioural contract refinement: internal choices on outputs can be reduced, while external choices on inputs can be extended. To the best of our knowledge, Mostrous et al. [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF] were the first to adapt the notion of session subtyping to an asynchronous setting. Their computation model is a session π-calculus with asynchronous communication that makes use of session queues for maintaining the order in which messages are sent. Based on such a model they introduce the idea of output anticipation, which is also relevant for our results in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF] that we present here. Mostrous and Yoshida [START_REF] Mostrous | Session typing and asynchronous subtyping for the higher-order π-calculus[END_REF] extended the notion of asynchronous subtyping to session types for the higher-order πcalculus. They also observed that their definition of asynchronous subtyping allows for orphan messages, i.e. sent messages which are never consumed from the session queue. Orphan messages are, instead, prohibited with the definition of subtyping given by Chen et al. [START_REF] Chen | On the preciseness of subtyping in session types[END_REF]: they show that such a definition is both sound and complete w.r.t. type safety and orphan message freedom.

We start with the formal syntax of binary session types, adopting a simplified notation (used, e.g., in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]) without dedicated constructs for sending an output/receiving an input. We instead represent outputs and inputs directly 3. if T = &{l i : T i } i∈I then ∃n ≥ 0 such that unfold n (S) = &{l j : S j } j∈J , J ⊆ I and ∀j ∈ J. (T j , S j ) ∈ R; 4. if T = µt.T then (T {T /t}, S) ∈ R.

T is a synchronous subtype of S, written T ≤ s S, if there is a synchronous subtyping relation R such that (T, S) ∈ R.

Two types T and S are related by ≤ s , whenever S is able to simulate T with output and input types enjoying covariance and contravariance properties, respectively. Notice the asymmetric use of unfolding between the left-and righthand terms T and S: in T recursion is always unfolded once, while in S many unfoldings can be needed in order to expose the starting operator of T .

As already discussed, subtyping is the counterpart of contract refinement in the context of session types. Consider, for instance, &{a : end, : end} ≤ s &{a : end} ⊕ {a : end} ≤ s ⊕ {a : end, b : end} that hold for input contravariance and output covariance. These examples of subtypings precisely correspond to those of contract refinements commented in Section 3.8. Note that, while in the case of contracts they were obtained as a consequence of considering the maximal independent refinement, in the theory of session types they are taken by definition. We now consider the standard notion of asynchronous subtyping ≤ introduced by Chen et al. [START_REF] Chen | On the preciseness of subtyping in session types[END_REF], which enjoys orphan message freedom; we consider the simple rephrasing based on dual closeness we introduced in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. In the definition of ≤ we use the following notion of input context.

Definition 4.4 (Input Context

). An input context A is a session type with multiple holes defined by the syntax:

A ::= [ ] n | &{l i : A i } i∈I
The holes [ ] n , with n ∈ N + , of an input context A are assumed to be consistently enumerated, i.e. there exists m ≥ 1 such that A includes one and only one [ ] n for each n ≤ m. Given types T 1 ,. . . , T m , we use A[T k ] k∈{1,...,m} to denote the type obtained by filling each hole k in A with the corresponding term T k .

Definition 4.5 (Asynchronous Subtyping, ≤). R is an asynchronous subtyping relation whenever it is dual closed and (T, S) ∈ R implies 1., 3., and 4. of Definition 4.3, plus the following modified version of 2.:

2. if T = ⊕{l i : T i } i∈I then ∃n ≥ 0, A such that • unfold n (S) = A[⊕{l j : S kj } j∈J k ] k∈{1,...,m} ,
• ∀k ∈ {1, . . . , m}. I ⊆ J k and

• ∀i ∈ I, (T i , A[S ki ] k∈{1,...,m} ) ∈ R
T is an asynchronous subtype of S, written T ≤ S, if there is an asynchronous subtyping relation R such that (T, S) ∈ R.

We now explain the modified version of Rule 2. and its impact on the obtained subtyping relation. Concerning the adopted notation, for each hole k of the input context A (which is at the beginnig of the righthand term S after any needed unfolding), we take l j , with j ∈ J k , to be the labels of the output selection in the hole. Moreover, we use S kj to denote the type reached after output l j in the hole k. An important characteristic of asynchronous subtyping (formalized by Rule 2. above) is the following one. In a subtype output selections can be anticipated so to bring them before the input branchings that in the supertype occur in front of them. For example

⊕ l : &{l 1 : T 1 , l 2 : T 2 } ≤ & l 1 : ⊕{l : T 1 }, l 2 : ⊕{l : T 2 }
where the output selection with label l (occurring in the supertype) is anticipated w.r.t. the input branching with labels l 1 and l 2 (such an output selection is present in all its input branches). As already discussed in the Introduction, output anticipation reflects the fact that we are considering asynchronous communication protocols in which messages are stored in queues. In this setting, it is safe to replace a peer that follows a given protocol with another one following a modified protocol where outputs are anticipated: in fact, the difference is simply that such outputs will be stored earlier in the communication queue.

As a further example, consider the types T = µt.&{l : ⊕{l : t}} and S = µt.&{l : &{l : ⊕{l : t}}}. We have T ≤ S by considering an infinite subtyping relation including pairs (T , S ), with S being &{l : S}, &{l : &{l : S}}, &{l : &{l : &{l : S}}}, . . . ; that is, the effect of each output anticipation is that a new input &{l : } is accumulated in the initial part of the r.h.s. It is worth to observe that every accumulated input &{l : } is eventually consumed in the simulation game (orphan message freedom), but the accumulated inputs grows unboundedly.

Undecidability of Asynchronous Subtyping

Asynchronous session subtyping was considered decidable before Bravetti, Carbone and Zavattaro [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF] and Lange and Yoshida [START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] independently proved that it was undecidable. Here, we report the proof of undecidability in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF], which is by reduction from the acceptance problem for queue machines. Queue machines are a variant of Pushdown automata that exploits a queue instead of a stack. Differently from a stack, a queue allows the automata to access any symbol in memory without losing other symbols, that can be simply reenqueued. For this reason, Queue machines are Turing powerful while Pushdown automata are not. Definition 4.6 (Queue machine). A queue machine M is defined by a sixtuple (Q, Σ, Γ, $, s, δ) where: Q is a finite set of states; Σ ⊂ Γ is a finite set denoting the input alphabet; Γ is a finite set denoting the queue alphabet (ranged over by A, B, C, X); $ ∈ Γ -Σ is the initial queue symbol; s ∈ Q is the start state; δ : Q × Γ → Q × Γ * is the transition function.

We now formally define queue machine computations.

1 ? A k ! ..... $? X 1 ? X n ? ..... A 1 ! A k ? Figure 1: Session type encoding the initial queue X 1 • • • Xn$ C 1 • • • C m . Definition 4.8 (Queue Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a queue ma- chine and let C 1 • • • C m ∈ Γ * , with m ≥ 0. We define: [[C 1 • • •C m ]] = &{C 1 : . . . &{C m : µt. ⊕ {A : &{A : t}} A∈Γ }} Given a configuration (q, γ) of M , the encoding of the queue γ = C 1 • • • C m is thus defined as [[C 1 • • • C m ]].
Note that whenever m = 0, we have [[ ]] = µt. ⊕ {A : &{A : t}} A∈Γ . Observe that we are using a slight abuse of notation: in both output selections and input branchings, labels l A , with A ∈ Γ, are simply denoted by A.

We now move to the encoding of the finite control of the queue machine into a session type. In Figure 2, we report a graphical representation of such type. We focus on the transition function δ, and a state q ∈ Q: let us consider δ(q, A i ) = (q i , B i 1 • • • B i ni ), with n i ≥ 0, for all i in {1, . . . , k}. This particular state of the queue machine has a corresponding state [[q]] of the graphical representation of the session type. This state [[q]] performs an input branching with a choice for each symbol in the queue alphabet Γ (with k being the cardinality of Γ). Each of these choices represents a possible symbol that can be read from the queue. In fact, the idea is to play a subtyping simulation game where this type is the subtype, and the type encoding the queue machine (discussed above) is the supertype. The latter initially has an input on a label A j representing the initial symbol of the queue. Hence, the unique branch to be considered in the simulation game is the one having such label A j . After this initial selection, the continuation is composed of a sequence of outputs labeled with the symbols B j 1 • • • B j nj that are expected to be inserted in the queue as the effect of consuming A j from the queue. After these output actions have been considered in the simulation game (with the effect of enqueuing the corresponding symbols, see the discussion above about the encoding of the queue) state [[q i ]] of the session type, corresponding to the subsequent state q i of the queue machine, is reached.

We are now ready to formally define the encoding of the finite control of the queue machine. twice both subterms µt. ⊕{l 2 : T 1 } and µt.& l 4 : µt . ⊕{l 5 : T 2 } . On the other hand, applying outDepth to the same term would unfold once the term reached with l 1 and twice the one reached with l 3 . In the subtyping procedure defined below we make use of outUnf() in order to have that recursive definitions under the scope of an output are never unfolded. This guarantees that during the execution of the procedure, even if the set of reached terms could be unbounded, all the subterms starting with an output are taken from a bounded set of terms. This is important to guarantee termination of the algorithm that we are going to define as an extension of the procedure described below.

In the definition of the procedure, we also make use of the notation & ∈ T to mean that T eventually reaches an input. Formally, & ∈ T if T = &{l i :

T i } i∈I , or T = ⊕{l i : T i } i∈I with & ∈ T i for all i ∈ I, or T = µt.T with & ∈ T .
Subtyping Procedure. An environment Σ is a set containing pairs (T, S), where T and S are types. Judgements are triples of the form Σ T ≤ a S which intuitively read as "in order to succeed, the procedure must check whether T is a subtype of S, provided that pairs in Σ have already been visited". The subtyping procedure, applied to the types T and S, consists of deriving the state space of our judgments using the rules in Figure 3 bottom-up starting from the initial judgement ∅ T ≤ a S. More precisely, we use the transition relation Σ T ≤ a S → Σ T ≤ a S to indicate that if Σ T ≤ a S matches the conclusions of one of the rules in Figure 3, then Σ T ≤ a S is produced by the corresponding premises. The procedure explores the reachable judgements according to this transition relation. We give highest priority to rule Asmp, thus ensuring that at most one rule is applicable. 10 The idea behind Σ is to avoid cycles when dealing with recursive types. Rules RecR 1 and RecR 2 deal with the case in which the type on the right-hand side is a recursion and must be unfolded. If the type on the left-hand side is not an output then the procedure simply adds the current pair to Σ and continues. On the other hand, if an output must be found, we apply RecR 1 which checks whether such output is available. Rule Out allows nested outputs to be anticipated (when not under recursion) and condition A = [ ] 1 ⇒ ∀i ∈ I.& ∈ T i (inspired by [START_REF] Chen | On the preciseness of subtyping in session types[END_REF]) makes sure there are no orphan messages. In fact, this condition implies that if there is some output which is anticipated in the subtype w.r.t. some inputs, in every continuation of the subtype there are input actions that will eventually reproduce also the input behaviour of the supertype. The remaining rules are self-explanatory. Σ T ≤ a S → * Σ T ≤ a S is the reflexive and transitive closure of the transition relation among judgements. We write Σ T ≤ a S → ok if the judgement Σ T ≤ a S matches the conclusion of one of the axioms Asmp or End, and Σ T ≤ a S → err to mean that no rule can be applied to Σ T ≤ a S. Due to input branching and output selection, the rules In and Out could generate branching also in the state space to be explored by the procedure. Namely, given a judgement Σ T ≤ a S, there are several subsequent judgements Σ T ≤ a S such that Σ T ≤ a S → Σ T ≤ a S . The procedure could (i) successfully terminate because all the explored branches reach a successful judgement Σ T ≤ a S → ok , (ii) terminate with an error in case at least one judgement Σ T ≤ a S → err is reached, or (iii) diverge because no branch terminates with an error and at least one branch never reaches a succesful judgement. As we prove in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF] the procedure is sound with respect to asynchronous subtyping ≤ and it can diverge only if the checked types are in the ≤ relation.

(A = [ ] 1 ) ⇒ ∀i ∈ I.& ∈ T i ∀n.I ⊆ J n ∀i ∈ I . Σ T i ≤ a A[S ni ] n Σ ⊕{l i : T i } i∈I ≤ a A[⊕{l j : S nj } j∈Jn ] n Out J ⊆ I ∀j ∈ J . Σ T j ≤ a S j Σ &{l i : T i } i∈I ≤ a &{l j : S j } j∈J In Σ end ≤ a end End Σ, (T, S) T ≤ a S Asmp Σ, (µt.T, S) T {µt.T /t} ≤ a S Σ µt.T ≤ a S RecL T = end ∨ T = &{l i : T i } i∈I Σ, (
If we consider types T and S of the example considered after Definition 4.5 the subtyping procedure in Figure 3 applied to ∅ T ≤ a S does not terminate. The problem is that the termination rule Asmp cannot be applied because the term on the r.h.s. (i.e. the supertype) generates always new terms in the form &{l : &{l : . . . &{l : S} . . . }}. Notice that, in this particular example, these infinitely many distinct terms are obtained by adding single inputs (i.e. singlechoice input branchings) in front of the term in the r.h.s.: we call this linear input accumulation. In general, however, input accumulation takes the form of a tree (thus accounting for all possible alternative accumulated input behaviors at the same time).

We now show how to decide asynchronous subtyping over single-out types, i.e. when input accumulation can indeed be in the general form of a tree, but, due to the absence of output selections with multiple choices, it gets accumulated in a deterministic (i.e. unique) way. This will also allow us to deal with single-in types by exploiting duality. As anticipated, it deals with general input accumulation by representing it as a tree. We need to be able to extract the leaves from the algorithm is intended to check V ≤Z, for some type Z). We start from the initial judgement ∅ V ≤ t Z and then apply from bottom to top the rules in Figure 3, where ≤ a is replaced by ≤ t , plus the following additional rule: S ∈ reach(Z) antOutInf(S) |γ| < |β| leafSet(antOut(S, γ)) = leafSet(antOut(S, β)) Σ, (T, antOut(S, γ)) T ≤ t antOut(S, β) Asmp2

Intuitively, we have that this additional termination rule guarantees to catch all those cases where the term on the right grows indefinitely, by anticipating outputs and accumulating inputs. These infinitely many distinct types are anyway obtainable starting from the finite set reach(Z), by means of output anticipations. Hence there exists S ∈ reach(Z) that can generate infinitely many of these types: this guarantees antOutInf(S) to be true. As observed above, the leaves of such infinitely many terms are themselves taken from the finite set reach(Z); hence the leaf sets are always taken from the finite set of subsets of reach(Z) (which is itself finite, see Proposition 4.1). In Section 2 we have recalled the notion of wqo, and that equality on a finite set is a wqo (i.e., in an infinite sequence of elements taken from a finite set, there are at least to equal elements). The termination of our algorithm follows from this wqo: Asmp2, besides checking conditions that are guaranteed to hold if the procedure ≤ a continues indefinitely, checks for the equality between the set of leaves of the r.h.s. term in the current judgement and the r.h.s. in a previously checked one. This is guaranteed to eventually happen as the set of leaves are taken from a finite domain, and equality is a wqo on this finite domain.

We are finally ready to formally state the decidability results for single-out/ single-in session types proved in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. We start with the single-out case, for which we have recalled the corresponding deciding algorithm. Theorem 4.2 (Decidability for Single-out Types). Asynchronous subtyping ≤ over single-out session types is decidable.

Exploiting dual closeness of ≤, the algorithm presented for single-out types can be applied also to single-in types (it is sufficient to check subtyping on the duals, observing that the dual of a single-in type is single-out).

Corollary 4.1 (Decidability for Single-in Types). Asynchronous subtyping ≤ over single-in session types is decidable.

Conclusion

In this paper we have described the contribution of our research group in the context of three areas of interest for the Coordination conference and its research community: shared dataspace coordination languages, behavioural contracts for service composition, and session types. The common denominator of the presented research is the exploitation of techniques borrowed from concurrency theory, in particular, process algebras and Petri nets.

The paper is not intended to be a survey on the three considered areas of research; survey papers already exists for coordination languages [START_REF] Papadopoulos | Coordination models and languages[END_REF], for the application of process algebras in the context of shared dataspace coordination [START_REF] Busi | A process algebraic view of shared dataspace coordination[END_REF], and for behavioural types [START_REF] Ancona | Behavioral types in programming languages[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF], that include both contracts and session types. On the contrary, the objective of the paper is to present, following an original form of presentation, techniques developed during the early years of formal study of coordination languages, that more recently turned out to be successfully applicable also in other contexts.

More precisely, we started by presenting a novel Linda-based process calculus based on the exchange of tuples of names through a shared dataspace. The distinguishing feature of this calculus is that new names can be produced and passed to other processes simply by placing them inside tuples. For this calculus we have considered the reachability and coverability problems, two properties dealing with the exploration of the reachable states: given a target dataspace, reachability consists of checking whether such dataspace can be reached, while for coverability it is sufficient to reach a state that includes at least the tuples in the target dataspace. By using techniques that we already applied to other shared dataspace process calculi, we have proved that (i) both properties are undecidable in the proposed calculus, (ii) coverability becomes decidable if we assume that processes can use the new names that they receive only inside output operations, while (iii) reachability turns out to be decidable if we remove from the calculus the possibility to generate new names. For undecidability proofs we resort to Random Access Machines, a register based Turing complete formalism, while for the decidability results we exploited Petri nets and Well Structured Transition Systems, that are transition systems equipped with a well quasi ordering on states.

In the second part of the paper we recall the main results in the context of behavioural contracts applied to service oriented computing. We present a language for services having essentially the same syntax of the Linda calculus introduced in the first part of the paper, but with a different semantics: processes (called services in this case) do not share a common message repository, but send messages directly to operations offered by other services. On this language we apply our contract theories by considering both synchronous and asynchronous communication. Contracts describe the input-output communication behaviour of services and can be used to reason about service composition and and service replaceability; formally, we say that a service can be used in place of another one if their behavioural contracts are in refinement relation. One of the open problems of behavioural contracts is an algorithmic characterization of refinement in the case of asynchronous communication.

We have presented behavioural contracts because the interest in trying to close the above open problem on contract refinement for asynchronous communication was the main justification for moving to the study of session types, discussed in the third part of this paper. Session types can be seen as a simplification of contracts that already had, besides a rich and well-established theory, a wide application on concurrent programming languages such as, e.g., Haskell [START_REF] Lindley | Embedding session types in haskell[END_REF], Go [START_REF] Ng | Static deadlock detection for concurrent go by global session graph synthesis[END_REF] and Rust [START_REF] Jespersen | Session types for Rust[END_REF]. We have specifically focused on session sub-typing which is, for session types, a notion equivalent to the notion of refinement in the context of contracts. We have recalled the well-known algorithm by Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] for synchronous session subtyping. For asynchronous communication, on the other hand, algorithms that were presented, like that in [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], revealed wrong: in fact, it was proved that asynchronous session subtyping. We have reported here our undecidability proof that, like those for Linda-like process calculi, is by reduction from the halting problem in Turing complete formalism. In this case we used Queue Machines instead of Random Access Machines. Another recent contribution that we have reported here is an algorithm for checking asynchronous session subtyping under the assumption that output (or input) choices have only one branch. Our algorithm is inspired by the one by Gay and Hole, but in order to deal with asynchronous communication we need a more sophisticated termination condition that must check also messages that have been buffered in the communication channels. The termination of this algorithm is proved by exploiting techniques like those used for the decidability proof in Linda-like calculi, namely, the application of well quasi orderings.

We expect two possible lines for future work: on the one hand, analyse the impact on the theory of contracts of our results for session types (in fact, very few results are present in the literature about contracts for asynchronous communication) and, on the other hand, continue in the context of session types by investigating novel techniques for sound algorithmic characterizations of asynchronous session subtyping.

Definition 2 . 1 (

 21 Processes). Let Name, ranged over by a, b, . . ., be a denumerable set of names. With Message we denote the set of tuples of names, denoted with ã, b, . . .. The class of processes is described by the following grammar: η ::= a | (a) P ::= 1 | out(ã) | in(η)P | (νa)P | P + P | P |P | P ; P | P *

Pη[

  aj / bj ] j∈J -→ P η[ a j / b j ] j∈J = ã P, S ã → P , S P ãb 1 •••bn -→ P ∀i ∈ 1 . . . n.b i ∈ S P, S → P , S ã

  is the process (resp. the dataspace) obtained by replacing names according to the renaming function f . More formally, f is a function from Name to Name, and P [f ] (resp. S[f ]) is obtained by replacing in P (resp. S) each occurrence of a ∈ Name with f (a). With an abuse of notation, we use f (α) to indicate the label obtained by replacing in α each occurrence of a ∈ Name with f (a).

Definition 3 . 1 .

 31 (Services) The syntax of services is defined by the following grammarS ::= 1 | τ | a * | a * | a | a l | S +S | S|S | S; S | S *

Definition 3 . 4 .

 34 (Behavioural Contracts as Terms) We consider a denumerable set of contract variables Var ranged over by X, Y , • • • . The syntax of contracts is defined by the following grammar

Definition 3 . 5 (

 35 Output Persistence). A contract C is output persistent if, for any C such that C w -→ C and C a l -→, the following holds: C √ -→ / and, if C α -→ C with α = a l , then also C a l -→. In the above definition we use C λ -→ to mean ∃C : C λ -→ C .

[

  Reservation travelAgency .(T ravelP lan + N oAvail)] client || [C T ravelAgency ] travelAgency || [ReserveF light.(AvailF lights travelAgency + N oF lights travelAgency )] airRes || [recX.(ReserveRoom.(N oRooms travelAgency .X + AvailRoom travelAgency

Definition 3 . 8 (

 38 Correct Contract Composition -Compliance). A system P is a correct contract composition, denoted P ↓, if for every P such that P τ -→ * P , there exists P such that P τ

Theorem 3 . 2 (

 32 Refinements with Extended Inputs and Outputs). Let C, C be contracts. Both of the following hold

A

Figure 3 :

 3 Figure 3: A Procedure for Checking Subtyping

Table 1 :

 1 The transition system for processes (λ = √ , symmetric rules of PAR and SUM omitted).

Table 2 :

 2 The reduction relation for systems (brackets in singletons are omitted).

Table 4 :

 4 Travel agency service.

	Example 3.2. (Travel Agency)
	As a more involved example we consider, in Table 4, a travel agency service.
	Upon reception of a client's reservation request, the travel agency sends two

* + koF light * ) + N oF lights; koF light * ) | (N oRooms; ReserveRoom hotelRes ) * ; AvailRoom; (okF light * ; T ravelP lan client + koF light * ; N oAvail client )

Table 5 :

 5 Semantic rules for contracts (symmetric rules omitted).

Table 6 :

 6 Reservation.(ReserveF light airRes .ReserveRoom hotelRes .C X + ReserveRoom hotelRes .ReserveF light airRes .C X ) Travel agency contract (trailing ".1" are omitted).

	C X = recX.(
	AvailRoom.(
	AvailF lights.(τ.T ravelP lan client + τ.N oAvail client ) +
	N oF lights.τ.N oAvail client
	) +
	N oRooms.(
	ReserveRoom hotelRes .X +
	AvailF lights.ReserveRoom hotelRes .C Y +
	N oF lights.ReserveRoom hotelRes .C Z
	) +
	AvailF lights.C Y +
	N oF lights.C Z
	)
	C

Y = recY.( AvailRoom.(τ.T ravelP lan client + τ.N oAvail client ) + N oRooms.ReserveRoom hotelRes .Y ) C Z = recZ.( AvailRoom.τ.N oAvail client + N oRooms.ReserveRoom hotelRes .Z )

Table 7 :

 7 Synchronous system semantics (symmetric rules omitted).

  of the travel agency service presented in Example 3.2 (seeTable 4). A supercontract of C T ravelAgency is obtained by considering the contract of a modified version of the travel agency service where we replace the line(N oRooms; ReserveRoom hotelRes ) * ; AvailRoom;The obtained contract C is a modification of that presented in Table6where in the definition of contracts C X , C Y and C Z we just remove the whole branch of choice (i.e. "+ ) starting with the "N oRooms" input (in the case of C Y and C Z the choice itself is consequently removed). Since in such a contract C the "N oRooms" input no longer occurs, we have N oRooms ∈ I(C T ravelAgency ) -I(C), hence, according to Theorem 3.2 (first statement), C T ravelAgency ≺ C. Formally this derives from the fact that C ≺ C and that the LTS of C{0/α.C | α ∈ I(C T ravelAgency ) -I(C)} is the same as that of C T ravelAgency .

	in Table 4 with just
	AvailRoom;

  T, µt.S) T ≤ a S{µt.S/t} Σ T ≤ a µt.S RecR 1 outDepth(S) ≥ 1 Σ, (⊕{l i : T i } i∈I , S) ⊕{l i : T i } i∈I ≤ a outUnf(S) Σ ⊕{l i : T i } i∈I ≤ a S RecR 2

In the real system, temperature and humidity are expected to be measured at each iteration. In our simplified abstract model, we represent all these possibly different measures with the same names t and h.

The side condition in SEQ1 avoids name captures between new names in the first process and free names in the second process in a sequential composition.

The compatibility notion used in this paper is named strict compatibility in[START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

It is possible to consider α-conversion because in the statement of the Theorem we consider P, S ⇓ T , which is defined on the standard semantics including α-conversion.

In the following, when writing services, we omit parentheses under the assumption that sequencing ; takes priority over choice + and parallel | .

We also omit parentheses under the assumption that prefix α. takes priority over choice + (similarly as we did for services).

As for basic CCS[START_REF] Milner | Communication and concurrency[END_REF] finite-stateness is an obvious consequence of the fact that the process algebra does not include static operators, like parallel or restriction.

In[START_REF] Bravetti | A Foundational Theory of Contracts for Multiparty Service Composition[END_REF] the same effect of requiring each output "a l " to syntactically occur as "τ ; a l " is obtained by modifying service operational semantics of Table3so that outputs are executed in two steps: the first step is a "τ " transition and the second step the actual "a l " transition.

Differently from our definitions, in the channel-based approach of Gay and Hole[START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] subtyping is covariant on branchings and contra-variant on selections.

The priority of Asmp is sufficient because all the other rules are alternative, i.e., given a judgement Σ T ≤a S there are no two rules different from Asmp that can be both applied.

inside choices. More precisely, we consider output selection ⊕{l i : T i } i∈I , expressing an internal choice among outputs, and input branching &{l i : T i } i∈I , expressing an external choice among inputs. Each possible choice is labeled by a label l i , taken from a global set of labels L, followed by a session continuation T i . Labels in a branching/selection are assumed to be pairwise distinct. Definition 4.1 (Session Types). Given a set of labels L, ranged over by l, the syntax of binary session types is given by the following grammar:

A session type is single-out if, for all of its subterms ⊕{l i : T i } i∈I , |I| = 1; it is single-in if, for all of its subterms &{l i :

In the sequel, we leave implicit the index set i ∈ I in input branchings and output selections when it is already clear from the denotation of the types. Note also that we abstract from the type of the message that could be sent over the channel, since this is orthogonal to our theory. Types µt.T and t denote standard tail recursion for recursive types. We assume recursion to be guarded: in µt.T , the recursion variable t occurs within the scope of an output or an input type. In the following, we will consider closed terms only, i.e., types with all recursion variables t occurring under the scope of a corresponding definition µt.T . Type end denotes the type of a channel that can no longer be used.

For session types, we define the usual notion of duality: given a session type T , its dual T is defined as: ⊕{l i : T i } i∈I = &{l i : T i } i∈I , &{l i : T i } i∈I = ⊕{l i : T i } i∈I , end = end, t = t, and µt.T = µt.T . In the sequel, we say that a relation R on session types is dual closed if (S, T ) ∈ R implies (T , S) ∈ R.

We start by considering a synchronous subtyping relation, similar to that of Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] but, to be more consistent with contracts, following a process-oriented instead of a channel-based approach. 9 Moreover, following [START_REF] Mostrous | Global principal typing in partially commutative asynchronous sessions[END_REF], we consider a generalized version of unfolding that allows us to unfold recursions µt.T as many times as needed. Definition 4.2 (n-unfolding).

Definition 4.3 (Synchronous Subtyping, ≤ s ). R is a synchronous subtyping relation whenever (T, S) ∈ R implies that:

1. if T = end then ∃n ≥ 0 such that unfold n (S) = end; 2. if T = ⊕{l i : T i } i∈I then ∃n ≥ 0 such that unfold n (S) = ⊕{l j : S j } j∈J , I ⊆ J and ∀i ∈ I. (T i , S i ) ∈ R; Definition 4.7 (Queue machine computation). A configuration of a queue machine is an ordered pair (q, γ) where q ∈ Q is its current state and γ ∈ Γ * is the queue (Γ * is the Kleene closure of Γ). The starting configuration on an input string x is (s, x$). The transition relation → M over configurations Q×Γ * , leading from a configuration to the next one, is defined as follows. For any p, q ∈ Q, A ∈ Γ and α, γ ∈ Γ * we have (p, Aα) → M (q, αγ) whenever δ(p, A) = (q, γ).

A machine M accepts an input x if it eventually terminates on input x, i.e. it reaches a blocking configuration with the empty queue (notice that, as the transition relation is total, the unique way to terminate is by emptying the queue). Formally, x is accepted by M if (s, x$) → * M (q, ) where is the empty string and → * M is the reflexive and transitive closure of → M .

As observed above Queue machines are Turing complete, see [START_REF] Kozen | Automata and computability[END_REF] (page 354) and [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF], hence it is undecidable whether a queue machine M accepts input x.

The undecidability of asynchronous session subtyping is proved as follows: given queue machine M with input x, construct a pair of types, say T and S, such that: T ≤ S if and only if x is not accepted by M . Given the undecidability of the acceptance problem for queue machines, we also have the undecidability of session subtyping.

Consider a queue machine M with input x. We will define a type T that encodes the finite control of M , i.e., its transition function δ, starting from its initial state s. We first concentrate on the definition of a type S that encodes the machine queue that initially contains x$, where assume x to be the input string x = X 1 • • • X n of length n ≥ 0. Before presenting the formal definition of this type S, we discuss Figure 1 which contains a graphical representation of such type. Session types can be represented as labeled transition systems (in the form of communicating automata [START_REF] Brand | On communicating finite-state machines[END_REF]), where an output selection ⊕{l i : T i } i∈I is represented as a choice among alternative output transitions labeled with "l i !", and an input branching &{l i : T i } i∈I is represented as a choice among alternative input transitions labeled with "l i ?".

In Figure 1 we report the graphical representation of the session type used to model the initial queue with content X 1 • • • X n $. Such session type starts with n + 1 inputs, respectively on the labels X 1 • • • X n $ (notice that the label alphabet for the session type corresponds with the queue alphabet Γ of the queue machine). After such sequence of inputs, there is a recursive type representing the capability to enqueue new symbols. Such a type repeatedly performs an output selection with one choice for each symbol A i in the queue alphabet Γ (with k being the cardinality of Γ), followed by an input labeled with the same symbol A i . In this way, assuming to play the subtyping simulation game, the effect of simulating an output on label A i is that of adding a new input on label A i at the end of the sequence of input on labels X 1 • • • X n $. In other words, this coincides with enqueueing A i as the new sequence of inputs X

We are now ready to formally define the encoding of the queue of a machine into a session type. Notice that, in order to have a general definition, instead of considering the initial queue X 1 • • • X n $ we consider a generic queue content

Figure 2: Session type encoding a finite control (for Γ = {A i |i ≤ k} and δ(q

Definition 4.9 (Finite Control Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a queue machine and let q ∈ Q and S ⊆ Q. We define:

The encoding of the transition function of M is then defined as

We finally state our undecidability result by means of the Theorem below which was proved in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF].

Decidability of Single-Out/Single-In Asynchronous Subtyping

We have seen that the problem of checking asynchronous session subtyping is undecidable. Despite this negative result, several simplified cases have been considered in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF] for which asynchronous session subtyping tunrs out to be decidable. These simplified cases are obtained by imposing limitations to the session type syntax. Here, we report the decidability result for the two fragments of single-out and single-in session types, which was proved in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF]. These fragments are more general than those presented in [START_REF] Bravetti | Undecidability of asynchronous session subtyping[END_REF][START_REF] Lange | On the undecidability of asynchronous session subtyping[END_REF].

We start by recalling a procedure (an algorithm that does not necessarily terminate) for the general subtyping relation, which we previously showed to be undecidable. We first introduce two functions on the syntax of types.

The function outDepth calculates how many unfoldings are necessary for bringing an output outside a recursion (in every possible input path). If that is not possible, the function is undefined (denoted by ⊥). As an example consider, for any T 1 and T 2 , outDepth(⊕{l 1 : T 1 , l 2 : T 2 }) = 0. On the other hand, consider the type

We then define outUnf(), a variant of the unfolding function given in Definition 4.2, which unfolds only where it is necessary, in order to reach an output. The function above differs from unfold n : for example, unfold 2 T ex would unfold these trees: this is done by the leaf set function. The leaf set of a session type T is the set of subterms reachable from its root through a path of inputs. For example, the leaf set of the term &{l 1 : µt.⊕{l 2 : t}, l 3 : &{l 4 : ⊕{l 2 : µt.⊕{l 2 : t}}}} is {µt. ⊕ {l 2 : t}, ⊕{l 2 : µt. ⊕ {l 2 : t}}.

During the check of subtyping, according to Figure 3 (rule Out), when a term in the r.h.s. having input accumulation has to mimic an output in front of the l.h.s., such output must be present in front of all the leaves of the tree. In this case, the checking continues by anticipating the output from all the leaves. We make use of an auxiliary output anticipation function, called antOut, that indicates the way a term changes after having anticipated a sequence of outputs. antOut(T, l) yields the term obtained from T by anticipating all outputs occurring in the sequence l. For example, the function applied to the type T = µt. ⊕ l 1 : &{l : ⊕{l 2 : t}, l : ⊕{l 2 : t} and the sequence (l 1 , l 2 ) returns &{l : T, l : T }, while it is undefined with the sequence (l 1 , l 1 ). Moreover, we say that T can infinitely anticipate outputs, written antOutInf(T ), if there exists an infinite sequence of labels

defined for every n. The definition of antOutInf(T ) is not algorithmic in that it quantifies on every possible natural number n. Nevertheless, it can be decided by checking whether, for every session type obtained from T by means of output anticipations, all the terms populating its leaf set can anticipate the same output label. Although the types that can be obtained from T by means of output anticipations may be infinite, the terms populating the leaf sets are finite and are over-approximated by the function reach(T ) which is defined as the minimal set of (single-out) session types such that:

1. T ∈ reach(T ); 2. &{l i : T i } i∈I ∈ reach(T ) implies T i ∈ reach(T ) for every i ∈ I; 3. µt.T ∈ reach(T ) implies T {µt.T /t} ∈ reach(T ); 4. ⊕{l : T } ∈ reach(T ) implies T ∈ reach(T ).

Notice that reach(T ) contains the session types obtained by consuming initial inputs and outputs, and by unfolding recursion when it is at the top level.

We now recall the decidability of antOutInf(T ) and the finiteness of reach(T ) that were proved in [START_REF] Bravetti | On the boundary between decidability and undecidability of asynchronous session subtyping[END_REF], and that will be used in the next subsection. Proposition 4.1. Given a single-out session type T , reach(T ) is finite and it is decidable whether antOutInf(T ).

Subtyping algorithm for single-out types. We are now ready to present an additional termination condition that, once included into the subtyping procedure in Figure 3, makes it a valid algorithm for checking subtyping for single-out types. The termination condition is defined as an additional rule, named Asmp2, that complements the already defined Asmp rule by detecting those cases in which the subtyping procedure in Figure 3 does not terminate (Asmp2, presented below, is assumed to have the same priority as rule Asmp: both rules have highest priority). The new rule is defined parametrically on the session type Z, which is the type on the right-hand side of the initial pair of types to be checked (i.e.