Lucia Acciai

Michele Boreale

Gianluigi

Gianluigi Zavattaro

Behavioural contracts with request-response operations ⋆

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

One interesting aspect of Service Oriented Computing (SOC) and Web Services technology is the need to describe in rigorous terms not only the format of the messages exchanged among interacting parties, but also their protocol of interaction. This specific aspect is clearly described in the Introduction of the Web Service Conversation Language (WSCL) specification [START_REF]W3C: Web Services Conversation Language (WSCL)[END_REF], one of the proposals of the World Wide Web Consortium (W3C) for the description of the so-called Web Services abstract interfaces:

Defining which XML documents are expected by a Web service or are sent back as a response is not enough. It is also necessary to define the order in which these documents need to be exchanged; in other words, a business level conversation needs to be specified. By specifying the conversations supported by a Web service -by defining the documents to be exchanged and the order in which they may be exchanged-the external visible behavior of a Web service, its abstract interface, is defined.

The abstract interface of services can be used in several ways. For instance, one could check the compliance between a client and a service, that is, a guarantee for the client that the interaction with the service will in any case be completed successfully. One could also check, during the service discovery phase, the conformance of a concrete service to a given abstract interface by verifying whether the service implements at least the expected functionalities and does not require more.

Formal models are called for to devise rigorous forms of reasoning and verification techniques for services and abstract interfaces. To this aim, theories of behavioural contracts based on CCS-like process calculi [START_REF] Milner | Communication and concurrency[END_REF] have been thoroughly investigated [START_REF] Boreale | Advanced mechanisms for service composition, query and discovery[END_REF][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][START_REF] Carpineti | A Formal Account of Contracts for Web Services[END_REF][START_REF] Castagna | A Theory of Contracts for Web Services[END_REF][START_REF] Castagna | Contracts for Mobile Processes[END_REF]. However, these models lack of expressiveness in at least one respect: they cannot be employed to describe bidirectional request-response interactions, in contexts where several instances of the client and of the service may be running at the same time. This situation, on the other hand, is commonly found in practiceoriented contract languages, like the abstract service interface language WSCL [START_REF]W3C: Web Services Conversation Language (WSCL)[END_REF] and Abstract WS-BPEL [START_REF]OASIS: Web Services Business Process Execution Language (WSBPEL)[END_REF].

In this paper, we begin a formal investigation of contract languages of the type described above, that is allowing bidirectional request-response interaction, taking place between instances of services and clients. We present two contract languages that, for simplicity, include only the request-response pattern 1 : the first language is inspired by WSCL while the second one by Abstract WS-BPEL. In both these models, the requestresponse interaction pattern is decomposed into sequences of more fundamental sendreceive-reply steps: the client first sends its invocation, then the service receives such an invocation, and finally the service sends its reply message back to the client. The binding between the requesting and the responding sides (instances) of the original operation is maintained by employing naming mechanisms similar to those found in the π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF]. In both models, we do not put any restriction on the number of client or service instances that can be generated at runtime, so that the resulting systems are in general infinite-state. The difference between the two models is that in the former it is not possible to describe intermediary activities of the service between the receive and the reply steps, while this is possible in the latter. In fact, WSCL models the service behaviour in request-response interactions with a unique ReceiveSend primitive indicating the kind of incoming and outgoing messages. On the contrary, in Abstract WS-BPEL there exist two distinct primitives that allows one to model independently the receive and the reply steps.

We define client-service compliance on the basis of the must testing relation of [START_REF] De Nicola | Testing equivalences for processes[END_REF]: a client and a service are compliant if any sequence of interactions between them leads the client to a successful state. Our main results show that client-service compliance is decidable in the WSCL-inspired model, while it is undecidable in the Abstract WS-BPEL model: this points to an interesting expressiveness gap between the two approches for the modeling of the request-response interaction pattern. In the former case, the decidability proof is based on a translation of contracts into Petri nets. This translation is not precise, in the sense that intermediate steps of the request-response interaction are not represented in the Petri net. However, the translation is complete, in the sense that it preserves and reflects the existence of unsuccessful computations, which is enough to reduce the original compliance problem to a decidable problem in Petri nets. This yields a practical compliance-checking procedure, obtained by adaptation of the classical Karp-Miller coverability tree construction [START_REF] Karp | Parallel Program Schemata[END_REF].

The rest of the paper is organized as follows. In Section 2 we present the two formal models and the definition of client-service compliance. Sections 3 contains the Petri nets semantics and the proof of decidability of client-service compliance for the WSCL model. Section 4 reports on undecidability for the Abstract WS-BPEL model. We draw some conclusions and discuss further work in Section 5.

Behavioural contracts with request-response

We presuppose a denumerable set of contract variables Var ranged over by X, Y, • • • , a denumerable set of names Names ranged over by a, b, r, s, • • • . We use I, J, • • • to denote a sets of indexes.

Definition 1 (WSCL Contracts). The syntax of WSCL contracts is defined by the following grammar

G ::= invoke(a, i∈I b i .C i ) | recreply(a, i∈I b i .C i ) | √ C ::= i∈I G i | C|C | X | recX.C
where recX._ is a binder for the contract variable X. We assume guarded recursion, that is, given a contract recX.C all the free occurrences of X in C are inside a guarded contract G. A client contract is a contract C containing at least one occurrence of the guarded success contract √ , while a service contract is a contract not containing √ .

G is used to denote guarded contracts, ready to perform either an invoke or a receive on a request-response operation a: the selection of the continuation C i depends on the actual reply message b i . A set of guarded contracts G i can be combined into a choice i∈I G i ; if the index set I is empty, we denote this term by 0. Contracts can be composed in parallel. Note that infinite-state contract systems can be defined using recursion (see example later in the section). In the following, we use Names(C) to denote the set of names occurring in C. Before presenting the semantics of WSCL contracts, we introduce BPEL contracts as well.

Definition 2 (BPEL Contracts). BPEL contracts are defined like WSCL contracts in Definition 1, with the only difference that guarded contracts are as follows

G ::= invoke(a, i∈I b i .C i ) | receive(a).C | reply(a,b).C | √ .
We now define the operational semantics of both models. We start by observing that the WSCL contract recreply(a, i∈I b i .C i ) is the same as the BPEL contract receive(a). i∈I reply(a,b i ).C i that receives an invocation on the operation a and then replies with one of the messages b i . We shall rely on a run-time syntax of contracts, which is obtained from the original one by extending the clause for guarded contract, thus G ::= • • • | a r | r b .C. Both terms a r and r b .C are used to represent an emitted and pending invocation of a request-response operation a: the name r represents a (fresh) channel r that will be used by the invoked operation to send the reply message back to the invoker. From now onwards we will call (WSCL) contract any term that could be obtained from this run-time syntax. In the following, we let Labels

△ = {τ, √ } ∪ {a b , a b , (a) | a, b ∈ Names}.
Definition 3 (Operational semantics). The operational semantics of a contract is given by the minimal labeled transition system, with labels taken from the set Labels, satisfying the following axiom and rules (a, b, r ∈ Names)

G l α -→ G ′ l l ∈ I i∈I G i α -→ G ′ l r Names( i∈I b i .C i ) invoke(a, i∈I b i .C i ) (r) -→ i∈I (r b i .C i ) | a r receive(a).C a r -→ C{ r /a} reply(r,b).C τ -→ C | r b √ √ -→ 0 r b r b -→ 0 r b .C r b -→ C P a b -→ P ′ Q a b -→ Q ′ P|Q τ -→ P ′ |Q ′ P α -→ P ′ α (r) P|Q α -→ P ′ |Q P (r) -→ P ′ r Names(Q) P|Q α -→ P ′ |Q C{ recX.C /X} α -→ C ′ recX.C α -→ C ′
plus the symmetric version of the three rules for parallel composition. With C{ r /a} we denote the term obtained from C by replacing with r every occurrence of a not inside a receive(a).D, while C{ recX.C /X} denotes the usual substitution of free contract variables with the corresponding definition.

In the following, we use C α -→ to say that there is some C ′ such that C α -→ C ′ . Moreover, we use C -→ C ′ to denote reductions, i.e. transitions that C can perform also when it is in isolation. Namely,

C -→ C ′ if C τ -→ C ′ or C (r)
-→ C ′ for some r. We now formalize the notion of client-service compliance resorting to musttesting [START_REF] De Nicola | Testing equivalences for processes[END_REF]. Intuitively, a client C is compliant with a service contract S if all the computations of the system C|S lead to the client's success. Other notions of compliance have been put forward in the literature [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]; we have chosen this one because of its technical and conceptual simplicity (see e.g. [START_REF] Carpineti | A Formal Account of Contracts for Web Services[END_REF]).

Definition 4 (Client-Service compliance). Given a contract D, a computation is a sequence of reduction steps D

1 -→ D 2 -→ • • • -→ D n -→ • • • . It is a maximal computation if it

is infinite or it ends in a state D n such that D n has no outgoing reductions.

A client contract C is compliant with a service contract S if for every maximal

computation C|S -→ D 1 -→ • • • -→ D l -→ • • • there exists k such that D k √ -→.
Example 1 (An impatient client and a latecomer service). This example shows that even very simple WSCL scenarios could result in infinite-state systems. Consider a client C that asks the box office service S for some tickets and then waits for them by listening on offerTicket. Our client is impatient: at any time, it can decide to stop waiting and issue a new request. This behaviour can be described in WSCL as follows

C △ = recX. invoke(requireTicket, ok.X) + recreply(offerTicket, ok. √ )
Consider the box office service S , defined below, that is always ready to receive a requireTicket invocation and immediately responds by notifying (performing a callback) on offerTicket.

S △ = recX.

recreply(requireTicket, ok.(invoke(offerTicket,ok)|X))

It is easy to see that, in case invoke(offerTicket, • • • ) on the service side and recreply(offerTicket, • • • ) on the client side never synchronize, C|S generates an infinite-state system where each state is characterized by an arbitrary number of invoke(offerTicket, • • • ). This infinite computation, moreover, does not traverse states in which the client can perform its √ action, thus C is not compliant with S according to Definition 4. 2

Decidability of client-service compliance for WSCL contracts

We translate WSCL contract systems into place/transitions Petri nets [START_REF] Petri | Kommunikation mit Automaten[END_REF], an infinitestate model in which several reachability problems are decidable (see, e.g., [START_REF] Esparza | Decidability Issues for Petri Nets -a survey[END_REF] for a review of decidable problems for finite Petri nets). The translation into Petri nets does not faithfully reproduce the operational semantics of contracts. In particular, in finite Petri nets it is not possible to represent the unbounded number of names dynamically created in contract systems to bind the reply messages to the corresponding invocations. The Petri net semantics that we present models bi-directional request-response interactions as a unique event, thus merging together the four distinct events in the operational semantics of contracts: the emission and the reception of the invocation, and the emission and the reception of the reply. We will prove that this alternative modeling preserves client-service compliance because in WSCL the invoker and the invoked contracts do not interact with other contracts during the request-response.

Another difference is that the Petri net semantics can be easily modified so that when the client contract enters in a successful state, i.e. a state with an outgoing transition √ , the corresponding Petri net enters a particular successful state and blocks its execution. This way, a client contract is compliant with a service contract if and only if in the corresponding Petri net all computations are finite and finish in a successful state. As we will show, this last property is verifiable for finite Petri nets using the so-called coverability tree [START_REF] Karp | Parallel Program Schemata[END_REF].

A Petri net semantics for WSCL contracts

We first recall the definition of Petri nets. For any set S , we let M f in (S ) be the set of the finite multisets (markings) over S .

0 [ m 1 [ m 2 • • • m n [ m.
Note that in c ⇒ p, the marking c represents the tokens to be "consumed", while the marking p represents the tokens to be "produced". The Petri net semantics that we present for WSCL contracts decomposes contract terms into multisets of terms, that represents sequential contracts at different stages of invocation. We introduce the decomposition function in Definition 7. Instrumental to this definition is the set Pl(C), for C a WSCL contract, defined below.

Pl(C) △ = { i∈I G i , a↑ i∈I b i .C i , c↓ i∈I b i .C i : i∈I G i , i∈I b i .C i occur in C (k) , a, c ∈ Names(C (k) )}.
D i ) = a↑ i∈I b i .D i if a r occurs in C dec C ( i∈I r b i .D i ) = c↓ i∈I b i .D i if r c occurs in C and c b i for every i ∈ I dec C (recX.D) = dec C (D{ recX.D /X}) dec C (a b ) = ∅ dec C (D 1 |D 2 ) = dec C (D 1 ) ⊕ dec C (D 2 ) dec C (D) = D, otherwise
There are three kinds of transitions in the Petri net we are going to define: transitions representing the emission of an invocation, transitions representing (atomically) the reception of the invocation and the emission and reception of the reply, and transitions representing (atomically) the reception of the invocation and the emission of a reply that will never be received by the invoker because it is outside the set of admitted replies. These three cases are taken into account in the definition below. Definition 8 (Petri net semantics). Let C be a WSCL contract system as in Definition 1. We define Net(C) as the Petri net (S , T ) where: -S = Pl(C);

{ i∈I G i } ⇒ {a↑ j∈J b j .C j } if G k = invoke(a, j∈J b j .C j ) for some k ∈ I {a↑ j∈J b j .C j , i∈I G i } ⇒ dec(C y ) ⊕ dec(D z ) if          G k = recreply(a, l∈L c l .D l ) for some k ∈ I and b y = c z for some y ∈ J, z ∈ L {a↑ j∈J b j .C j , i∈I G i } ⇒ {c z ↓ j∈J b j .C j } ⊕ dec(D z ) if          G k = recreply(a,
-T ⊆ M f in (S ) × M f in (S )
includes all the transitions that are instances of the transitions schemata in Table 1.

We define the marked net Net m (C) as the marked net (S , T, m 0 ), where the initial marking is m 0 = dec(C). The marked net Net m (S |C) is depicted on the right. A bunch of unreachable places (like ok ↓ok. √ , ok ↑ok. √ , . . .) have been omitted for the sake of clarity.

C ′ S ′ requireTicket↑ok.C invoke(offerTicket,ok) offerTicket↑ok √
We divide the proof of the correspondence between the operational and the Petri net semantics of WSCL contracts in two parts: we first prove a soundness result showing that all Petri net computations reflect computations of contracts, and then a completeness result showing that contract computations leading to a state in which there are no uncompleted request-response interactions are reproduced in the Petri net.

In the proof of the soundness result we use the following structural congruence rule to remove empty contracts and in order to rearrange the order of contracts in parallel compositions. Let ≡ be the minimal congruence for contract systems such as

C|0 ≡ C C|D ≡ D|C C|(D|E) ≡ (C|D)|E recX.C ≡ C{ recX.C /X}
As usual, we have that the structural congruence respects the operational semantics. The following result establishes a precise relationship between the form of m and the form of C when dec(C) = m. Lemma 1. Let C be a WSCL contract system and suppose dec(C) = m. The following holds: In order to prove that the Petri net semantics preserves client-service compliance, we need to introduce the notion of success marking. A success marking m contain at least one token in a place corresponding to a successful client state, formally, m( i∈I G i ) > 0 for some contract i∈I G i such that G k = √ , for some k ∈ I. We are now ready to prove the soundness result. Proof: The proof proceeds by case analysis on the three possible kinds of transition. Notice that any initial WSCL contract (according to the syntax of Definition 1) is stable.

1. if m = { i∈I G i } ⊕ m ′ then C ≡ i∈I G i | D, for some D such that dec(D) = m ′ ; 2. if m = {a↑ j∈J b j .C j } ⊕ m ′ then C ≡ j∈J r b j .C j | a r | D,

If m[ m ′ by applying the first kind of transition then

m = { j∈J G j } ⊕ m ′′ , with G k = invoke(a, i∈I b i .C i ) for a k ∈ J. Moreover, m ′ = {a↑ i∈I b i .C i } ⊕ m ′′ . By Lemma 1, D ≡ j∈J G j | C ′ -→ a r | i∈I r b i .C i | C ′ △ = D ′ and dec(D ′ ) = m ′ . 2. If
D -→ j∈J r b j .C j | l∈L reply(r,c l ).D l | C ′ -→ j∈J r b j .C j | r c z | D z | C ′ -→ C y | D z | C ′ △ = D ′ with dec(D ′ ) = dec(C y ) ⊕ dec(D z ) ⊕ m ′′ = m ′ .

Lemma 2. Suppose C is stable and that

C -→ C ′ . Then, there exists C ′′ stable such that C ′ -→ C 1 -→ • • • -→ C l -→ C ′′ (l ≥ 0) and for each i = 1, • • • , l it holds that C i √ -→ .
Proof: If C ′ is not stable then it may contain both unguarded reply actions and pairs of the form r b and r b . According to the operational semantics of contracts, all unguarded reply actions and r b and r b can be consumed performing a sequence of reductions. Therefore a stable contract C ′′ can be reached from C ′ without traversing any state capable of √ -→.

✷ We now move to the completeness part.

Theorem 2 (Completeness). Let C be a WSCL contract and let D be a contract reachable from C through the computation C

= C 0 -→ C 1 -→ • • • -→ C n = D. If D is stable then there exists a computation m 0 [ m 1 [ m 2 • • • m l-1 [ m l of the marked Petri net Net m (C) such that dec(D) = m l . Moreover, if there exists no k ∈ {0, • • • , n} such that C k √ -→ then for every j ∈ {0, • • • , l} we have that m j is not a success marking.
Proof: The proof is by induction on the length n of the derivation

C = C 0 -→ C 1 -→ • • • -→ C n = D.
The base case (n = 0) is trivial. In the inductive case there are two possible cases: C n-1 is stable or it is not stable. In the first case the proof is straightforward. In the second case, there are two possible scenarios to be considered: either C n contains an unguarded action reply(r,b) term, or it contains a pair of matching terms r b and r b . We consider the first of these two cases, the second one can be treated similarly.

Let C n-1 be a non stable contract containing an unguarded action reply(r,b). This action cannot appear unguarded in the initial contract C: let C j , with j > 0, be the first contract traversed during the computation of C in which the action reply(r,b) appears unguarded. Hence, we have that C j-1 -→ C j consists of the execution of a receive action. We now consider a different computation from C to D obtained by rearranging the order of the steps in the considered computation

C = C 0 -→ C 1 -→ • • • -→ C n = D. Namely, let C = C 0 -→ C 1 -→ • • • -→ C l-1 -→ C ′ l -→ • • • -→ C ′ n-2 -→ C n-1 -→ C n = D be
the computation obtained by delaying as much as possible the execution of the receive action generating the unguarded action reply(r,b). In the new computation, this action appears for the first time in the contract C n-1 . Moreover, C ′ n-2 must be a stable contract otherwise C n is not stable. Hence, we can straightforwardly prove the thesis by applying the inductive hypothesis to the shorter computation

C = C 0 -→ C 1 -→ • • • -→ C l-1 -→ C ′ l -→ • • • -→ C ′ n-2 leading to the stable contract C ′ n-2 .
✷ As a simple corollary of the last two theorems, we have that client-service compliance is preserved by the Petri net semantics.

Corollary 1 (Compliance preservation). Let C and S be respectively a WSCL and service contract, as in Definition 1. We have that C is compliant with S if and only if in the marked Petri net Net m (C|S ) all the maximal computations traverse at least one success marking.

Proof: (⇒). Trivial by Theorem 1.

(⇐). Suppose that in Net m (C|S ) all the maximal computations traverse at least one success marking and suppose by contradiction that C is not compliant with S . This means that there is a maximal computation from C|S that does not traverse a state D such that D √ -→. This computation can either end in a state D ′ with no outgoing reductions or can be infinite.

In the first case we get a contradiction by Theorem 2. Indeed there would be a maximal computation from Net m (C|S ) traversing only non-success markings.

Consider the second case. From the infinite sequence of reductions, we can build an infinite set of maximal computations of arbitrary length, starting from C and ending in a stable state (Lemma 2) without traversing a succes state. By Theorem 2, for each of these maximal computations there exists a corresponding maximal computation in the net Net m (S |C) that does not traverse a success marking. We can arrange these computations so as to form a tree where m ′ is a child of m iff m[ m ′ : this is an infinite, but finite-branching, tree. By König's lemma, in Net m (S |C) there exists then an infinite computation that does not traverse a success marking and we get a contradiction. ✷

Verifying client-service compliance using the Petri net semantics

In the light of Corollary 1, checking whether C is compliant with S reduces to verifying if all the maximal computations in Net m (C|S ) traverse at least one success marking. In order to verify this property, we proceed as follows:

we first modify the net semantics in such a way that the net computations block if they reach a success markings; we define a (terminating) algorithm for checking whether in the modified Petri net all the maximal computations are finite and end in a success marking.

The modified Petri net semantics simply adds one place that initially contains one token. All transitions consume such a token, and reproduce it only if they do not introduce tokens in success places, i.e., places i∈I G i such that G k = √ for some k ∈ I Definition 10 (Modified Petri net semantics). Let C be a WSCL contract and Net(C) = (S , T ) the corresponding Petri net as defined in Definition 8. We define ModNet(C) as the Petri net (S ′ , T ′ ) where:

-S ′ = S ∪ {run}, where run is an additional place; for each transition c ⇒ p ∈ T , then T ′ contains a transition that consumes the multiset c ⊎ {run} and produces either p, if p contains a place i∈I G i such that G k = √ for some k ∈ I, or p ⊎ {run}, otherwise.

The marked modified net ModNet m (C) is defined as the net ModNet(C) with initial marking m 0 where

m 0 = dec(C) ⊎ {run} if dec(C) is not a success marking dec(C) otherwise.
We now state an important relationship between Net m (C) and ModNet m (C). It can be proved by relying on the definition of modified net. Proposition 3. Let C be a WSCL contract, Net m (C) (resp. ModNet m (C)) the corresponding Petri net (resp. modified Petri net). We have that all the maximal computations of Net m (C) traverse at least one success marking if and only if in ModNet m (C) all the maximal computations are finite and end in a success marking.

We now present the algorithm for checking whether in a Petri net all the maximal computations are finite and end in a success marking. In the algorithm and in the proof, we utilize the following preorder over multisets on Places(C): m m ′ iff for each p, m(p) ≤ m ′ (p). It can be shown that this preorder is a well-quasi-order, that is, in any infinite sequence of multisets there is a pair of multisets m and m ′ such that m m ′ (see e.g. [START_REF] Finkel | Well-Structured Transition Systems Everywhere![END_REF]). Theorem 3. Let C be a WSCL contract as in Definition 1 and let ModNet m (C) = (S , T, m 0 ) be the corresponding modified Petri net. The algorithm described in Table 2 always terminates. Moreover, it returns TRUE iff all the maximal computations in ModNet m (C) are finite and end in a success marking.

Undecidability of client-service compliance for BPEL contracts

We now move to the proof that client-service compliance is undecidable for BPEL contracts. The proof is by reduction from the termination problem in Random Access Machines (RAMs) [START_REF] Minsky | Computation: finite and infinite machines[END_REF], a well known Turing powerful formalism based on registers containing nonnegative natural numbers. The registers are used by a program, that is a set of indexed instructions I i which are of two possible kinds:

i : Inc(r j ) that increments the register r j and then moves to the execution of the instruction with index i + 1 and i : DecJump(r j , s) that attempts to decrement the register r j ; if the register does not hold 0 then the register is actually decremented and the next instruction is the one with index i + 1, otherwise the next instruction is the one with index s.

1. If the initial marking m 0 is not a success marking then label it as the root and tag it "new". 2. While "new" markings exist do the following: (a) Select a "new" marking m.

(b) If no transitions are enabled at m, return FALSE. (c) While there exist enabled transitions at m, do the following for each of them: i. Obtain a marking m ′ that results from firing the transition. ii. If on the path from the root to m there exists a marking m ′′ such that m ′ (p) ≥ m ′′ (p) for each place p then return FALSE. iii. If m ′ is not a success marking introduce m ′ as a node, draw an arc from m to m ′ , and tag m ′ "new". (d) Remove the tag "new" from the marking m. 3. Return TRUE.

Table2. An algorithm for checking the coverability of success markings.

Without loss of generality we assume that given a program I 1 , • • • , I n , it starts by executing I 1 with all the registers empty (i.e. all registers contain 0) and terminates trying to perform the first undefined instruction I n+1 .

In order to simplify the notation, in this section we introduce a notation corresponding to standard input and output prefixes of CCS [START_REF] Milner | Communication and concurrency[END_REF] 3 . Namely, we model simple synchronization as a request-response interaction in which there is only one possible reply message. Assuming that this unique reply message is ok (with ok ∈ Names not necessarily fresh), we introduce the following notation: a.P = invoke(a,ok.P) a.P = receive(a).reply(a,ok).P

In order to reduce RAM termination to client-service compliance, we define a client contract that simulates the execution of a RAM program, and a service contract that represent the registers, such that the client contract reaches the success √ if and only if the RAM program terminates.

Given a RAM program I 1 , • • • , I n , we consider the client contract C as follows

i∈{1,••• ,n} [[I i ]] | inst n+1 . √ [[I i ]] =        recX. inst i .inc j .ack.(inst i+1 | X) if I i = i : Inc(r j ) recX. inst i .dec j .(ack.(inst i+1 | X) + zero.(inst s | X)) if I i = i : DecJump(r j , s)
An increment instruction Inc(r j ) is modeled by a recursive contract that invokes the operation inc j , waits for an acknowledgement on ack, and then invokes the service corresponding to the subsequent instruction. On the contrary, a decrement instruction DecJump(r j , s) invokes the operation dec j and then waits on two possible operations: ack or zero. In the first case the service corresponding to the subsequent instruction with index i + 1 is invoked, while in the second case the service corresponding to the target of the jump is invoked instead. We now move to the modeling of the registers. Each register r j is represented by a contract representing the initially empty register in parallel with a service responsible to model every unit subsequently added to the register [[r j ]] = recX. dec j .zero.X + inc j .unit j .invoke(u j ,ok.ack.X) | recX.unit j . X | receive(u j ).ack.recY.(dec j .reply(u j ,ok)+ inc j .unit j .invoke(u j ,ok.ack.Y)) .

The idea of the encoding is to model numbers with chains of nested request-response interactions. When a register is incremented, a new instance of a contract is spawn invoking the operation unit j , and a request-response interaction is opened between the previous instance and the new one. In this way, the previous instance blocks waiting for the reply. When an active instance receives a request for decrement, it terminates by closing the request-response interaction with its previous instance, which is then reactivated. The contract that is initially active represents the empty register because it replies to decrement requests by performing an invocation on the zero operation. We extend structural congruence ≡, introduced in Section 3, to ≡ ren to admit the injective renaming of the operation name C ≡ ren D if there exists an injective renaming σ such that Cσ ≡ D Clearly, injective renaming preserves the operational semantics. Now, we introduce {{r j , c}} that we use to denote the modeling of the register r j when it holds the value c. Namely, {{r j , 0}} = [[r j ]], while if c > 0 then

{{r j , c}} =                           
b 0 ok .ack.recX.(dec j .zero.X + inc j .unit j .invoke(u j ,ok.ack.X)) | b 1 ok .ack.recY.(dec j .b 0 ok + inc j .unit j .invoke(u j ,ok.ack.Y)) | • • • | recY.(dec j .b c-1 ok + inc j .unit j .invoke(u j ,ok.ack.Y)) | recX.unit j . X | receive(u j ).ack.recY.(dec j .reply(u j ,ok)+ inc j .unit j .invoke(u j ,ok.ack.Y))

In the following theorem, stating the correctness of our encoding, we use the following notation: (i, c 1 , • • • , c m ) to denote the state of a RAM in which the next instruction to be executed is I i and the registers r As a corollary we get that client-service compliance is undecidable.

1 , • • • , r m respectively contain the values c 1 , • • • , c m , and (i, c 1 , • • • , c m ) → R (i ′ , c ′ 1 , • • • , c ′ m )

Conclusion

We have presented two models of contracts with bidirectional request-response interaction, studied a notion of compliance based on must testing and established an expressiveness gap between the two models showing that compliance is decidable in the first one while it is undecidable in the second one.

As for future work, we plan to investigate the (un)decidability of other definitions of compliance present in the literature. In fact, the must-testing approach -the one that we consider in this paper-has been adopted in early works about service compliance (see e.g. [START_REF] Carpineti | A Formal Account of Contracts for Web Services[END_REF]). More recent papers consider more sophisticated notions. For instance, the should-testing approach [START_REF] Rensink | Fair testing[END_REF] adopted, e.g., in [START_REF] Bravetti | Contract-Based Discovery and Composition of Web Services[END_REF] admits also infinite computations if in every reached state there is always at least one path leading to a success state. Other approaches require the successful completion of all the services in the system (see e.g. [START_REF] Bravetti | Towards a Unifying Theory for Choreography Conformance and Contract Compliance[END_REF][START_REF] Castagna | Contracts for Mobile Processes[END_REF]) in order to deal with multiparty service compositions in which there is no distinction between a client and a service.

Moreover, it would be interesting to apply the techniques presented in this paper to more sophisticated orchestration languages, like the recently proposed calculi based on the notion of session [START_REF] Boreale | SCC: A Service Centered Calculus[END_REF][START_REF] Boreale | Sessions and Pipelines for Structured Service Programming[END_REF]. For instance, in [START_REF] Acciai | Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday[END_REF], a type system is presented ensuring a client progress property -basically, absence of deadlock -in a calculus where interaction between (instances of) the client and the service is tightly controlled via session channels. It would be interesting to check to what extent the decidability techniques presented here apply to this notion of progress. Also connections with behavioural types [START_REF] Igarashi | A generic type system for the Pi-calculus[END_REF][START_REF] Acciai | Spatial and behavioural Types in the pi-calculus[END_REF] deserve attention. In the setting of process calculi, these types are meant to provide behavioural abstractions that are in general more tractable than the original process. In the present paper, the translation function of WSCL contracts into Petri nets can be seen too as a form of behavioural abstraction. In the case of tightly controlled interactions (sessions) [START_REF] Acciai | Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday[END_REF], BPP processes, a proper subset of Petri nets featuring no synchronization [START_REF] Esparza | Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes[END_REF], have been seen to be sufficient as abstractions. For general piprocesses, full CCS with restriction is in general needed. One would like to undertake a systematic study of how communication capabilities in the original language (unconstrained interaction vs. sessions vs. request-response vs....) trades off with tractability of the behavioural abstractions (CCS vs. BPP vs. Petri nets vs. ...).

Definition 5 (

 5 Petri net). A Petri net is a pair N = (S , T ), where S is the set of places and T ⊆ M f in (S ) × M f in (S ) is the set of transitions. A transition (c, p) is written c ⇒ p. A transition c ⇒ p is enabled at a marking m if c ⊆ m. The execution of the transition produces the marking m ′ = (m \ c) ⊕ p (where \ and ⊕ are the multiset difference and union operators). This is written as m[ m ′ . A dead marking is a marking in which no transition is enabled. A marked Petri net is a triple N(m 0 ) = (S , T, m 0 ), where (S , T ) is a Petri net and m 0 is the initial marking. A computation in N(m 0 ) leading to the marking m is a sequence m

Definition 6 (

 6 Pl(C)). For any contract C, let C (k) denote the term obtained by performing k unfolding of recursive definitions in C. Let k be the minimal s.t. in C (k) every recX.D is guarded by one of the following prefixes: invoke( • , • ), receive( • ), reply( • , • ), a b . Pl(C) is defined as follows:

  The function dec(•) transforms a WSCL contract C, as given in Definition 1, into a multiset m ∈ Pl(C). Definition 7 (Decomposition). The decomposition dec(C) of a WSCL contract C, as given in Definition 1, is dec C (C). The auxiliary function dec C (D) is defined below by lexicographic induction on the pair (n 1 , n 2 ), where n 1 is the number of unguarded (i.e. not under an invoke( • , • ), receive( • ), reply( • , • ), a b ) sub-terms of the form recX.D ′ in D and n 2 is the syntactic size of D. dec C ( i∈I r b i .

  l∈L c l .D l ) for some k ∈ I and there exists z ∈ L s.t. c z b j for every j ∈ J Table1. Transitions schemata for the Petri net semantics of WSCL contracts.

Example 2 .

 2 Consider the client C and the service S introduced in Example 1 and let C ′ △ = invoke(requireTicket, ok.C) +recreply(offerTicket, ok. √ ) S ′ △ = recreply requireTicket, ok.(invoke(offerTicket,ok)|S ) .

Proposition 1 .

 1 Let C and D be two contract systems such that C ≡ D. If C α -→ C ′ , then there exists D ′ such that D α -→ D ′ and C ′ ≡ D ′ .

  for some D and r such that r Names(D) and dec(D) = m ′ ; 3. if m = {c↓ j∈J b j .C j } ⊕ m ′ then c b j for each j ∈ J and C ≡ j∈J r b j .C j | r c | D, for some D and r such that r Names(D) and dec(D) = m ′ . Proposition 2. Let C be a WSCL contract. Consider the Petri net Net(C) = (S , T ) and a marking m of Net(C). We have that m is dead if and only if D has no outgoing reductions, for every D such that dec(D) = m.

Theorem 1 (

 1 Soundness). Let C be a WSCL contract. Consider the Petri net Net(C) = (S , T ) and let m be a marking of Net(C). If m[ m ′ then for each D such that dec(D) = m there exists a computation D △ = D 0 -→ D 1 -→ • • • -→ D l , with dec(D l ) = m ′ . Moreover, if m is not a success marking then there exists no j ∈ {0, • • • , l -1} such that D j √ -→.

  m[ m ′ by applying the second kind of transition then m = {a↑ j∈J b j .C j , i∈I G i }⊕ m ′′ , with G k = recreply(a, l∈L c l .D l ), for some k ∈ J, and b y = c z for some y ∈ J and z ∈ L. By Lemma 1, if dec(D) = m then D ≡ a r | j∈J r b j .C j | i∈I G i | C ′ , for any C ′ such that dec(C ′ ) = m ′′ . Therefore, by G k = recreply(a, l∈L c l .D l ):

3 .✷Definition 9 (

 39 Notice that each intermediate state in the reduction sequence from D to D ′ cannot perform a successful transition. If m[ m ′ by applying the third kind of transition then m = {a↑ j∈J b j .C j , i∈I G i } ⊕ m ′′ , with G k = recreply(a, l∈L c l .D l ), for some k ∈ J, and there is z ∈ L such that b y c z for each y ∈ J. By Lemma 1, if dec(D) = m then D ≡ a r | j∈J r b j .C j | i∈I G i | C ′ , for any C ′ such that dec(C ′ ) = m ′′ . Therefore, by G k = recreply(a, l∈L c l .D l ), we get D -→ j∈J r b j .C j | l∈L reply(r,c l ).D l | C ′ -→ j∈J r b j .C j | r c z | D z | C ′ △ = D ′ with dec(D ′ ) = {c z ↓ j∈J b j .C j } ⊕ dec(D z ) ⊕ m ′′ = m ′ .Notice that each intermediate state in the reduction sequence from D to D ′ cannot perform a successful transition. Stable contracts). A WSCL contract C (in the run-time syntax) is said stable if it contains neither unguarded reply(r,b) actions nor pairs of matching terms of the form r b and r b .

Proposition 4 .

 4 Let C and D be two contract systems such that C ≡ ren D. If C α -→ C ′ , then there exists D ′ and a label α ′ obtained by renaming the operation names in α such that D α ′ -→ D ′ and C ′ ≡ ren D ′ .

Theorem 4 .

 4 to denote the change of the state of the RAM R due to the execution of the instructionI i . Consider a RAM R with instructions I 1 , • • • , I n and registers r 1 , • • • , r m . Consider also a state (i, c 1 , • • • , c m ) of the RAM R and a corresponding contract C such that C ≡ ren inst i |[[I 1 ]]| • • • |[[I n ]]|inst n+1 . √ |{{r 1 , c 1 }}| • • • |{{r m , c m }}. We have that either the RAM computation has terminated, thus i = n + 1 or (i, c 1 , • • • , c m ) → R (i ′ , c ′ 1 , • • • , c ′ m ) and there exists l > 0 such that C -→ C 1 -→ • • • -→ C l and • C l ≡ ren inst i ′ |[[I 1 ]]| • • • |[[I n ]]|inst n+1 . √ |{{r 1 , c ′ 1 }}| • • • |{{r m , c ′ m }} • for each k (1 ≤ k < l): C k √ -→ /.

Corollary 2 .

 2 Consider a RAM R with instructions I1 , • • • , I n and registers r 1 , • • • , r m . Consider the client contract C = inst 1 |[[I 1 ]]| • • • |[[I n ]]|inst n+1 .√ and the service contract S = {{r 1 , 0}}| • • • |{{r m , 0}}. We have that C is compliant with S if and only if R terminates.

As discussed in Section 4, the languages that we propose are sufficiently expressive to model also the one-way communication pattern.

Other definitions of compliance, see e.g.[START_REF] Bravetti | Contract based Multi-party Service Composition[END_REF], resort to should-testing[START_REF] Rensink | Fair testing[END_REF] instead of musttesting: according to these alternative definitions C and S turn out to be compliant due to the fairness assumption characterizing the should-testing approach.

The input and output prefixes correspond also to the representation of the one-way interaction pattern in contract languages such as those in[START_REF] Carpineti | A Formal Account of Contracts for Web Services[END_REF][START_REF] Bravetti | Contract based Multi-party Service Composition[END_REF][START_REF] Castagna | A Theory of Contracts for Web Services[END_REF].

⋆ The third author is partly supported by the EU integrated projects HATS and is member of the joint INRIA/University of Bologna Research Team FOCUS.


Nadia Ambrosetti
email: nadia.ambrosetti@unimi.it

Wonder, Sorcery, and Technology: Contribute to the History of Medieval Robotics

Keywords: automata, design, sorcery, science, technology, feed-back control, history, magic, robot, robotics

The paper considers some Medieval sources about imagined or actually studied automata, to make a contribution to the reconstruction of the cultural landscape of a period that, from the technological point of view, is commonly regarded as less interesting than others. It will be shown that the idea of an automatic device or system, capable of performing not necessarily simple tasks, of measuring its own state and of taking action based on it, was well established in the Medieval mind, even though sometimes connected with magic.

Introduction

The Greek adjective αύτό ατος, coming from the adjectives αύτός (self) and ατός (having in mind, acting), was at first used to refer to any event, that happened spontaneously, without external intervention; later its use was extended to those mechanical devices, which perform, after a user's input, a finite number of default actions, typically, but not necessarily in a periodic sequence. Such automata were, during the Hellenism, also equipped with mechanisms for controlling their state and were so capable of taking action in dependence on the state itself (a first and essential mechanism for feedback). The purpose they were built for, was essentially playful: they were made to arouse the spectators' wonder (θαΰ α) and therefore their admiration not only for the engineer's skills, but also for the monarch, who had sponsored his designs and works. Often, these designers managed to surprise their audience through the implementation of devices activated by an input that doesn't appear to involve the produced effect: the typical example is the mechanism that opens the doors of a temple after the lighting of a ritual brazier. We rarely find examples of devices which also can have a practical use (such as a purifying water dispenser, or a pump to extinguish fires).

The most important source for this study are the works by Hero of Alexandria (1 st century AD): Πνευ ατική (Pneumatics) and Άυτο ατοποιητική (Automata building); these works came to us almost complete and they let us understand much of ancient engineering applied to automata. This fortunate tradition demonstrates that such works passed from Alexandria into the Romans' hands at first, then to the Byzantines and Arabs; during the Dark and Middle Ages they were read, understood, and copied, so that today, dispersed in many European libraries, we have respectively more than 100 copies in Greek language, and 13 translated into Latin [START_REF]Heronis opera quae supersunt omnia[END_REF]. Another well-known author of a treatise about Pneumatics is also Philo of Byzantium [START_REF]Philo of Byzantium, Pneumatica: the first treatise on experimental physics[END_REF][START_REF] Drachmann | Ktesibios, Philon and Heron: A Study in Ancient Pneumatics[END_REF]: his work, though less widespread than Hero's, was, however, read and studied during the Middle Ages and today we have 15 manuscripts of Latin translations, mostly entitled De spiritualibus ingeniis (About devices dealing with fluids).

2

The "Thauma Connection": from Alexandria to Baghdad, and Byzantium

When these works came into the hands of Arabic and Byzantine scholars, they were not only subject to a thorough theoretical study, but they also brought to the actual implementation of devices. While in the Byzantine empire no translation of these texts was required, in the 9 th century, Qusta ibn Luqa, author of many translations of scientific works from Greek into Arabic, provided Arabic scholars with a version of Hero's Mechanics.

The social structure of the Byzantine and the Arabic empires was fundamentally identical to the Alexandrian one: the king (emperor or caliph) was the undisputed arbiter of cultural life; for his impressive palace, wonderful automata were constructed for the double purpose of amusing the king and his court, and of arousing the admiration of the audience, mainly ambassadors of foreign peoples.

Arabic World

In the Arabic world, the most famous scholars in this field were the brothers Banu Musa, who lived in the 9 th century in Baghdad, and al-Jazari, who flourished between the 12 th and 13 th centuries [START_REF] Hill | The Book of Ingenious Devices: Kitáb al-Hiyal. By The Banú (sons of) Músà bin Shákir[END_REF][START_REF]The Book of Knowledge of Ingenious Mechanical Devices by Ibn al-Razzaz al-Jazari[END_REF]. Their works titles are all connected with the idea of surprising the audience, and their actual achievements were exactly in that direction, although by different paths: they tried to reproduce scenes of wildlife (birds singing on a tree), or men and women performing some actions (e.g., an orchestra of musicians playing a song on a boat floating in a pool of the royal garden; a drinkserving waitress). Some of these automata had however a practical purpose, such as a medical equipment, like the device for measuring the amount of blood drawn with the phlebotomy, or liturgical objects, such as a peacock-shaped basin for ritual ablutions.

Byzantine Empire

At the magnificent court of Byzantium, the natural heir of Hellenistic tradition, but also of the splendour of the Eastern world, automatic devices seem to have been exclusively used in the imperial Great Palace, in the Magnaura. Interestingly, in this case, the sources are not technical and no name of architect or engineer, that made automata in Byzantium, was handed down. The emperor Constantinus VII Porphyrogenitus (913-959) composed the Ἔκθεσις τῆς βασιλείου τάξεως (Ceremonies at the Imperial Court), a compilative work. The main content is a detailed description of the ceremonies from the court's point of view; in II,15, he relates what usually happened during a typical audience granted by the emperor: after the ritual bowing, the postulant heard a roar coming from the lions on either side of the throne, while birds, resting on the trees that surrounded the throne, began to sing harmoniously. Subsequently, the lions, in perfect synchrony with the various moments of the ceremony, departed from their starting position and then returned back to it; both lions and birds gave up singing at the end of the ceremony [START_REF]Constantini Porphyrogeniti Imperatoris De Ceremoniis Aulae Byzantinae[END_REF][START_REF] Lewis | Antique Engineering in the Byzantine World[END_REF].

A very similar ritual is also described by the bishop Liutprand of Cremona (920-972), in his Antapodosis, a report about his stay at the court of Byzantium as an ambassador of Berengarius II (900-966), who was eager to be accredited as king of Italy by the emperor of the Eastern Roman Empire; Liutprand was formally received by Constantinus Porphyrogenitus, in 949, and stayed for some time in the city, taking part in court ceremonies [START_REF] Ravegnani | L'ambasceria di Liutprando di Cremona alla corte di Costantino Porfirogenito e il Libro delle cerimonie[END_REF][START_REF]Rerum Italicarum Scriptores. Vol. II, caput II. ex typographia Petri Cajetani Viviani[END_REF].

The presence of a tree near a king's throne [START_REF] Jacobsthal | Ornamente Griechischer Vasen -Aufnahmen, Beschreibungen und Untersuchungen[END_REF] dates back to the Sumeric epic of Gilgamesh; a golden plate tree and a golden vine are also cited in Herodotus' Histories (VII, 27), as a gift to the Persian emperor Darius by the king of Lydia, Pythius, grandson of the renown Croesus [START_REF] Briant | Histoire de l'Empire perse[END_REF][START_REF] Herodote | Histoires. Tome VII : Livre VII : Polymnie[END_REF]. Singing birds are likely to have been inspired by Hero's and Philo's Pneumatics (respectively, I, 4; I, 5; I, 16; and 61, for instance), exactly as it had happened in the Arabic world, but, given such lack of technical Byzantine sources, one could also suppose that the Byzantine engineers were inspired by Arabic designs or models possibly seen in Baghdad. The reference to such a device by the Sicilian poet Ibn Hamdis, who lived during the 11 th century, could support the hypothesis of the spreading of such automaton design [START_REF]Poeti arabi di Sicilia. Edi.bi.si[END_REF].

Concerning the lions, an iconographic source for the Byzantine engineers could have been the throne of Solomon, as described in the Bible (Kings, I, x, 18-20), though no reference is here made to any motion.

These automata show perfectly how the intellectual resources of the Byzantines (in this case, their competence in the fields of mechanical engineering) could be used as instrumentum regni, and they also demonstrate the effort that was made both in the imitation of nature, and in showing the emperor as a God's epiphany.

Automata descriptions within the Byzantine Empire are also present in many literary works written in order to entertain the audience: romances, and allegorical poems [START_REF] Trapp | Learned and Vernacular Literature in Byzantium: Dichotomy or Symbiosis?[END_REF].

Dark and Middle Ages

After the great season of Hellenistic engineering and during all the early medieval centuries in the Eastern Roman Empire or in the territories under Arabic domination, the sources related to automata decrease dramatically and are limited in Europe to secondary references, and to romances. No designs or technical descriptions are available, at least until the 13 th century.

Dark Ages

Anyway, secondary sources can testify the existence of mechanical precision devices, demonstrating that even in Roman-barbarian kingdoms the technical skills required for such objects were not completely lost. For instance, in Cassiodorus' Variae, the official correspondence of the Ostrogothic court in Ravenna, a letter (XLV, 6) addressed to the philosopher Boethius is preserved; Theodoric says that the Burgundian king has repeatedly asked him for a water clock and for craftsmen (probably as maintenance men); he comments the episode with revealing words: the reason why the Burgundian king insisted so much, is that he considers as a "miraculum" (wonder) an object that for Theodoric is instead "cottidianum" (daily) [START_REF]Cassiodori senatoris Variae. apud Weidmannos[END_REF].

Although we can suppose that Theodoric overemphasized his acquaintance with these devices, it is clear that at the beginning of the 7 th century in Europe there were still craftsmen capable of building a water clock.

Middle Ages

Another important secondary source consists in romances [START_REF] Bruce | Human Automata in Classical Tradition and Mediaeval Romance[END_REF]: whether they belong to the Matter of Britain (King Arthur's stories) or of France (Charles the Great's stories), or of Rome (the main character is taken from ancient history, such as Julius Caesar or Alexander the Great), references to automata are frequent; they are primarily used as guardians of a strategic place (a tomb, a bridge, a cave, or a castle) and their makers are usually magicians, not technicians. The reason is easily explained: all mechanical arts were in no esteem throughout the Middle Ages to the point that, for a cultured man, technical practice was considered morally, religiously, and socially dishonorable [START_REF] White | Medieval Engineering and the Sociology of Knowledge[END_REF]. On the contrary, knowledge and practice of magic were reserved for a selected group of people, who had chosen to engage in "religiously illicit pursuits, illegitimate knowledge, and trafficking with the Devil" [START_REF] Truitt | Trei poëte, sages dotors, qui mout sorent di nigromance": Knowledge and Automata in Twelfth-Century French Literature[END_REF]; by attributing the construction of automata to magicians, any moral conflict was avoided.

Even the legends about the French monk Gerbert d'Aurillac (946-1003), later Pope Sylvester II, and the Dominican philosopher Albertus Magnus (1206-1280) as automata builders, reveal an explicit moral intent: both episodes end with the destruction of the automaton (Albertus' talking head would have been broken by one of his students, St. Thomas Aquinas), which is moreover impossible to restore.

The Great Sorcerer Gerbert d'Aurillac?

In Gerbert's biography by William of Malmesbury (1080/1095-1143), an interesting event is reported [START_REF]William of Malmesbury's Chronicle of the Kings of England[END_REF][START_REF]William of Malmesbury De gestis regum Anglorum libri quinque[END_REF]. During his stay in Rome, the future pope had decided (by sheer greed) to rescue Octavian's treasure, buried, according to a legend, in a cave beneath the Roman Forum; the cave entrance was indicated by a statue. Many others had unsuccessfully tried to find the entrance, being less artful than him: he marked the place, where the shadow of a statue's finger fell at noon-day; at night he made the earth open by means of his magical arts and, attended by a servant with a lantern, he entered a beautiful golden palace, where they found a court of golden automata. The light source was a small carbuncle of the first quality, standing on a base. At the opposite corner of the room, stood a young archer, holding a bow and an arrow. Gerbert and his servant soon noticed that, if they tried to take anything, all these automata appeared to rush forward to attack them. So Gerbert guessed what would be the consequences of such an attempt, and decided to give up, but his servant, unable to resist, decided to steal a superb knife. Immediately, the automata cried loudly and began moving, and the archer shot the carbuncle with his arrow, so that all was in darkness; Gerbert ordered his servant to drop the knife, otherwise their lives would have been in danger. He obeyed, and they left the palace, though without any treasure.

The story is very interesting from several points of view. First of all, the palace designer had planned the system in order to kill any thieves or at least to give them a moral lesson, not to impress them with the automata's capabilities. We have the description of an actual distributed system made up of automata: they are all running the same task (stop the intruders, if they are stealing something). The actions performed by the automata are not periodical: they begin and end depending on values measured by "sensors". Nothing is said about how the system reverts to its initial state after the departure of the intruders.

Then, in Hero's Pneumatics (I, 41), an automaton composed by two figures, entitled Hercules and the Snake, is described: when a user lifts an apple (placed between the statue of the archer Hercules and the tree the snake is wrapped around) Hercules shoots with an arrow the snake, which in the meanwhile begins to hiss. Its operation is relatively simple: the base of the group is divided horizontally into two parts (the top compartment is full of water), connected by a drain hole, where a cork is set. By raising the apple, a double synchronous effect is produced:

1. a chain, connected to the apple, pulls the cork from the hole, causing the gurgling through the various ducts that is similar to a snake hiss; 2. a second chain, also connected to the apple, acts on the figure of Hercules, making him stretch and release the string of his bow. In addition, in a French romance, whose first written version dates to the middle of the 12 th century, entitled Le pèlerinage de Charlemagne (Charles the Great's Pilgrimage), the setting of the emperor's main adventure is the vaulted and circular palace of Hugon, emperor of Constantinople, where Charles and his 12 peers are housed as guests in a beautiful bed-chamber, full of precious decorations and refined objects. The light source is a carbuncle, set on a pillar [START_REF] Legrand | Bibliothèque grecque vulgaire[END_REF]. The front of the palace is decorated with the statues of two smiling young men, holding ivory horns. Whenever a wind comes up, these images blow their horns, producing a loud clear sound, and immediately the palace begins rotating. A carbuncle and a moving room appear also in the 14 th -century allegorical poem titled Σοφροσύνη (Temperance) by Theodore Meliteniotes [START_REF] Miller | Poème allégorique de Meliténiote[END_REF]. Here we also find an abridged version of a lapidary, a book where stones are put in relation with moral qualities: the carbuncle is a symbol for temperance, a cardinal virtue, related to self-control.

Last, but not least, remark: Gerbert is told to have designed and built a water organ, during his stay in Reims; his treatise on the subject has been recently studied [START_REF] Flusche | The Life and Legend of Gerbert of Aurillac: The Organbuilder Who Became Pope Sylvester II[END_REF].

Even taking into consideration that this is a legendary episode, one cannot but be struck by the strong similarity between this system and the Heronian automaton, which may have been the remote source of the story, though it was considered neither in the Arabic written tradition nor in the Byzantine implementations.

It is therefore reasonable to make two assumptions, not mutually exclusive: 1. this knowledge was transmitted within the workshops by the masters to their apprentices from the Antiquity to the Middle Ages with or without Arabic contribution; it is unfortunately very hard to prove such an assumption, due to the lack of sources. 2. a Latin cultured tradition, mostly separated from the Arabic one, existed, and flourished, probably in the monasteries; this second assumption could be easier to prove, by means of a census of Latin manuscripts on the subject.

Looking for Pneumatics' Medieval Latin Tradition

Despite the wide diffusion of Arabic culture and technology, that had accompanied the territorial expansion of the 7 th -15 th centuries, at the time neither the Latin versions of Arabic engineers' masterpieces, nor information in this regard are available, since the lists of the translations carried out in Europe don't include these works. We may assume that the oldest (so far as it is known at the moment) Latin translation of Philo's Pneumatics (Cambridge, Pembroke College, 169) has been made from an Arabic translation: its incipit "In nomine Dei pii <et> misericordis…" is common to other Latin translations of Arabic scientific works (e.g., Robert of Chester's version of al-Khwarizmi's al-jabr w'al-muqabalah, or Iohannes Hispalensis' De scientia astrolabii) [START_REF] Van Egmond | Practical Mathematics in the Italian Renaissance: A catalogue of Italian Abbacus Manuscripts and Printed Books to 1600[END_REF][START_REF] Ambrosetti | L'eredità arabo-islamica nelle scienze e nelle arti del calcolo dell'Europa medievale[END_REF].

It is equally unlikely that Byzantine technical works existed, since in European libraries no Greek manuscripts are housed dating before the 15 th century. Even the oldest copy of Hero's Pneumatics (Venezia, Biblioteca Marciana, gr. 516) dates back to the 13 th century, but it was brought to Italy from Byzantium by Cardinal Bessarion during the 15 th century.

Another part of Europe where an intense activity of translation took place, was the Norman Sicily [START_REF] Houben | Roger II. von Sizilien. Herrscher zwischen Orient und Okzident[END_REF]: Greek, and Arabic works were translated into Latin [START_REF] Setton | The Byzantine Background to the Italian Renaissance[END_REF]. One of the most renowned translators in the 12 th century was the archdeacon of Catania, Henricus Aristippus, whose origins and life are still largely unknown. He translated from Greek into Latin Diogenes Laertius' works, Ptolemy's Almagest, Plato's Meno and Phaedo, Aristotle's Meteorologica. In his preface to the translation of the Phaedo, he addresses to an Englishman who was to return home from Sicily, using the following words: " […] Habes Heroni philosophi Mechanica pre manibus, qui tam subtiliter de inani disputat […] " (you have in your hands the Mechanics by Hero, who so subtly deals with the void). These words led Rose and Birkenmajer [START_REF] Rose | Die Lücke im Diogenes Laertius und der alten Übersetzer[END_REF][START_REF] Birkenmajer | Vermischte Untersuchungen zur Geschichte der mittelalterlichen Philosophie[END_REF] to believe that it was the Pneumatics, since in the Mechanics Hero doesn't speak of void; Haskins [START_REF] Haskins | Further Notes on Sicilian Translations of the Twelfth Century[END_REF][START_REF] Haskins | Studies in the History of Medieval Science[END_REF][START_REF] Haskins | The Sicilian Translators of the Twelfth Century and the First Latin Version of Ptolemy's Almagest[END_REF] refused such an inference, because the content of Mechanics is known only from Arabic translations, possibly incomplete; moreover, Haskins rejected the subsequent inference by the above mentioned scholars as a risky assumption: according to them, Henricus was referring to his own Latin translation, since other translations of his are quoted in the passage.

Birkenmajer [START_REF] Birkenmajer | La Bibliothèque de Richard de Fournival[END_REF] goes further than Rose, stating that he had found evidence of a copy of this translation in the Biblionomia (the library catalogue of the French philosopher and poet Richard de Fournival, living in the 13 th century), where the Pneumatics would be referred to as Excerpta de libro Heronis de specialibus ingeniis (excerpts from Hero's book about special devices); "specialibus" is probably a wrong transcription of "spiritualibus" (concerning with void), due to the fact that the shortening of the two words is identical. Unfortunately, though the library is now part of the Bibliothèque Nationale de France, no evidence of the manuscript is now available, and even the assumptions that it could be Philo's instead of Hero's Pneumatics, or a Latin translation of an Arabic compilation from Banu Musa's work, can be neither validated nor rejected [START_REF] Grant | Henricus Aristippus, William of Moerbeke and Two Alleged Mediaeval Translations of Hero's Pneumatica[END_REF].

Birkenmajer also argues that, in the 13 th century, the Flemish Dominican William of Moerbecke would have translated, among many other works, Hero's Pneumatics into Latin; his proof is based on the presence of a treatise entitled De aquarum conductibus et ingeniis erigendis in a list of works, owned by St.Thomas, actually translated by the Flemish scholar [START_REF] Birkenmajer | Vermischte Untersuchungen zur Geschichte der mittelalterlichen Philosophie[END_REF]. Although the evidence is not completely convincing, it is remarkable that the Aquinas, already present in the legend about Albertus Magnus' automaton as a minor character, returns as a possible reader of a Hero's text.

Another work, entitled De inani et vacuo (About void), is both quoted without any reference to the author by the 14 th -century philosopher Marsilius of Inghen in his Quaestiones super VIII physicorum libros (Questions on the Eight Books of the Physics; IV, 13), and copied in 1466 in a manuscript (Krakow, Biblioteka Jagiellonska, MS 568, ff. 207-211), where it is attributed to Hero. The Polish manuscript has two interesting issues:

• in the colophon the scribe's name of the antigraph is mentioned (quem inscripsit Landfridus); such a name (in the German version Lantfrid) is present also in the colophon of a Carolingian manuscript (München, Bayerische Staatsbibliothek, Clm. 14461, f.150) of religious content, copied in the 820s in Freising, and housed in St.Emmeram's abbey library, near Regensburg, at least since 1347. If the scribe would be the same, we would have an evidence of the connection between a Pneumatics tradition in Latin language and a Benedictine monastery, a place quite advanced from the technological point of view during the Middle Ages; • the handwriting is very similar to Regiomontanus', the famous German astronomer and mathematician; in addition, we must say that the manuscript was bound in Germany, and the author of the letters included in the last part of the manuscript was a friend of Regiomontanus': Cristianus Roder de Hamburgo. Regiomontanus is said by the French humanist Pierre de la Ramée to have built an eagle, and a fly, that could fly away and back.

Despite the fact that the story told by Pierre is certainly exaggerated, the fact that Regiomontanus may have dealt with an abridged version of Pneumatics, makes it less improbable. Though there is no definitive proof of direct knowledge of Pneumatics during the Middle Ages, we, however, have 28 copies of Latin translations from Philo's or Hero's treatises made in the 14 th -15 th century. Based on a comparison of the incipits, they can be grouped into at very least 3 families:

• Quum/Cum apud antiquos: 12 manuscripts.

• Quoniam tuum, where the incipit mentioned above (In nomine Dei ...) is often, but not always, placed before: 15 manuscripts. • Cum spirituale negocium: 1 manuscript.

A deep comparative study of all these manuscripts is in progress.

A Useful Mechanical Automaton called Maurizio

Concerning craft tradition, we can remark that more or less in the same years one of the oldest mechanical automata appeared in Italy, in Orvieto. In 1347 the Opera del Duomo (Committee on the cathedral works) charged the clockmaker Francesco with building a clock mechanism, which required 285 pounds of iron, three blacksmiths, and eight craftsmen. The following year a bronze automaton was added to the clock as a striking system; it represents a "dottiere", a yard overseer, who was in charge of verifying compliance with working hours, and of forbidding workers to waste time. This is one of the rarest, and oldest, instances of automata (before the Renaissance), due inter alia to a virtually unknown clockmaker. In addition, this is clearly a device which was rather designed for practical purposes than to impress an audience: the automaton had become so familiar to the citizens of Orvieto, and to the yard workers, that it was even given a name: Maurizio (distortion of the word "muricçio", that indicates the yard).

Conclusions

As it is clear from the above, the Medieval landscape is fragmented and often uncertain, and it must be frequently reconstructed upon secondary sources, such as literary texts, or hearsay. All sources and cross references need to be verified by means of careful philological and/or historical work.

In addition, such a thorough collection of sources would be useful only for documentary purposes, and would make it impossible to fully understand similarities and differences in implementation among automata designed in different ages. To solve this problem and not to reduce their works to a mere display of erudition, some scholars [START_REF] Bruce | Human Automata in Classical Tradition and Mediaeval Romance[END_REF][START_REF] Truitt | Trei poëte, sages dotors, qui mout sorent di nigromance": Knowledge and Automata in Twelfth-Century French Literature[END_REF][START_REF] Pugliara | Il mirabile e l'artificio: creature animate e semoventi nel mito e nella tecnica degli antichi[END_REF][START_REF] Söhring | Werke bildender Kunst in altfranzösischen Epen[END_REF][START_REF] Faral | Le merveilleux et ses sources dans les descriptions des romans français du XIIe siècle[END_REF] have already attempted a classification of automata, based upon different features: their being connected with musical devices, rather than standalone; their being human figures rather than objects, or animals; the role they play in the story, as guardians, or entertainers; the finesse of their movements. These classifications, though useful, cannot, however, fully capture the variety of behavior of automata in the same class, or any similarities in behavior among automata belonging to different classes. Consequently, it may be useful to introduce a different approach, based on a standard, language-independent representation of the automata's behavior.

To this purpose, at an advanced stage of sources' collection, it would be useful to make a modeling of the automata's behavior with UML diagrams; we believe that the diagram that can better represent the temporal sequence of actions and interaction between user and any automaton or system of automata is the sequence diagram. An example of this representation is given below, in relation to the above narrated episode of Gerbert d'Aurillac.

The next research step will therefore be to implement a database in which diagrams, similar to the above, will be added to quotations from the corresponding passages of literary and/or technical works, in order to allow abstraction and analysis of persistent archetypal elements, such as ideas and designs.

Fig. 1 :

 1 Fig. 1: UML sequence diagram of the episode of Gerbert d'Aurillac and Octavian's palace, from William of Malmesbury's biography.