# A Game Interpretation of Retractable Contracts

Franco Barbanera, Ugo De' Liguoro

► To cite this version:

Franco Barbanera, Ugo De' Liguoro. A Game Interpretation of Retractable Contracts. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. pp.18-34, 10.1007/978-3-319-39519-7_2. hal-01631714

HAL Id: hal-01631714

https://inria.hal.science/hal-01631714

Submitted on 9 Nov 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
A game interpretation of retractable contracts*

Franco Barbanera¹ and Ugo de' Liguoro²

¹ Dipartimento di Matematica e Informatica, University of Catania
barba@dmi.unict.it

² Dipartimento di Informatica, University of Torino
ugo.deliguoro@unito.it

**Abstract.** In the setting of contract theory, retractable contracts have been defined to formalize binary session protocols where the partners can go back to certain particular synchronization points when the session gets stuck, looking for a successful state, if any.

In the present paper we propose a three-party game-theoretic interpretation of client/server systems of retractable contracts. In particular, we show that a client is retractable-compliant with a server if and only if there exists a winning strategy for a particular player in a game-theoretic model of contracts. Such a player can be looked at as a *mediator*, driving the choices in the retractable points. We show that winning strategies for the mediator player correspond to orchestrators in a system of orchestrated client/server sessions, and vice versa.

The notion of *contract* has been proposed as an abstraction to formally specify and check the behaviour of software systems, and especially of web services. In particular, in the setting of service-oriented architectures the concept of agreement, often called *compliance*, is of paramount importance while searching components and ensuring that they will properly collaborate with each other. The main challenge is that compliance has to meet the contrasting requirements of guaranteeing correctness of interactions w.r.t. certain safety and liveness conditions, while remaining coarse enough to maximize the possibilities of finding compliant components in a library or services through the web.

The main conceptual tool to face the issue is that of relaxing the constraint of a perfect correspondence among contracts through *contract refinement*, also called sub-contract [9,8] and sub-behaviour [3] relations, that is pre-order relations such that processes conforming to more demanding contracts (which are lower in the pre-order) can be safely substituted in contexts allowing more permissive ones. Indeed contract refinement closely resembles subtyping, as it is apparent in the case of session types [10,3], and it is related to (but doesn't coincide with) observational pre-orders and *must-testing* in process algebra [11,6].

However, since the first contributions to the theory of contracts [9], a rather different approach has been followed, based on the idea of filtering out certain actions that, although unmatched on both sides of a binary interaction, can be

<footnote>* This work was partially supported by the COST Action IC1405 of the European Union and by the Project FIR 1B8C1 of the University of Catania.</footnote>
neglected or prevented by the action of a mediating process called the *orchestra-tor* [14,13], without compromising the reaching of the goals of the participants, like the satisfaction of all client requests in a client-server architecture.

An alternative route for the same purpose is to change the semantics of
contracts so that interacting processes can adapt each other by means of a roll-
back mechanism: these are the *retractable contracts* proposed in [4]. Although
compliance can be decided in advance, interaction among processes exposing re-
tractable contracts undergoes a sequence of failures and backtracks that might
be avoided by extracting information from the compliance check.

The contribution of the present paper is to show that the two approaches
of orchestrated and retractable compliance are indeed equivalent, at least in the
case of *session contracts* (see [2,3], where they are dubbed “session behaviours”),
which are contracts that limit the non-determinism by constraining both external
and internal choices to a more regular form. More precisely, we consider contracts
that are syntactically the same as retractable ones, but instead of adding rollback
to the usual contract semantics, we abstractly define outputs in an external
choice as *affectible* actions: their actual sent can be influenced by the partner
in a binary session or by some entity external to the system. Affectible actions
correspond to retractable actions in [4].

The essence of the construction is that (an appropriate restriction of) or-
chestrators correspond to winning strategies in certain concurrent games that
naturally model retractable contracts. In [5] the theory of contracts has been
grounded on games over event structures among multiple players; applying this
framework to retractable contracts, the interaction among a client and a server
can be seen as a play in a three-party game. Player A moves according to the
unaffectible actions of the client; player B moves according to the unaffectible
actions of the server, whereas moves by player C correspond to affectible ac-
tions on both sides, namely the retractable agreement points of the system. The
client ρ is hence affectible-compliant with the server σ whenever C has a win-
ning strategy in the game with players A and B, where player C wins when she
succeeds to lead the system ρ||σ to a successful state (the client terminates) or
the interaction proceeds indefinitely without deadlocking.

The payoff of the game theoretic interpretation is that there is a precise
correspondence between winning strategies for player C and elements of a class
of orchestrators in the sense of [14]. Such a correspondence is of interest on
its own, since strategies are abstract entities while orchestrators are terms of
a process algebra and concrete witnesses of the agreement among participants
of a session. Moreover, we can decide whether a client-server pair is reversible-
compliant by means of an algorithm that synthesizes an orchestrator if any, or
reports failure.

# 1 Affectible contracts and retractable compliance

*Affectible session contracts* (affectible contracts for short) are a variant of *re-
tractable contracts* in [4]; they are syntactically the same, but affectible session
contracts have a different, and more abstract semantics. Nonetheless compliance coincides in both settings as we show in this section.

**Definition 1 (Affectible session contracts).** Let $\mathcal{N}$ (set of names) be some countable set of symbols and let $\overline{\mathcal{N}} = \{\bar{a} \mid a \in \mathcal{N}\}$ (set of conames), with $\mathcal{N} \cap \overline{\mathcal{N}} = \emptyset$. The set $\mathcal{ASC}$ of affectible session contracts is defined as the set of the closed (with respect to the binder $\text{rec}$) expressions generated by the following

$$
\begin{array}{lcl}
\sigma, \rho := & \mathbf{1} & \text{success} \\
& \sum_{i \in I} a_i \cdot \sigma_i & \text{input} \\
& \sum_{i \in I} \bar{a}_i \cdot \sigma_i & \text{affectible output} \\
& \bigoplus_{i \in I} \bar{a}_i \cdot \sigma_i & \text{unaffectible output} \\
& x & \text{variable} \\
& \text{rec } x \cdot \sigma & \text{recursion}
\end{array}
$$

where *I* is non-empty and *finite*, the names and the conames in choices are pairwise distinct and *σ* is not a variable in *rec x.σ*.

Affectible as well as retractable contracts stem from session behaviours of [3] also called session contracts in [6]. With respect to session behaviors, affectible contracts add the affectible output construct, which is called retractable output in [4]. The affectible output represents points where the client-server interaction can be influenced by the partner process, or can be guided by a third party; consequently they are represented by the CCS external choice operator as it is the case of the input branching (which is always affectible). Outputs in an internal choice are regarded as unaffectible actions and treated as unretractable in the setting of retractable contracts. The transitions representing an internal choice have no label; note that any $\bigoplus_{i \in I} \bar{a}_i \cdot \sigma_i$ just reduces to one of its summands. In the following we consider recursion up-to unfolding, that is we equate $\text{rec } x \cdot \sigma$ with $\sigma\{x/\text{rec } x \cdot \sigma\}$. The symbol $\alpha$ will be used as a variable ranging over $\mathcal{N} \cup \overline{\mathcal{N}}$.

**Definition 2 (LTS for ASC).** Let $\mathbf{Act} = \mathcal{N} \cup \overline{\mathcal{N}} \cup \{\bar{a}^+ \mid \bar{a} \in \overline{\mathcal{N}}\}$.

$$ (+) \quad a.\sigma + \sigma' \xrightarrow{a} \sigma \qquad (\oplus) \quad \bar{a}.\sigma + \sigma' \xrightarrow{\bar{a}^+} \sigma $$

$$ (\oplus) \quad \bar{a} \cdot \sigma \oplus \sigma' \rightarrow \bar{a} \cdot \sigma \qquad (\alpha) \qquad \alpha \cdot \sigma \xrightarrow{\alpha} \sigma $$

A client/server system (system for short) is a pair of contracts in $\mathbf{ASC}$ that we denote by $\rho \parallel \sigma$.

**Definition 3 (LTS for systems).** Let $\mathbf{csAct} = \{+, \tau\}$.

$$
\begin{array}{c}
\displaystyle \frac{\rho \to \rho'}{\rho \parallel \sigma \to \rho' \parallel \sigma} \\[2ex]
\displaystyle \frac{\rho \xrightarrow{a} \rho' \qquad \sigma \xrightarrow{\bar{a}^+} \sigma'}{\rho \parallel \sigma \xrightarrow{+} \rho' \parallel \sigma'} \\[2ex]
\displaystyle \frac{\rho \xrightarrow{\bar{a}^+} \rho' \qquad \sigma \xrightarrow{a} \sigma'}{\rho \parallel \sigma \xrightarrow{+} \rho' \parallel \sigma'} \\[2ex]
\displaystyle \frac{\rho \xrightarrow{\alpha} \rho' \qquad \sigma \xrightarrow{\bar{a}} \sigma'}{\rho \parallel \sigma \xrightarrow{\tau} \rho' \parallel \sigma'}
\end{array}
$$
We define $\Rightarrow = \to^* \circ \xrightarrow{\tau}$ and $\xrightarrow{\pm} = \to^* \circ \xrightarrow{\pm}$. In the last rule, $\bar{\alpha}$ is the CCS involution of names and co-names.

The semantics of $\rho \parallel \sigma$ is reminiscent of CCS parallel composition as used to define testing preorders in [12], but for the usage of the labels $+$ and $\tau$ and for the absence of a success marker (there is a set of success states instead: see below). We use labels $+$ and $\tau$ to distinguish among affectible and unaffectible communications respectively, although they are both unobservable as the only observable facts are termination and the resulting state.

**Lemma 1.** Let $\rho, \sigma \in \mathbf{ASC}$. $\rho \parallel \sigma \Rightarrow$ and $\rho \parallel \sigma \xrightarrow{\pm} \Rightarrow$ can never both occur.

The affectible compliance relation can be now coinductively defined as follows.

**Definition 4 (Affectible Compliance Relation $\neg\neg^A$).**

i) Let $\mathcal{H}: \mathcal{P}(\mathbf{ASC} \times \mathbf{ASC}) \to \mathcal{P}(\mathbf{ASC} \times \mathbf{ASC})$ be such that, for any $\mathcal{R} \subseteq \mathbf{ASC} \times \mathbf{ASC}$, we get $(\rho, \sigma) \in \mathcal{H}(\mathcal{R})$ if the following conditions hold:

1) $[ \rho \parallel \sigma \Leftrightarrow \text{ and } \rho \parallel \sigma \Leftrightarrow ]$ implies $\rho = \mathbf{1}$;

2) $\forall \rho', \sigma'. [ \rho \parallel \sigma \Rightarrow \rho' \parallel \sigma' \text{ implies } \rho' \mathcal{R} \sigma' ]$;

3) $\rho \parallel \sigma \Leftrightarrow \text{ implies } \exists \rho', \sigma'. [ \rho \parallel \sigma \Rightarrow \rho' \parallel \sigma' \text{ and } \rho' \mathcal{R} \sigma' ]$.

ii) A relation $\mathcal{R} \subseteq \mathbf{ASC} \times \mathbf{ASC}$ is an affectible compliance relation if $\mathcal{R} \subseteq \mathcal{H}(\mathcal{R})$. $\neg\neg^A$ is the greatest solution of the equation $X = \mathcal{H}(X)$, that is $\neg\neg^A = \nu\mathcal{H}$.

In words the client $\rho$ is affectible-compliant with the server $\sigma$ if either $\rho$ and $\sigma$ cannot communicate because $\rho = \mathbf{1}$, namely all client requirements have been satisfied; or all unaffectible communications of the system $\rho \parallel \sigma$ lead to compliant systems; or there exists an affectible communication leading to a compliant system. By Lemma 1 the last two conditions cannot be simultaneously satisfied.

Because of conditions i2) and i3), the affectible compliance relation is an abstract concept; but it can be made concrete via the characterization in terms of retractable computations, provided in section 1.

Let us consider the following example from [4]. A Buyer is looking for a bag (bag) or a belt (belt); she will decide how to pay, either by credit card (card) or by cash (cash), after knowing the price from the Seller.

$$ \text{Buyer} = \overline{\text{bag.price.}}(\text{card} \oplus \text{cash}) + \overline{\text{belt.price.}}(\text{card} \oplus \text{cash}) $$

The Seller does not accept credit card payments for items of low price, like belts, but only for more expensive ones, like bags:

$$ \text{Seller} = \overline{\text{belt.price.cash}} + \overline{\text{bag.price.}}(\text{card} + \text{cash}) $$

From the previous definition it is not difficult to check that Buyer $\neg\neg^A$ Seller.

**Retractable contracts.** Let us recall the formalism of retractable contracts; the following definitions and Theorem 1 below are from [4]. As said before, retractable and affectible contracts are syntactically the same, but the operational semantics of the formers is based on a rollback operation, acting on the recording of certain discarded branches of an interaction. The notion of contracts with histories is defined as follows:
**Definition 5 (Contracts with histories).** Let Histories be the set of expressions (referred to also as stacks) generated by the grammar:

$$ \gamma ::= [] | \gamma : \sigma \quad \text{where } \sigma \in \mathbf{ASC} \cup \{\circ\}. $$

Then the set of contracts with histories is defined by:

$$ \text{RCH} = \{ \gamma \prec \sigma \mid \gamma \in \text{Histories}, \sigma \in \mathbf{ASC} \cup \{\circ\} \}. $$

Histories are finite lists of contracts representing the branches which have been discarded because of a retractable synchronization action. The effect of retracting such an action is modeled by restoring the last contract on the history as the actual contract and by trying a different branch, if any. This is formalised by the operational semantics of contracts with histories that is defined as follows.

**Definition 6 (LTS of Contracts with Histories).**

$$ (+) \quad \gamma \prec \alpha.\sigma + \sigma' \xrightarrow{\alpha} \gamma : \sigma' \prec \sigma $$

$$ (\alpha) \quad \gamma \prec \alpha.\sigma \xrightarrow{\alpha} \gamma : \circ \prec \sigma $$

$$ (\oplus) \quad \gamma \prec \bar{a}.\sigma \oplus \sigma' \xrightarrow{\tau} \gamma \prec \bar{a}.\sigma $$

$$ (\text{rb}) \quad \gamma : \sigma' \prec \sigma \xrightarrow{\text{rb}} \gamma \prec \sigma' $$

When selecting a branch of an external choice, the discarded branches are memorised on top of the new stack (the last contract of the history) in the right-hand side of rule (+); on the contrary, when an internal choice occurs, the stack remains unchanged in rule (⊕). When a single action is executed, the history is modified by adding a ‘o’, meaning that the only available branch has been tried and no alternative is left. Rule (rb) recovers the contract on the top of the stack (if the stack is different than [] ) by replacing the current one with it. Note that the combined effect of rules (⊕) and (α) is that the alternative branches of an internal choice are unrecoverable.

The interaction of a client with a server is modeled by the reduction of their parallel composition, that can be either forward, consisting of CCS style synchronisations and single internal choices, or backward if there is no possible forward reduction, the client is different than 1 (the fulfilled contract) and rule (rb) is applicable on both sides.

**Definition 7 (TS of Client/Server Pairs).** We define the relation $\rightarrow$ over pairs of retractable contracts with histories by the following rules:

$$ \frac{\delta \prec \rho \xrightarrow{\alpha} \delta' \prec \rho' \quad \gamma \prec \sigma \xrightarrow{\bar{\alpha}} \gamma' \prec \sigma'}{\delta \prec \rho \parallel \gamma \prec \sigma \rightarrow \delta' \prec \rho' \parallel \gamma' \prec \sigma'} \quad \text{(comm)} $$

$$ \frac{\delta \prec \rho \xrightarrow{\tau} \delta \prec \rho'}{\delta \prec \rho \parallel \gamma \prec \sigma \rightarrow \delta \prec \rho' \parallel \gamma \prec \sigma} \quad \text{(\tau)} $$

$$ \frac{\gamma \prec \rho \xrightarrow{\text{rb}} \gamma' \prec \rho' \quad \delta \prec \sigma \xrightarrow{\text{rb}} \delta' \prec \sigma' \quad \rho \neq 1}{\gamma \prec \rho \parallel \delta \prec \sigma \rightarrow \gamma' \prec \rho' \parallel \delta' \prec \sigma'} \quad \text{(rbk)} $$

plus the rule symmetric to (τ) w.r.t. $\parallel$. Moreover, rule (rbk) applies only if neither (comm) nor (τ) do.
Up to the rollback mechanism, compliance in the retractable setting is defined as usually done with client/server contracts.

**Definition 8 (Retractable Compliance, $\neg \text{Retractable}$).**

i) The relation $\neg \text{Retractable}$ on contracts with histories is defined as follows:
for any $\delta', \rho', \gamma', \sigma'$, $\delta \prec \rho \neg \text{Retractable} \quad \gamma \prec \sigma$ holds whenever

$$ \delta \prec \rho \parallel \gamma \prec \sigma \xrightarrow{*} \delta' \prec \rho' \parallel \gamma' \prec \sigma' \dashrightarrow \text{implies } \rho' = 1 $$

ii) The relation $\neg \text{Retractable}$ on contracts is defined by: $\rho \neg \text{Retractable} \sigma$ if $[] \prec \rho \neg \text{Retractable} [] \prec \sigma$.

In Buyer/Seller example we have that, in case a belt is agreed upon and the buyer decides to pay using her credit card, the system gets stuck in an unsuccessful state. This causes a rollback enabling a successful state to be reached. So Buyer $\neg \text{Retractable}$ Seller.

Retractable compliance can be axiomatised in terms of derivability in a formal system whose statements do not mention histories.

**Definition 9 (Formal System $\triangleright$ for Retractable Compliance).**

$$ (\text{AX}) : \overline{\Gamma \triangleright 1 \neg \sim \sigma} \qquad (\text{HYP}) : \overline{\Gamma, \rho \neg \sim \sigma \triangleright \rho \neg \sim \sigma} $$

$$ (+ \cdot +) : \frac{\Gamma, \alpha.\rho + \rho' \neg \sim \bar{\alpha}.\sigma + \sigma' \triangleright \rho \neg \sim \sigma}{\Gamma \triangleright \alpha.\rho + \rho' \neg \sim \bar{\alpha}.\sigma + \sigma'} $$

$$ (\oplus \cdot +) : \frac{\forall i \in I. \Gamma, \bigoplus_{i \in I} \bar{a}_i. \rho_i \neg \sim \sum_{j \in I \cup J} a_j. \sigma_j \triangleright \rho_i \neg \sim \sigma_i}{\Gamma \triangleright \bigoplus_{i \in I} \bar{a}_i. \rho_i \neg \sim \sum_{j \in I \cup J} a_j. \sigma_j} $$

$$ (+ \cdot \oplus) : \frac{\forall i \in I. \Gamma, \sum_{j \in I \cup J} a_j. \sigma_j \neg \sim \bigoplus_{i \in I} \bar{a}_i. \rho_i \triangleright \rho_i \neg \sim \sigma_i}{\Gamma \triangleright \sum_{j \in I \cup J} a_j. \sigma_j \neg \sim \bigoplus_{i \in I} \bar{a}_i. \rho_i} $$

Let us formally show that $\emptyset \triangleright \text{Buyer} \neg \sim \text{Seller}$

$$ \frac{\frac{\overline{\Gamma'' \triangleright 1 \neg \sim 1} (\text{AX})}{\Gamma' \triangleright \overline{\text{card}} \oplus \overline{\text{cash}} \neg \sim \text{card} + \text{cash}} (\text{AX})} {\frac{\text{Buyer}' \neg \sim \text{Seller} \triangleright \text{price}.(\overline{\text{card}} \oplus \overline{\text{cash}}) \neg \sim \text{price}.(\overline{\text{card}} + \text{cash})}{\triangleright \text{Buyer} \neg \sim \text{Seller}}} (+, +) $$

where $\Gamma' = \text{Buyer} \neg \sim \text{Seller}, \text{price}.(\overline{\text{card}} \oplus \overline{\text{cash}}) \neg \sim \text{price}.(\overline{\text{card}} + \text{cash})$

and $\Gamma'' = \Gamma'$, $\overline{\text{card}} \oplus \overline{\text{cash}} \neg \sim \text{card} + \text{cash}$

The formal system $\triangleright$ completely axiomatises retractable compliance:

**Theorem 1 (Soundness and Completeness of system $\triangleright$ w.r.t $\neg \text{Retractable}$).**

$\rho \neg \text{Retractable} \sigma$ if and only if $\triangleright \rho \neg \sim \sigma$.
**Equivalence of $\vdash^A$ and $\vdash^{\text{ik}}$.** As previously observed, the judgements of system $\vdash$ abstract away from histories, which are essential in the definition of rollback. This is possible because rollback is just a backtracking mechanism, which is however limited to the exploration of alternative branches of the reduction tree of a system rooted at retractable communications. Since affectible and retractable communications are the same, it is natural to look at system $\vdash$ to establish the equivalence among $\vdash^A$ and $\vdash^{\text{ik}}$.

**Lemma 2.** If $\rho \vdash^A \sigma$, then one of the following conditions holds:

1. $\rho = 1$;

2. $\rho = \sum_{i \in I} \alpha_i \cdot \rho_i$, $\sigma = \sum_{j \in J} \bar{\alpha}_j \cdot \sigma_j$ and $\exists h \in I \cap J. \rho_h \vdash^A \sigma_h$;

3. $\rho = \bigoplus_{i \in I} \bar{a}_i \cdot \rho_i$, $\sigma = \sum_{j \in J} a_j \cdot \sigma_j$, $I \subseteq J$ and $\forall h \in I. \rho_h \vdash^A \sigma_h$;

4. $\rho = \sum_{i \in I} a_i \cdot \rho_i$, $\sigma = \bigoplus_{j \in J} \bar{a}_j \cdot \sigma_j$, $I \supseteq J$ and $\forall h \in J. \rho_h \vdash^A \sigma_h$.

In Theorem 1, soundness and completeness of system $\vdash$ has been proved when the symbol $\vdash^\prec$ is interpreted as the retractable compliance relation $\vdash^{\text{ik}}$. We now show that system $\vdash$ is sound and complete also when the symbol $\vdash^\prec$ is interpreted as the affectible compliance relation $\vdash^A$. The equivalence of the relations $\vdash^{\text{ik}}$ and $\vdash^A$ follows then as an immediate corollary.

**Definition 10 (A $\vdash^A$-semantics for system $\vdash$).**

Let $\Gamma$ be a set of statements of the form $\rho \vdash^\prec \sigma$. We define

i) $\models^A \Gamma$ if $\forall (\rho' \vdash^\prec \sigma') \in \Gamma$. $[\rho' \vdash^A \sigma]$;

ii) $\Gamma \models^A \rho \vdash^\prec \sigma$ if $\models^A \Gamma \Rightarrow \rho \vdash^A \sigma$.

The proof of the following Lemma is inspired to [7].

**Lemma 3 (Soundness of $\vdash$ w.r.t $\vdash^A$).** If $\Gamma \vdash \rho \vdash^\prec \sigma$, then $\Gamma \models^A \rho \vdash^\prec \sigma$.

We write $\mathcal{D} :: \Gamma \vdash \rho \vdash^\prec \sigma$ when $\mathcal{D}$ is a derivation in the system $\vdash$ with conclusion $\Gamma \vdash \rho \vdash^\prec \sigma$. We can easily implement a backward proof search (from conclusion to premises) in the formal system $\vdash$ by means of a procedure **Prove**.

**Lemma 4.** i) Prove($\Gamma \vdash \rho \vdash^\prec \sigma$) = $\mathcal{D} \neq \text{fail}$ implies $\mathcal{D} :: \Gamma \vdash \rho \vdash^\prec \sigma$;

ii) Prove($\Gamma \vdash \rho \vdash^\prec \sigma$) terminates for all judgments $\Gamma \vdash \rho \vdash^\prec \sigma$.

**Lemma 5 (Completeness of $\vdash$ w.r.t $\vdash^A$).** If $\rho \vdash^A \sigma$, then $\vdash \rho \vdash^\prec \sigma$.

*Proof.* (Sketch) If $\rho \vdash^A \sigma$ then by Lemma 2 there are four possibilities; disregarding the contexts $\Gamma$'s, we see that each of these cases corresponds exactly to one rule in system $\vdash$, where **Prove** is recursively applied to the respective premises, but for rule (HYP), that corresponds to an exit clause in **Prove**. It follows that **Prove**($\vdash \rho \vdash^\prec \sigma$) $\neq$ **fail**, so that the thesis follows by Lemma 4, since **Prove** always terminates either returning a correct derivation or **fail**.

**Corollary 1.** $\vdash^{\text{ik}} = \vdash^A$

*Proof.* By Lemmas 3 and 5 and Theorem 1
## 2 Game-theoretic interpretation of retractable contracts

Following [5] we interpret affectible contracts as certain games over event structures. This yields a game-theoretic interpretation of affectible contracts, and hence of retractable contracts by Corollary 1. For the reader's convenience we briefly recall the basic notions of event structure and game associated to an LTS.

**Definition 11 (Event structure [15]).** Let $\mathbf{E}$ be a denumerable universe of events and let $\mathbf{A}$ be a universe of action labels. Besides, let $\# \subseteq E \times E$ be an irreflexive and symmetric relation (called conflict relation).

i) The predicate $CF$ on sets $X \subseteq E$ and the set $Con$ of finite conflict-free sets are defined by $CF(X) = \forall e, e' \in X. \neg(e\#e')$ $Con = \{X \subseteq_{fin} E \mid CF(X)\}$

ii) An event structure is a quadruple $\mathcal{E} = (E, \# , \vdash, l)$ where
$\vdash \subseteq Con \times E$ is a relation such that $sat(\vdash) = \vdash$ (i.e. $\vdash$ is saturated),
where $sat(\vdash) = \{ (Y, e) \mid X \vdash e \ \& \ X \subseteq Y \in Con \};$
$- l: E \to \mathbf{A}$ is a labelling function.

Given a set $E$ of events, $E^\infty$ denotes the set of sequences (both finite and infinite) of its elements. We denote by $e = \langle e_0 e_1 \cdots \rangle$ a sequence of events$^3$. Given $e$, we denote by $\hat{e}$ the set of its elements, by $|e|$ its length (either a natural number or $\infty$) and by $e_i$ for $i < |e|$ the subsequence $\langle e_0 e_1 \cdots e_{i-1} \rangle$ of its first $i$ elements. Given a set $X$ we denote by $|X|$ its cardinality. $\mathbb{N}$ is the set of natural numbers.

**Definition 12 (LTS over configurations [5]).** Given an event structure $\mathcal{E} = (E, \# , \vdash, l)$, we define the LTS $(\mathcal{P}_{fin}(E), E, \to_{\mathcal{E}})$ as follows:

$$ C \xrightarrow{e} C \cup \{e\} \quad \text{if} \quad C \vdash e, e \notin C \text{ and } CF(C \cup \{e\}) $$

Given an LTS $(S, \to)$ and a state $s \in S$, we denote by $(s, \to)$ the restriction of $\to$ to the transitions starting with the state $s$, and by $\mathrm{Tr}(s, \to)$ the set of the (finite or infinite) traces in $(s, \to)$ out of $s$.

**Multi-player games.** All the subsequent definitions and terminology are from [5], except in the case of games that we call multi-player instead of “contracts”, which would be confusing in the present setting.

A set of partecipants (players) to a game will be denoted by $\mathfrak{P}$, whereas the universe of partecipants is denoted by $\mathfrak{P}_U$. We shall use $A, B, \dots$ as variables ranging over $\mathfrak{P}$ or $\mathfrak{P}_U$. The symbols $A, B, \dots$ will denote particular elements of $\mathfrak{P}$ or $\mathfrak{P}_U$. We assume that each event is associated to a player by means of a function $\pi: \mathbf{E} \to \mathfrak{P}_U$. Moreover, given $A \in \mathfrak{P}_U$ we define $E_A = \{e \in \mathbf{E} \mid \pi(e) = A\}$.

**Definition 13 (Multi-player game).**

i) A game $\mathcal{G}$ is a pair $(\mathcal{E}, \Phi)$ where $\mathcal{E} = (E, \# , \vdash, l)$ is an event structure and $\Phi: \mathfrak{P}_U \to E^\infty \to \{-1, 0, 1\}$ associates each participant and trace with a payoff. Moreover, for all $X \vdash e$ in $\mathcal{E}$, $\Phi(\pi(e))$ is defined. We say that $\mathcal{G}$ is a game with partecipants $\mathfrak{P}$ whenever $\Phi A$ is defined for any player $A$ in $\mathfrak{P}$.

<footnote>$^3$ Differently than in [5], we use the notation $e$ for sequences instead of $\sigma$, which refers to a contract here.</footnote>
ii) A play of a game $\mathcal{G} = (\mathcal{E}, \mathcal{F})$ is a (finite or infinite) trace of $(\emptyset, \to_{\mathcal{E}})$ i.e. an element of $\mathrm{Tr}(\emptyset, \to_{\mathcal{E}})$.

**Definition 14 (Strategy and conformance).** A strategy $\Sigma$ for a partecipant $A$ in a game $\mathcal{G}$ is a function which maps each finite play $e = (e_0 \cdots e_n)$ to a (possibly empty) subset of $\mathbf{E}_A$ such that: $e \in \Sigma(e) \Rightarrow ee$ is a play of $\mathcal{G}$. A play $e = (e_0 e_1 \cdots)$ conforms to a strategy $\Sigma$ for a partecipant $A$ in $\mathcal{G}$ if, for all $i \ge 0$, $e_i \in \mathbf{E}_A \Rightarrow e_i \in \Sigma(e_i)$.

Although events, namely moves, are associated to players via the map $\pi$, this is not injective in general, so that players can share moves. In general there are neither a turn rule nor alternation of players, similarly to concurrent games in [1]. A strategy $\Sigma$ provides “suggestions” to some player on how to legally move continuing finite plays (also called “positions” in game-theoretic literature). But $\Sigma$ may be ambiguous at some places, since $\Sigma(e)$ may contain more than an event; in fact it can be viewed as a partial mapping which is undefined when $\Sigma(e) = \emptyset$.

We refer to [5] for the general definition of winning strategy for multi-player games (briefly recalled also in Remark 1 below), since it involves the conditions of fairness and innocence, which will be trivially satisfied in our interpretation of affectible client/server systems, where the notion of winning strategy corresponds to the one given in Def. 19.

**Turn-based operational semantics and compliance.** Toward the game theoretic interpretation of a client/server system $\rho \parallel \sigma$, we introduce a slightly different description of the semantics of affectible contracts, making explicit the idea of a three-player game. We interpret the internal choices and the input actions of the client as moves of a player A and the internal choices and the input actions of the server as moves of a player B. The synchronisations due to affectible choices are instead interpreted as moves of the third player C.

From a technical point of view this is a slight generalization and adaptation to our scenario of the turn-based semantics of “session types” in [5], §5.2. The changes are needed both because we have three players instead of two, and because session types are just session contracts, that is affectible contracts without affectible outputs.

**Definition 15 (Single-buffered ASC).** The set $\mathrm{ASC}^{[1]}$ of single-buffered affectible contracts is defined by $\mathrm{ASC}^{[1]} = \mathrm{ASC} \cup \{\mathbf{0}\} \cup \{[\bar{a}_k]\sigma_k \mid \oplus_{i \in I} \bar{a}_i \cdot \sigma_i \in \mathrm{ASC}, k \in I\}$

We use the symbols $\tilde{\rho}, \tilde{\sigma}, \tilde{\rho}', \tilde{\sigma}'$... to denote elements of $\mathrm{ASC}^{[1]}$. A turn-based configuration (configuration for short) is a pair $\tilde{\rho} \parallel \tilde{\sigma}$, where $\tilde{\rho}, \tilde{\sigma} \in \mathrm{ASC}^{[1]}$.

As in [5], we have added the “single buffered” contracts $[\bar{a}]\sigma$ to represent the situation in which $\bar{a}$ is the only output offered after an internal choice. Since the actual synchronization takes place in a subsequent step, $\bar{a}$ is “buffered” in front of the continuation $\sigma$.
<figure><img src="image_2.png" /><figcaption>Fig. 1. Turn-based operational semantics of turn-based configurations</figcaption></figure>

**Definition 16 (Turn-based operational semantics of configurations).**

Let $\mathbf{tbAct} = \{A, B, C\} \times (\mathbf{Act} \cup \{\checkmark\})$. In Figure 1 we define the LTS $\rightarrow$ over turn-based configurations, with labels in $\mathbf{tbAct}$.

Comparing $\rightarrow$ with the LTS for affectible contracts, we observe that $[\bar{a}]\sigma$ is a duplicate of $\bar{a}\cdot\sigma$, with the only difference that now there is a redundant step in $\oplus_{i \in I} \bar{a}_i \cdot \rho_i \parallel \tilde{\sigma} \xrightarrow{A:\bar{a}_k} [\bar{a}_k] \rho_k \parallel \tilde{\sigma}$ when $I$ is the singleton $\{k\}$. Also we have the new reduction $\mathbf{1} \parallel \tilde{\rho} \xrightarrow{C:\checkmark} \mathbf{0} \parallel \tilde{\rho}$ to signal when player C wins.

Let $\beta = (\beta_1 \cdots \beta_n) \in \mathbf{tbAct}^*$. We shall use the notation $\xrightarrow{\beta} = \xrightarrow{\beta_1} \cdots \xrightarrow{\beta_n}$

**Definition 17 (Turn-Based Compliance Relation $\oplus^b$).**

i) Let $\mathcal{H} : \mathcal{P}(\mathbf{ASC}^{[1]} \times \mathbf{ASC}^{[1]}) \rightarrow \mathcal{P}(\mathbf{ASC}^{[1]} \times \mathbf{ASC}^{[1]})$ be such that, for any $\mathcal{R} \subseteq \mathbf{ASC}^{[1]} \times \mathbf{ASC}^{[1]}$, we get $(\tilde{\rho}, \tilde{\sigma}) \in \mathcal{H}(\mathcal{R})$ if:

1) $\tilde{\rho} \parallel \tilde{\sigma} \dashrightarrow \mathbf{implies} \rho = \mathbf{0}$;

2) $\forall \tilde{\rho}', \tilde{\sigma}'. \ [ \tilde{\rho} \parallel \tilde{\sigma} \xrightarrow{\beta} \tilde{\rho}' \parallel \tilde{\sigma}' \ \mathbf{implies} \ \tilde{\rho}' \mathcal{R} \tilde{\sigma}' ]$, \\
where $\beta \in \{A:a, A:\bar{a}, B:a, B:\bar{a} \mid a \in \mathcal{N}\}$;

3) $\exists a \in \mathcal{N}. \tilde{\rho} \parallel \tilde{\sigma} \xrightarrow{C:a} \mathbf{implies} \exists \tilde{\rho}', \tilde{\sigma}', a. [ \tilde{\rho} \parallel \tilde{\sigma} \xrightarrow{C:a} \tilde{\rho}' \parallel \tilde{\sigma}' \text{ and } \tilde{\rho}' \mathcal{R} \tilde{\sigma}' ]$;

ii) A relation $\mathcal{R} \subseteq \mathbf{ASC}^{[1]} \times \mathbf{ASC}^{[1]}$ is a turn-based compliance relation if $\mathcal{R} \subseteq \mathcal{H}(\mathcal{R})$. $\oplus^b$ is the greatest solution of the equation $X = \mathcal{H}(X)$, that is $\oplus^b = \nu\mathcal{H}$.

iii) For $\rho, \sigma \in \mathbf{ASC}$, we say that $\rho$ is turn-based compliant with $\sigma$ if $\rho \oplus^b \sigma$.

Turn-based compliance is equivalent to affectible compliance

**Theorem 2.** Let $\rho, \sigma \in \mathbf{ASC}$. $\rho \oplus^b \sigma \Leftrightarrow \rho \oplus^A \sigma$.

**Three-player game interpretation for ASC client/server systems.** Using the turn-based semantics, we associate to any client/server system an event structure, and then a three-player game$^4$, extending the treatment of session types with two-player games in [5]. For our purposes we just consider the LTS of a given client/server system instead of an arbitrary one.

<footnote>$^4$ Such interpretation is called semantic-based in [5] and it applies quite naturally to our context. Instead the syntax-based approach (which is equivalent to the semantic-based one in a two-players setting; see [5] §5.3.2) cannot be straightforwardly extended to a three-player game.</footnote>
**Definition 18 (ES of affectible-contracts systems).**

Let $\rho \parallel \sigma$ be a client/server system of affectible contracts. We define the event structure $[[\rho \parallel \sigma]] = (E, \# , \vdash, l)$, where

$$ - E = \{ (n, \beta) \mid n \in \mathbb{N}, \beta \in \mathbf{tbAct} \} $$

$$ - \# = \{ ((n, \beta_1), (n, \beta_2)) \mid n \in \mathbb{N}, \beta_1, \beta_2 \in \mathbf{tbAct}, \beta_1 \neq \beta_2 \} $$

$$ - \vdash = \mathrm{sat}(\vdash_{\rho||\sigma}) $$

$$ \text{where } \vdash_{\rho||\sigma} = \{ (X, (n, \beta)) \mid \rho \parallel \sigma \xrightarrow{\mathrm{snd}(X)} \tilde{\rho}' \parallel \tilde{\sigma}' \xrightarrow{\beta} \text{ and } n = |X| + 1 \} $$

$$ - l(n, \beta) = \beta $$

where the partial function $\mathrm{snd}(-)$ maps any $X = \{ (i, \beta_i) \}_{i=1..n}$ to $\langle \beta_1 \cdots \beta_n \rangle$, and it is undefined over sets not of the shape of $X$.

Events in $[[\rho \parallel \sigma]]$ are actions in **tbAct** paired with time stamps. Two events are in conflict if different actions should be performed at the same time, so that configurations must be linearly ordered w.r.t. time. The relation $X \vdash_{\rho||\sigma} (n, \beta)$ holds if $X$ is a trace in the LTS of $\rho \parallel \sigma$ of length $n-1$; therefore the enabling $Y \vdash (n, \beta)$ holds if and only if $Y$ includes a trace of length $n-1$ that can be prolonged by $\beta$, possibly including $(n, \beta)$ itself and any other action that might occur after $\beta$ in the LTS.

So, by the above, $\vdash_{\mathrm{Buyer}||\mathrm{Seller}}$ in $[[\mathrm{Buyer} || \mathrm{Seller}]]$ corresponds to
$$ \begin{array}{l} \{ \emptyset \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (1, (C: \mathbf{belt})), \emptyset \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (1, (C: \mathbf{bag})), \\ \{ (1, (C: \mathbf{belt})) \} \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (2, (B: \overline{\mathbf{price}})), \{ (1, (C: \mathbf{bag})) \} \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (2, (B: \overline{\mathbf{price}})), \\ \{ (1, (C: \mathbf{belt})), (2, (\mathrm{Seller}: \overline{\mathbf{price}})) \} \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (3, (A: \overline{\mathbf{price}})), \dots \\ \dots X_1 \vdash_{\mathrm{Buyer}||\mathrm{Seller}} (6, (C, \checkmark)) \end{array} $$

where $X_1 = \{(1, (C:bag)), (2, (B:price)), (3, (A:price)), (4, (A:cash)), (5, (B:cash))\}$

The $\vdash_{\rho||\sigma}$ of this simple example is finite. It is not so in general for systems with recursive contracts.

The following definition is a specialisation of Definitions 4.6 and 4.7 in [5]. We use $\mathrm{MaxTr}(s, \rightarrow)$ and $\mathrm{FinMaxTr}(s, \rightarrow)$ to denote the set of maximal traces and finite maximal traces, respectively, of $\mathrm{Tr}(s, \rightarrow)$.

**Definition 19.** Given $\rho, \sigma \in \mathbf{ASC}$, we define the game $\mathcal{G}_{\rho||\sigma}$ as $([\rho \parallel \sigma], \Phi)$, where $\pi(n, \beta) = A$ if $\beta = A:\alpha$, $\Phi A$ is defined only if $A \in \{A, B, C\}$ and

$$ \Phi A e = \begin{cases} 1 & \text{if } \mathbf{P}(A, e) \\ -1 & \text{otherwise} \end{cases} $$

where $\mathbf{P}(A, e)$ holds whenever

$$ e \in \mathrm{Tr}(\emptyset, \rightarrow^{[\rho||\sigma]}) \ \& \ [e \in \mathrm{FinMaxTr}(\emptyset, \rightarrow^{[\rho||\sigma]}) \Rightarrow \exists e', n. e = e'(n, (A:\checkmark))] $$

A player $A$ wins in the sequence of events $e$ if $\Phi A e > 0$. A strategy $\Sigma$ for player $A$ is winning if $A$ wins in all plays conforming to $\Sigma$.

Note that, $\mathbf{P}(A, e)$ holds for any $A$ and infinite element $e$ of $\mathrm{Tr}(\emptyset, \rightarrow^{[\rho||\sigma]})$.

For the game $\mathcal{G}_{\mathrm{Buyer}||\mathrm{Seller}}$, it is possible to check that, for instance,

$$ \Phi C s_1 = 1, \quad \Phi A s_1 = -1, \quad \Phi B s_2 = -1, \quad \Phi C s_3 = -1 $$

where $s_1 = (1, (C:bag))(2, (B:price))(3, (A:price))(4, (A:cash))(5, (B:cash))(6, (C, \checkmark))$, $s_2 = (4, (A:bag))(1, (C:price))$

$$ s_3 = (1, (C:bag))(2, (B:price))(3, (A:price))(4, (A:cash))(5, (B:cash)) $$
Let us define a particular strategy $\tilde{\Sigma}$ for C in $\mathcal{G}_{\text{Buyer} \parallel \text{Seller}}$ as follows:

$$ \tilde{\Sigma}(s) = \begin{cases} \{(1, (\text{C:bag}))\} & \text{if } s = \langle\rangle \\ \{(6, (\text{C, }\check{\text{}}))\} & \text{if } s = s_3 \\ \emptyset & \text{for any other play} \end{cases} $$

The strategy $\tilde{\Sigma}$ for C in $\mathcal{G}_{\text{Buyer} \parallel \text{Seller}}$ is winning.

**Remark 1.** According to [5], A wins in a play if $WAe > 0$, where $WAe = \Phi Ae$ if all players are “innocent” in $e$, while if $A$ is “culpable”, $WAe = -1$, and if $A$ is innocent and someone else culpable, $WAe = +1$. A strategy $\Sigma$ of $A$ is winning if $A$ wins in all *fair* plays conforming to $\Sigma$. A play $e$ is “fair” for a strategy $\Sigma$ of a player $A$ if any event in $E_A$ which is infinitely often enabled is eventually performed. Symmetrically $A$ is “innocent” in $e$ if she eventually plays all persistently enabled moves of her in $e$, namely if she is fair to the other players, since the lack of a move by $A$ might obstacle the moves by others; she is “culpable” otherwise. As said above, Definition 19 is a particularisation of the general definitions in [5]. In fact in a game $G_{\rho||\sigma}$ no move of any player can occur more than once in a play $e$ because of time stamps. Therefore no move can be “persistently enabled”, nor it can be prevented since it can be enabled with a given time stamp only if there exists a legal transition in the LTS with the same label. Hence any player is innocent in a play $e$ of $G_{\rho||\sigma}$ and all plays are fair. Therefore $W$ coincides with $\Phi$.

It is possible to characterize affectible and retractable compliance in terms of the existence of a winning strategy for C in $G_{\rho||\sigma}$.

**Theorem 3.** $\rho \stackrel{-|^A}{\sigma}$ (or, equivalently, $\rho \stackrel{-|^k}{\sigma}$) if and only if player C has a winning strategy in the three-player game $G_{\rho||\sigma}$.

## 3 Strategies as orchestrators

In the present section we show that a client $\rho$ is retractable-compliant with a server $\sigma$ if and only if their interactions can be led to a successful state by means of the mediation of an orchestrator. To do that we show how an orchestrator can be obtained out of a “univocal” winning strategy (see Def. 24 below) for player C in the game $G_{\rho||\sigma}$, and vice versa. For a detailed discussion on orchestrators for contracts and orchestrators for session-contracts, we refer to [14,13] and [2] respectively. In the present setting, our orchestrators, that we dub *strategy-orchestrators*, are defined as a variant of the session-orchestrators of [2], which in turn are a restriction of orchestrators in [14]. The task of a strategy orchestrator is to mediate the interactions between two affectible session contracts by selecting one of the possible affectible choices and constraining non-affectible ones.
We consider two sorts of orchestration actions, having the following shapes:

$$ \langle\alpha, \bar{\alpha}\rangle, \text{ enabling the unaffectible synchronization } \rho \parallel \sigma \xrightarrow{\tau} \rho' \parallel \sigma'; $$

$$ \langle\alpha, \bar{\alpha}\rangle^{+}, \text{ enabling the affectible synchronization } \rho \parallel \sigma \xrightarrow{+} \rho' \parallel \sigma'. $$
**Definition 20 (Strategy Orchestrators).**

i) The set **OrchAct** of strategy-orchestration actions is defined by
**OrchAct** = { $\langle \alpha, \bar{\alpha} \rangle$ | $\alpha \in \mathcal{N} \cup \bar{\mathcal{N}}$ } $\cup$ { $\langle \alpha, \bar{\alpha} \rangle^+$ | $\alpha \in \mathcal{N} \cup \bar{\mathcal{N}}$ }

We let $\mu, \mu', \dots$ range over elements of **OrchAct** with the shape $\langle \alpha, \bar{\alpha} \rangle$, and
$\mu^+, \mu'^+, \dots$ range over elements of **OrchAct** with the shape $\langle \alpha, \bar{\alpha} \rangle^+$.

ii) We define the set **Orch** of strategy orchestrators, ranged over by $f, g, \dots$, as the closed (with respect to the binder **rec**) terms generated by the following

grammar:

<table>
  <thead>
    <tr>
      <th>f, g</th>
      <th>::=</th>
      <th>1</th>
      <th>idle</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>|</td>
      <td>μ<sup>+</sup>.f</td>
      <td></td>
      <td>prefix</td>
    </tr>
    <tr>
      <td>|</td>
      <td>μ<sub>1</sub>.f<sub>1</sub> ∨ . . . ∨ μ<sub>n</sub>.f<sub>n</sub></td>
      <td></td>
      <td>disjunction</td>
    </tr>
    <tr>
      <td>|</td>
      <td>x</td>
      <td></td>
      <td>variable</td>
    </tr>
    <tr>
      <td>|</td>
      <td>rec x.f</td>
      <td></td>
      <td>recursion</td>
    </tr>
  </tbody>
</table>

where the $\mu_i$ in a disjunction are pairwise distinct. Moreover, we impose
strategy orchestrators to be contractive, i.e. the $f$ in $\text{rec } x.f$ is assumed not
to be a variable.

We write $\bigvee_{i \in I} \mu_i.f_i$ as short for $\mu_1.f_1 \vee \dots \vee \mu_n.f_n$, where $I = \{1, \dots, n\}$.
If not stated otherwise, we consider recursive orchestrators up-to unfolding, that
is we equate $\text{rec } x.f$ with $f\{x/\text{rec } x.f\}$. We omit trailing 1's.

Strategy orchestrators are “simple orchestrators” in [14] and “synchronous
orchestrators” in [13], but for the kind of prefixes which are allowed in a single
prefix or in a disjunction. In fact a prefix $\langle \alpha, \bar{\alpha} \rangle^+$ cannot occur in disjunctions,
where all the orchestrators must be prefixed by $\langle \alpha, \bar{\alpha} \rangle$ actions.

**Definition 21 (Strategy orchestrators LTS).**

We define the labelled transition system (Orch, OrchAct, ↦→) by

$$
\mu^+.f \stackrel{\mu^+}{\mapsto} f \qquad (\bigvee_{i \in I} \mu_i.f_i) \stackrel{\mu_k}{\mapsto} f_k \quad (k \in I)
$$

An orchestrated system, represented by $\rho \parallel_f \sigma$, is client/server system whose
interaction is mediated by an orchestrator.

**Definition 22 (LTS for orchestrated-systems).**

Let $\rho, \sigma \in \mathbf{ASC}$ and $f \in \mathbf{Orch}$.

$$
\frac{
  \begin{array}{c}
    \rho \to \rho' \\
    \rho \parallel_f \sigma \to \rho' \parallel_f \sigma
  \end{array}
}{
  \rho \xrightarrow{a} \rho' \quad f \xrightarrow{\langle \bar{\alpha}, \alpha \rangle} f' \quad \sigma \xrightarrow{\bar{\alpha}^+} \sigma'
}
\qquad
\frac{
  \begin{array}{c}
    \sigma \to \sigma' \\
    \rho \parallel_f \sigma \to \rho \parallel_f \sigma'
  \end{array}
}{
  \rho \xrightarrow{\bar{\alpha}^+} \rho' \quad f \xrightarrow{\langle \alpha, \bar{\alpha} \rangle} f' \quad \sigma \xrightarrow{a} \sigma'
}
\qquad
\frac{
  \begin{array}{c}
    \rho \xrightarrow{\alpha} \rho' \quad f \xrightarrow{\langle \bar{\alpha}, \alpha \rangle} f' \quad \sigma \xrightarrow{\bar{\alpha}} \sigma' \\
    \rho \parallel_f \sigma \xrightarrow{\tau} \rho' \parallel_f \sigma'
  \end{array}
}{
  \alpha \in \mathcal{N} \cup \bar{\mathcal{N}}
}
$$

$$
\frac{\rho \xrightarrow{\alpha} \rho' \quad f \xrightarrow{\langle \bar{\alpha}, \alpha \rangle} f' \quad \sigma \xrightarrow{\bar{\alpha}} \sigma'}{\rho \parallel_f \sigma \xrightarrow{\tau} \rho' \parallel_f \sigma'} (\alpha \in \mathcal{N} \cup \bar{\mathcal{N}})
$$

Moreover, we define $\Rightarrow = \to^* \circ (\to \to \to^+)$.
In both transitions $\xrightarrow{+}$ and $\xrightarrow{\tau}$ synchronization may happen only if the orchestrator has a transition with the appropriate pair of actions. This is because in an orchestrated interaction both client and server are committed to the synchronizations allowed by the orchestrator only. It is then clear that an orchestrator always selects one synchronisation of affectible actions on client and server side, while the disjunction of orchestrators represents the constraint that only certain synchronisations of unaffectible actions are permitted.

**Definition 23 (Strategy-orchestrated Compliance).**

i) $f: \rho \nvDash^{\text{Orch}} \sigma$ if for any $\rho'$ and $\sigma'$, the following holds:

$$ \rho \|_f \sigma \implies^* \rho' \|_{f'} \sigma' \not\iff \text{implies } \rho' = 1. $$

ii) $\rho \nvDash^{\text{Orch}} \sigma$ if $\exists f. [f: \rho \nvDash^{\text{Orch}} \sigma]$.

**Definition 24 (Univocal strategies).** $\Sigma$ is univocal if $\forall e. |\Sigma(e)| \le 1$.

The strategy $\tilde{\Sigma}$ for $C$ in $G_{\text{Buyer}} \|_{\text{Seller}}$, defined in the previous section, is univocal.

The proof of the following theorem relies on the fact that any orchestrator $f$ such that $f: \rho \nvDash^{\text{Orch}} \sigma$ corresponds to a univocal winning strategies for player $C$ in $G_{\rho} \|_{\sigma}$. Vice versa a univocal winning strategy $\Sigma$ for $C$ always induces an orchestrator $f_{\Sigma}$. It is not restrictive to look at univocal strategies only, as established in the next lemma.

We say that $\Sigma$ refines $\Sigma'$, written $\Sigma \le \Sigma'$, if and only if $\Sigma(e) \subseteq \Sigma'(e)$ for all $e$.

**Lemma 6.** If $C$ has a winning strategy $\Sigma$, then $C$ has a univocal winning strategy $\Sigma'$ such that $\Sigma' \le \Sigma$.

**Theorem 4.**

$\exists f. [f: \rho \nvDash^{\text{Orch}} \sigma] \Leftrightarrow \text{there exists a winning strategy for player } C \text{ in } G_{\rho} \|_{\sigma}.$
In particular, a winning strategy for player $C$ in $G_{\rho} \|_{\sigma}$ can be obtained out of an
orchestrator $f$ such that $f: \rho \nvDash^{\text{Orch}} \sigma$, and vice versa.

The orchestrator that can be obtained out of the strategy $\tilde{\Sigma}$ is
$$ \langle \text{bag}, \overline{\text{bag}} \rangle^+. \langle \text{price}, \overline{\text{price}} \rangle (\langle \text{cash}, \overline{\text{cash}} \rangle \lor \langle \text{card}, \overline{\text{card}} \rangle). $$

**Remark 2.** Univocal strategies correspond to strategy-orchestrators and are technically easier to work with. On the other hand, we can recover a full correspondence among $C$ strategies and orchestrators by allowing disjunctions of affectible synchronization actions $\langle \alpha, \bar{\alpha} \rangle^+$. In a session-based scenario, however, we expect any nondeterminism to depend solely on either the client or the server. By allowing $f = \langle \bar{a}, a \rangle^+. f_1 \lor \langle \bar{b}, b \rangle^+. f_2$ in the system $a.\rho_1 + b.\rho_2 \|_f \bar{a}.\sigma_1 + \bar{b}.\sigma_2$, the nondeterminism would depend on the orchestrator too.

Based on the formal system of Definition 9, the algorithm **Synth** in Figure 3 takes a (initially empty) set of assumptions $\Gamma$, and the affectible contracts $\rho$ and $\sigma$, and it returns a set $O$ of orchestrators (and hence a set of strategies by the above) if any, such that for any $f \in O$ we have $f: \rho \nvDash^{\text{Orch}} \sigma$; the algorithm returns the empty set otherwise. In the algorithm **Synth** we consider orchestrators as explicit terms, that is we do not consider recursion up-to unfolding.
Synth($\Gamma$, $\rho$, $\sigma$) =
  if $x: \rho \nV^{\text{Orch}} \sigma \in \Gamma$ then $\{x\}$
else if $\rho = 1$ then $\{1\}$
else if $\rho = \sum_{i \in I} \bar{\alpha}_i \cdot \rho_i$ and $\sigma = \sum_{j \in J} \alpha_j \cdot \sigma_j$ (where $\alpha \in \mathcal{N} \cup \bar{\mathcal{N}}$) then
  let $\Gamma' = \Gamma$, $x: \rho \nV^{\text{Orch}} \sigma$ in
    $\bigcup_{i \in I} \{ \text{rec } x \cdot (\langle \alpha_i, \bar{\alpha}_i \rangle^+ \cdot f \mid f \in \text{Synth}(\Gamma', \rho_i, \sigma_i) \}$
else if $\rho = \bigoplus_{i \in I} \bar{\alpha}_i \cdot \rho_i$ and $\sigma = \sum_{j \in I \cup J} a_j \cdot \sigma_j$ then
  let $\Gamma' = \Gamma$, $x: \rho \nV^{\text{Orch}} \sigma$ in
    $\{ \text{rec } x \cdot \bigvee_{i \in I} (\langle a_i, \bar{a}_i \rangle \cdot f_i \mid \forall i \in I, f_i \in \text{Synth}(\Gamma', \rho_i, \sigma_i) \}$
else if $\rho = \sum_{j \in I \cup J} \bar{\alpha}_j \cdot \rho_i$ and $\sigma = \bigoplus_{i \in I} a_i \cdot \sigma_i$ then
  let $\Gamma' = \Gamma$, $x: \rho \nV^{\text{Orch}} \sigma_i$ in
    $\{ \text{rec } x \cdot \bigvee_{i \in I} (\langle a_i, \bar{a}_i \rangle \cdot f_i \mid \forall i \in I, f_i \in \text{Synth}(\Gamma', \rho_i, \sigma_i) \}$
else $\emptyset$

<caption>Fig. 2. The algorithm Synth.</caption>

**Theorem 5 (Soundness and Completeness of Synth).**

The algorithm Synth is correct and complete in the following sense:

i) Synth($\Gamma$, $\rho$, $\sigma$) terminates for any $\Gamma$, $\rho$ and $\sigma$.

ii) If $f \in \text{Synth}(\emptyset, \rho, \sigma) \neq \emptyset$ then $f: \rho \nV^{\text{Orch}} \sigma$.

iii) If $f: \rho \nV^{\text{Orch}} \sigma$ then there exists $g \in \text{Synth}(\emptyset, \rho, \sigma) \neq \emptyset$ such that the (possibly infinite) unfolding of $f$ and $g$ yields the same regular tree.

It is not difficult to check that by computing Synth($\emptyset$, Buyer, Seller) we get a set just consisting of the orchestrator corresponding to the strategy $\tilde{\Sigma}$, namely
$$ \text{Synth}(\emptyset, \text{Buyer}, \text{Seller}) = \{ (\text{bag}, \text{bag})^+ \cdot (\langle \text{price}, \text{price} \rangle \langle (\text{cash}, \text{cash}) \vee (\langle \text{card}, \text{card} \rangle) \rangle) \} $$
Using the previous results and Lemma 6 we get the following:

**Corollary 2.** i) The relation $\nV^{\text{Orch}}$ is decidable.

ii) For any $\rho, \sigma \in \mathcal{ASC}$, it is decidable whether there exists a winning strategy for player C in $G_{\rho \parallel \sigma}$.

Moreover, in case a winning strategy exists, it is possible to effectively compute a univocal winning strategy.

# 4 Conclusion and Future Work

We have studied two approaches to loosening compliance among a client and a server in contract theory, based on the concepts of dynamic adaptation and of mediated interaction respectively. We have seen that these induce equivalent notions of compliance, which can be shown via the abstract concept of winning strategy in a suitable class of games.

The byproduct is that the existence of the agreement among two contracts specifying adaptive behaviours is established by statically synthesizing the proper
orchestrator, hence avoiding any trial and error mechanism at run time. The study in this paper has been limited to the case of binary sessions since this is the setting in which both orchestrators and retractable contracts have been introduced. However strategy based concepts of agreement have been developed in the more general scenario of multiparty interaction, which seems a natural direction for future work.

**Acknowledgments.** The authors wish to thank Massimo Bartoletti for an insightful discussion, Mariangiola Dezani for her everlasting support and the three anonymous referees for their help in improving the final version of the paper.

## References

1. Abramsky, S., Mellies, P.A.: Concurrent games and full completeness. In: Logic in Computer Science, 1999. Proceedings. 14th Symposium on. pp. 431–442 (1999)

2. Barbanera, F., van Bakel, S., de'Liguoro, U.: Orchestrated session compliance. In: Proceedings ICE'15. EPTCS, vol. 189, pp. 21–36 (2015)

3. Barbanera, F., de'Liguoro, U.: Sub-behaviour relations for session-based client/server systems. MSCS 25(6), 1339–1381 (2015)

4. Barbanera, F., Dezani-Ciancaglini, M., Lanese, I., de'Liguoro, U.: Retractable contracts. In: PLACES. EPTCS, vol. 203, pp. 61–72. Open Publishing Ass. (2015)

5. Bartoletti, M., Cimoli, T., Pinna, G.M., Zunino, R.: Contracts as games on event structures. J.of Logical and Algebraic Methods in Progr. 85(3), 399 – 424 (2016)

6. Bernardi, G., Hennessy, M.: Compliance and testing preorders differ. In: Software Engineering and Formal Methods - SEFM 2013. LNCS, vol. 8368, pp. 69–81 (2013)

7. Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inform. 33(4), 309–338 (1998)

8. Bravetti, M., Zavattaro, G.: A theory of contracts for strong service compliance. Mathematical Structures in Computer Science 19(3), 601–638 (2009)

9. Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. on Prog. Lang. and Sys. 31(5), 19:1–19:61 (2009)

10. Gay, S., Hole, M.: Subtyping for Session Types in the Pi-Calculus. Acta Informatica 42(2/3), 191–225 (2005)

11. Laneve, C., Padovani, L.: The Must Preorder Revisited: An Algebraic Theory for Web Services Contracts. In: CONCUR'07. LNCS, vol. 4703, pp. 212–225. Springer (2007)

12. Nicola, R.D., Hennessy, M.: Testing equivalence for processes. In: ICALP. LNCS, vol. 154, pp. 548–560. Springer (1983)

13. Padovani, L.: Contract-based discovery and adaptation of web services. In: SFM. LNCS, vol. 5569, pp. 213–260. Springer (2009)

14. Padovani, L.: Contract-Based Discovery of Web Services Modulo Simple Orchestrators. Theoretical Computer Science 411, 3328–3347 (2010)

15. Winskel, G.: Event structures. In: Advances in Petri Nets 1986, Part II (1987)