Daniel Hirschkoff

Enguerrand Prebet

Davide Sangiorgi

On the Representation of References in the pi-calculus

Keywords: 2012 ACM Subject Classification Theory of computation → Semantics and reasoning Keywords and phrases Process calculus, Bisimulation, Asynchrony, Imperative programming Digital Object Identifier 10.4230/LIPIcs.CONCUR.2020.31

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue.

We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π ref , an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π ref . We then consider a translation of π ref into Aπ. References of π ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive 'game' on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.

Introduction

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). This therefore requires representations of references using the names of the π-calculus. There are strong similarities between the names of the π-calculus and the references of imperative languages. This is evident in the denotational semantics of these languages: the mathematical techniques employed in modelling the π-calculus (e.g., [START_REF] Stark | A fully abstract domain model for the pi-calculus[END_REF][START_REF] Fiore | A fully abstract model for the π-calculus[END_REF]) were originally developed for the semantic description of references. Yet names and references behave rather differently: receiving from a name is destructive -it consumes a value -whereas reading from a reference is not; a reference has a unique location, whereas a name may be used by several processes both in input and in output; etc. These differences

31:2

On the Representation of References in the pi-calculus make it unclear if and how interesting properties of imperative languages can be proved via a translation into the π-calculus.

A subset of the π-calculus that often appears in the literature, for its expressive power and elegant theory, is the Asynchronous π-calculus (Aπ). Aπ allows one to provide a simpler representation of references, where a reference storing a value n is just an output message n (in Aπ output is not a prefix, hence it has no process continuation). A process that wishes to access the reference is supposed to make an input at and then immediately emit a message at with the new content of the reference. For instance a process reading on the reference and binding its content to x in the continuation P is (x). ( x | P ) .

Another reason that makes this representation of references in Aπ interesting is the bisimilarity of Aπ, called asynchronous bisimilarity. It differs from standard bisimilarity in the input clause, in which a transition P n m

---→ P (where P is receiving m on n) can be answered by a bisimilar process Q thus:

n m | Q = ⇒ Q ( * )
(provided P and Q are bisimilar), where = ⇒ stands for zero or several internal communication steps. Intuitively, Q does not necessarily perform an input on n in response to the transition done by P . To see why this clause could be interesting with references, consider a process that performs a useless read on a reference and then continues as P 2 ; in a language with references this would be equivalent to P 2 itself. When written in Aπ, the process with the useless read becomes P 1 def = (x). ( x | P 2 ) where x does not appear in P 2 . In ordinary bisimilarity, P 1 is immediately distinguished from P 2 , as the latter cannot answer the input

transition P 1 n ---→ n | P 2 .
However, the answer is possible using the clause ( * ), as we have

n | P 2 = ⇒ n | P 2 .
We are not aware of studies that investigate the faithfulness of the above representation of references in Aπ. In this paper we address this issue. For this, we first define π ref , an extension of Aπ with references and operators to manipulate them. We then consider a translation of π ref into Aπ and:

we study the properties of this translation;

we establish proof techniques on Aπ to reason about references.

The calculus with references, π ref , has constructs for reading from a reference, writing on a reference, and a swap operation for atomically reading on a reference and placing a new value onto it. Modern computer architectures offer hardware instructions similar to swap, e.g., test-and-set, or control-and-swap constructs to atomically check and modify the content of a register. These constructs are important to tame the access to shared resources.

In distributed systems, swap can be used to solve the consensus problem with two parallel processes, whereas simple registers cannot [START_REF] Herlihy | Impossibility and universality results for wait-free synchronization[END_REF].

The swap construct is also suggested by the translation of references into Aπ. The pattern for accessing a reference is (x). ( n | P ). This yields four cases, depending on whether x is used in P and whether x is equal to n: n = x n = x x free in P swap read x not free in P write useless read D. Hirschkoff, E. Prebet and D. Sangiorgi

31:3

We define a type system in Aπ to capture the intended pattern of usage of names that represent references, called reference names, in particular the property that there is always a unique output message available at these names. The type system has linearity features similar to π-calculus type systems for locks [START_REF] Kobayashi | A partially deadlock-free typed process calculus[END_REF] or for receptiveness [START_REF] Sangiorgi | The name discipline of uniform receptiveness[END_REF].

Imposing a type system has consequences on behavioural equivalences. Since the set of legal contexts becomes smaller, the behavioural equivalence itself becomes coarser. For instance, in the case of reference names, a process P is supposed to be tested only in a context that guarantees that all references mentioned in P are 'allocated' (thus, an input at a reference name is never 'stuck', as an output message at must always exist). A consequence of these is a read in which the value read is not used is irrelevant (see formally law [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF]).

In both calculi, as behavioural equivalence we use barbed congruence and barbed equivalence.

These equivalences equate processes which, roughly, in all contexts give rise to 'matching reductions'.

We establish an operational correspondence between the behaviour of a process in π ref and its encoding in Aπ, and from this we establish full abstraction of the translation of π ref into Aπ with respect to both barbed equivalence and barbed congruence in the two calculi.

We then investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness. This bisimilarity is similar to, but not the same as, asynchronous bisimilarity. For instance, it is defined on 'reference-closed' processes (intuitively, processes in which all references are allocated); therefore inputs on reference names from the tested processes are not visible (because such inputs are supposed to consume the unique output message at that reference that is present in the tested processes). The output clause of bisimilarity on reference names is also different, as we have to make sure that the observer respects the pattern of usage for reference names; thus the observer consuming the output message on a reference name should immediately re-install an output on .

The second bisimilarity is more efficient because it does not require processes to be 'reference-closed'. Thus output messages on reference names consumed by the observer need not be immediately re-installed. However sometimes access to a certain reference is needed by a process in order to answer the bisimulation challenge from the other process. And depending on the content of such references, further accesses to other references may be needed. Since we wish to add only the needed references, this introduces an inductive game, in which a player requires a reference and the other player specifies the content of such reference, within the coinductive game of bisimulation. We show that the resulting bisimilarity is sound, and leave completeness as an open problem. Finally, we discuss examples of uses of the bisimilarities.

Related Work.

The classic encoding of references in the π-calculus [15] follows their encoding into CCS [START_REF] Milner | Communication and concurrency[END_REF]: a reference is a stateful recursive process, which may be interrogated using two names, one for read operations, the other for write operations. Properties of this encoding have been explored [START_REF] Röckl | A pi-calculus process semantics of concurrent idealised ALGOL[END_REF], comparing the π-calculus to Concurrent Idealised Algol [START_REF] Brookes | The Essence of Parallel Algol[END_REF], an extension of Idealised Algol [START_REF] Reynolds | The essence of ALGOL[END_REF] with shared variables concurrency. The encoding has been shown to be sound but not complete.

Many works have studied the effect of type systems on behavioural equivalence, formalised using both barbed congruence and labelled bisimilarity. (See the references in the books [START_REF] Sangiorgi | The pi-calculus: a Theory of Mobile Processes[END_REF][START_REF] Hennessy | A distributed Pi-calculus[END_REF]). To our knowledge, no such study has been done regarding the discipline for reference names which we use in this work. This discipline bears similarities with receptiveness [START_REF] Sangiorgi | The name discipline of uniform receptiveness[END_REF],

C O N C U R 2 0 2 0 31:4
On the Representation of References in the pi-calculus which is also related to the results in [START_REF] Sangiorgi | Typed pi-calculus at work: A Correctness Proof of Jones's Parallelisation Transformation on Concurrent Objects[END_REF][START_REF] Merro | Mobile objects as mobile processes[END_REF]. We can also remark that our notion of complete processes is reminiscent of the notion of catalysers used by Dezani et al. [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF] in session types to enforce progress.

Section 5 discusses further related work.

Paper outline. In Section 2, we introduce π ref and discuss examples of behavioural equivalences between π ref processes. In Section 3 we present Aπ with reference names, using a type system that captures the usage of such names. We show the encoding of π ref into such Aπ and prove its full abstraction for barbed equivalence and congruence. In Section 4 we introduce the two new labelled bisimilarities for Aπ, we establish soundness and completeness for one and soundness for the other (we conjecture that also completeness holds), and present a useful 'up-to' technique for the second one. Finally we illustrate the benefits of using the proof techniques based on the labelled bisimilarities of Aπ on some examples.

Asynchronous Processes Accessing References: π ref

In this section, we introduce π ref , the asynchronous π-calculus extended with primitives to interact with memory locations.

Syntax and Semantics

We assume an infinite set Names of names and a distinct infinite set Refs of references.

These sets do not contain the special symbol , that stands for the constant "unit". We use The operators in the first line are the standard π-calculus constructs for the inactive process, input, asynchronous output, replication, parallel composition, name restriction, and matching (however matching here is defined on both names and references). In the second line, we find the operators to handle references: reference restriction, or allocation (creating a new reference with initial value n), write (setting the content of to n), read (reading in

x the value of ), swap (atomically reading on x and replacing the content of the reference with n).

As usual, we often omit 0, and abbreviate a as a (and similarly for inputs a. P ). We use a tilde, •, for (possibly empty) finite tuples; then (ν a) is a sequence of restrictions; and

(ν L) a sequence of reference allocations (i.e., a piece of store), using L to represent a single allocation such as = n. Given the binders (νa)P and (ν = n)P (for a and , respectively), a(x). P , (x). P and n(x) (for x), we define bn(O), fn(O) (resp. fr(O), br(O)), for the bound and free names (resp. references) of some object O (process, action, etc.). The set of names of O is defined as the union of its free and bound names; and analogously for references. In a(x). P or a x , name a is the subject whereas x is the object.

We assume the calculus is simply-typed. Any basic type system for the π-calculus would do. In this paper, we assume Milner's sorting: names and references are partitioned into a collection of types (or sorts). Name types contain names, and reference types contain references. Then a sorting function maps types onto types. If a name type s is mapped R-Equiv:

P ≡ P P -→ Q Q ≡ Q P -→ Q R-Ctxt: P -→ P E[P ] -→ E[Q] R-Comm: a(x). P | a n -→ P {n/x} R-Read: , n / ∈ br(ν L) (ν = n)(ν L)( (x). P | Q) -→ (ν = n)(ν L)(P {n/x} | Q) R-Write: , n / ∈ br(ν L) (ν = m)(ν L)( n. P | Q) -→ (ν = n)(ν L)(P | Q) R-Swap: , n, m / ∈ br(ν L) (ν = m)(ν L)( n(x). P | Q) -→ (ν = n)(ν L)(P {m/x} | Q) Figure 1 π ref , reduction relation
onto a type t, this means that names in s may only carry, or contain, objects in t; if s is a reference type then only objects of type t may be stored in s. We shall assume that there is a sorting system under which all processes we manipulate are well-typed. For simplicity we use simple types; e.g., the sorting is non-recursive (meaning that the graph that represents the sorting function, in which the nodes are the types, does not contain cycles). In the remainder we assume that all objects (processes, contexts, actions, etc.) respect a given sorting.

The definition of structural congruence, ≡, is the expected one from the π-calculus, treating the (ν = n) operator like a restriction (see Appendix B.1).

Contexts, ranged over by C, are process expressions with a hole [ ] in it. We write C [P ] for the process obtained by replacing the hole in C with P . Active (or evaluation) contexts, ranged over by E, are given by:

E ::= [ ] E | P (νa)E (ν = n)E .
The reduction relation -→ is presented in Figure 1. It uses active contexts to isolate the subpart of the term that is active in a reduction. We write =⇒ for the 'multistep' version of -→, whereby P =⇒ P if P may become P after a (possibly empty) sequence of reductions.

Rules R-Read, R-Write and R-Swap in Figure 1 describe an interaction between the process and a reference . These rules make use of a store (ν L); this is necessary because there might be references that depend on , and as such cannot be moved past the restriction on . An example is (ν = a)(ν = ) b. P : the write operation is executed by applying rule R-Write, with (ν L) = (ν = ), as the restriction on cannot be brought above the restriction on . We recall that br(ν L) are the references bound by the ν.

As usual in concurrent calculi, the reference behavioural equivalence will be barbed congruence (in its variant sometimes called reduction-closed barbed congruence), a form of bisimulation on reduction that uses closure under contexts and simple observables. In the context closure, however, we make sure that all references mentioned in the tested process have been allocated. As often in π-calculi, we also consider barbed equivalence, that uses only active contexts. The restriction to closing contexts (as opposed to arbitrary contexts) yields laws such as

C O N C U R
(x).P ∼ =ref P, (1)
whenever x / ∈ fn(P ). Closing contexts ensure that the reading on is not blocking, and therefore possible observables in P are visible on both sides.

As the quantification on contexts refers to the free references of the tested processes, transitivity of barbed congruence and equivalence requires some care. As usual in the π-calculus, barbed equivalence is not preserved by the input construct, and the closure of barbed equivalence under all (well-typed) substitutions coincides with barbed congruence.

Behavioural Equivalence in π ref : Examples

We present a few examples that illustrate some subtleties of behavioural equivalence in The first example shows that processes may be equivalent even though the store is public and holds different values. (In the example, the reference is actually restricted, but the process P underneath the restriction, representing an observer, is arbitrary).

Example 3. For any P , we have P 1 ∼ =ref P 2 , for

P 1 def = (ν = a)(P | ! a | ! b) P 2 def = (ν = b)(P | ! a | ! b)
In the second example, the write on top of P is not blocking, provided that the same writing is anyhow possible, and provided that the current value of the store can be recorded.

Example 4. We have P 1 ∼ =ref P 2 , for

P 1 def = b. P | ! b | ! (x). x P 2 def = P | ! b | ! (x). x
On the left, it would seem that P runs under a store in which contains b; whereas on the right, P could also run under the initial store, where could contain a different value, say a.

However the component ! (x).

x allows us to store a in x and then write it back later, thus overwriting b.

Example 5. We have P s ∼ = e ref Q s , where

P s def = (νt) b. (t | !t. a. (c | b. (t | c))) Q s def = (νt) a. (t | !t. b. (c | a. (t | c)))
The discriminating context being large, the formal discussion is moved in Appendix A.

Intuitively, P s and Q s are refinements of the processes in Example 3, in that their initial writes store different values on the reference , but both processes maintain the capability of writing both values in . The difference with Example 3 are the additional inputs and outputs on name c, which are generated along the transitions. These allow an observer to distinguish P s from Q s by exploiting the swap construct. We informally explain the reason.

If the two processes have written the same value, say a, in , then Q s has generated the same number of inputs and outputs on c, while P s must have generated an extra output. An observer can use swap to read the content of , so to check that the value is indeed a, and write back a fresh name, say e. Now the observer can tell that P s has an extra output on c:

process Q s cannot add a further output, because this would require overwriting e in , which can be tested by the observer at the end.

We have seen in Example 3 two equivalent processes whose initial store (a single reference) is different. The equivalence holds intuitively because the values that the two processes can store are the same. Using two references, it is possible to complicate the example. In Example 6, the processes are equivalent and yet the pairs of values that may be simultaneously stored in the two references are different for the two processes. For each reference separately, the set of possible values is the same. But setting a reference to a certain value implies first having set the other reference to some specific values. (The processes could be distinguished if an observer had the possibility to simultaneously read the two references.) Example 6. Consider two references 1 , 2 where booleans (represented as 0,1 below) can be stored. Then for any P , we have P 1 ∼ =ref P 2 , where

P 1 def = (ν 1 = 0, 2 = 0)(P | (νt)(t | !t. 1 1. 1 0. 2 1. 2 0. t)) P 2 def = (ν 1 = 0, 2 = 0)(P | (νt)(t | !t. 1 1. 2 1. 1 0. 2 0. t))
P 1 and P 2 can write 0 and 1 in references 1 and 2 , but not in the same order. By doing so, we see that if P 1 loops, the content of 1 and 2 will evolve thus: (0, 0) → (1, 0) → (0, 0) → (0, 1) → (0, 0), while for P 2 the loop is different: (0, 0) → (1, 0) → (1, 1) → (0, 1) → (0, 0).

In particular, P 2 can always go through the state (1, 1), independently of the transitions of P , while P 1 cannot, in general, reach this state.

The example above relies on the fact that the domain of possible values for 1 and 2 is finite. A more sophisticated example, without such assumption, is given in the Appendix A.

Mapping π ref onto the Asynchronous π-calculus

We present the encoding of π ref into Aπ, which follows the folklore encoding of references into Aπ.

The Asynchronous π-calculus

Below is the grammar of the asynchronous π-calculus, Aπ; we reuse all notations from π ref .

P ::= 0 n(x). P !P n m P

-there is Q such that Q μ = ⇒ Q and P R Q ; -µ = n m and there is Q such that Q | n m = ⇒ Q and P R Q .
Asynchronous bisimilarity, ≈ a , is the largest asynchronous bisimulation.

Theorem 8 ([1]

). Relations ∼ = e a and ≈ a coincide.

Encoding π ref

In π-calculi such as Aπ, there are no references, only names. To make the encoding easier to read, we assume however that the set of names contains the set of references

{ , • • • } of π ref .
We call such names reference names, and call plain names the remaining names. Reference names will be used to represent the references of π ref .

The encoding E • , from π ref to Aπ, is a homomorphism on all operators (thus, e.g.,

E P 1 | P 2 def = E P 1 | E P 2
, and E a(m). P def = a(m). E P ), except for reference constructs for which we have:

E (ν = m). P def = (ν )( m | E P ) E v. P def = (_). ( v | E P ) E (x). P def = (x). ( x | E P ) E n(x). P def = (x). ( n | E P )
(We write (_). Q for an input whose bound name does not appear in Q.) In the encoding, an object m stored at reference is represented as a message m . Accordingly, the encoding of a write v. P is (_). ( v | E P ), meaning that the process acquires the current message at (which is thus not available anymore) and replaces it with an output with the new value.

The encoding of a read (x). P follows a similar pattern, this time however the same value is received and emitted: (x). ( x | P ). The encoding of swap combines the two patterns.

Types and Behavioural Equivalences with Reference Names

To prove a full abstraction property for the encoding, we use types to formalise the behavioural difference between reference names and plain names in the asynchronous π-calculus. The typing discipline can be added onto any basic type system for the π-calculus. As for π ref , we follow Milner's sorting. The types of the sorting impose a partition on the two sets of names (reference names and plain names). Thus we assume such a sorting, under which all processes are well-typed. We separate the base type system (Milner's sorting) from the typing rules for reference names so as to show the essence of the latter rules. Accordingly, we only present the additional typing constraints for reference names.

We write: RefTypes for the the set of reference types (i.e., types that contain reference names); Type(n) is the type of name n; ObType(n) is the type of the objects of n (i.e., the type of the names that may be carried at n). For example in well-typed processes such as n m and n(m). P , name m will be of type ObType(n).

TNil ∅ 0 TOut ∅ a m TInp ∅ P ∅ a(x). P TRep ∅ P ∅ !P TPar ∆ 1 P ∆ 2 Q ∆ 1 ∆ 2 P | Q TResN ∆ P ∆ (
∆ -x as abbreviation for ∆ -{x}. Moreover ∆ 1 ∆ 2 is defined only when ∆ 1 ∩ ∆ 2 = ∅, in which case it is ∆ 1 ∪ ∆ 2 ; we write ∆, x for ∆ {x}.
The type system is presented in Figure 2. Judgements have the form ∆ P , where P is an Aπ process. Rule TRefO along with Rule TPar ensures that every reference names in ∆ appears in subject of exactly one unguarded output. Rule TResR ensures that new reference names are always in ∆ while Rule TRefI ensures that ∆ is constant after a communication between references (by re-emitting an output after one has been consumed).

Intuitively, if ∆ P , then P must make available the names in ∆ immediately and exactly once in output subject position. We say that is output receptive in P if there is exactly one unguarded output at , and moreover this output is not underneath a replication. Then ∆ P holds if any ∈ ∆ is output receptive in P ;

in any subterm of P of the form (ν )Q or (m). Q, name is output receptive in Q.

This intuition is formalised in Lemma 9, and in Proposition 10 that relates types and operational semantics.

Typing is important because it allows us to derive the required behavioural equivalences.

For instance, allowing parallel composition with the ill-typed process (x). 0 would invalidate barbed equivalence between the (translations of the) terms in law (1).

In the remainder of the paper, it is assumed that all processes are well typed, meaning that each process P obeys the underlying sorting system and that there is ∆ s.t. ∆ P holds. Two processes P, Q are type-compatible if both ∆ P and ∆ Q, for some ∆; we write ∆ P, Q in this case. In the remainder of the paper, all relations are on pairs of type-compatible processes. Similarly, all compositions (i.e., of a context with processes) and actions are well-typed.

The type system satisfies standard properties, like uniqueness of typing (∆ P and ∆ P imply ∆ = ∆ ), and preservation by structural congruence (P ≡ Q and ∆ P imply ∆ Q). As claimed above, if ∆ P , then names in ∆ are output receptive: 5. if µ = m or µ = (νb) b , then ∆ -P .

Lemma 9. If ∆, P then P ≡ (ν ñ)( m | Q), with ∈ ñ,

if µ = (ν )

, then (∆ -), P .

We can remark that in case 3, we have / ∈ ∆, as otherwise the context would not be able to trigger an input (since, by typing, it could not generate an output on ).

Barbed congruence.

As usual in typed calculi, the definitions of the barbed relations take typing into account, so that the composition of a context and a process be well-typed. In the case of reference names, an additional ingredient has to be taken into account, namely the accessibility of reference names. If a process has the possibility of accessing a reference, then a context in which the process is tested should guarantee the availability of that reference.

For this, we define the notion of completing context and complete process. Then, roughly, barbed congruence becomes "barbed congruence under all completing contexts".

A process P is complete if each reference name that appears free in P is 'allocated' in P .

We write frn(P ) for the set of free reference names in P . This typed barbed equivalence is the behavioural equivalence we are mainly interested in.

The reference name discipline weakens the requirements on names (by limiting the number of legal contexts), hence the corresponding typed barbed relation is coarser. We are not aware of existing works in the literature that study the impact of the reference name discipline on behavioural equivalence.

Lemma 14. For all compatible P , Q, P ∼ = e a Q (and hence also P ≈ a Q) implies P ∼ = e Arn Q.

We show in Section 4 that the inclusion is strict.

Validating the Encoding

We now show that the two notions of barbed congruence coincide via the encoding.

Theorem 15 (Operational correspondence). If P -→ P , then E P -→ E P .

Conversely, if E P -→ Q, then P -→ P , with E P ≡ Q.

The next lemma shows that, up to asynchronous bisimilarity, we can 'read back' well-typed processes in Aπ, via the encoding, as processes in π ref .

And similarly for contexts.

Lemma 16. If ∅ P , then there exists R in π ref such that E R ≈ a P .

Theorem 15 and Lemma 16 are the main ingredients to derive the following theorem:

Theorem 17 (Full abstraction). For any P, Q in π ref :

P ∼ =ref Q iff E P ∼ =Arn E Q ; and similarly P ∼ = e ref Q iff E P ∼ = e Arn E Q . 4
Bisimulation with Reference Names

Two Labelled Bisimilarities

In this section we present proof techniques for barbed equivalence based on the labelled transition semantics of Aπ. For this we introduce two labelled bisimilarities.

The first form of bisimulation, reference bisimilarity, only relates complete processes; processes that are not complete have to be made so. Intuitively, in this bisimilarity processes are made complete by requiring a closure of the relation with respect to the (well-typed) addition of output messages at reference names (the 'closure under allocation' below).

Moreover, when an observer consumes an output at a reference name, say n , then, following the discipline on reference names, he/she has to immediately provide another such output message, say m . This is formalised using transition notations such as

P n [m]
-----→ P , which makes a swap on (reading its original content n and replacing it with m). As a consequence of the appearance of such swap transitions, ordinary outputs at reference names are not observed in the bisimulation. Similarly for inputs at reference names: an input P m ---→ P from a complete process P is not observed, since it is supposed to interact with unique output at contained in P (which exists as P is complete). Finally, an observer should respect the completeness condition by the processes and should not communicate a fresh reference name -to communicate such a reference, say , an allocation for (an output message at ) has first to be added. --------→ P . Then, as usual, P

A relation R is closed under allocation if P R Q implies P | n R Q | n
n [m] = ==== ⇒ P holds if P = ⇒ P n [m]
-----→ P = ⇒ P for some P , P , and similarly for P

(νn) n [m]
= ======= ⇒ P .

We let α range over the actions µ plus the aforementioned 'update actions' n [m] and

(νn) n [m].
Setting m to be the object of an update actions, we write ∆ α when: (i) if the object of α is a free reference name then it is in ∆, and (ii) α is not an input or an output at a reference name.

Definition 18 (Reference bisimilarity). A symmetric relation R closed under allocation is a

reference bisimulation if whenever P R Q with P, Q complete, ∆ P, Q and P

that Q α = ⇒ Q and P R Q for some Q 2. or α is an input a m and Q | a m = ⇒ Q with P R Q for some Q .
Reference bisimilarity, written ≈, is the largest reference bisimulation.

We now show that ≈ coincides with barbed equivalence. The structure of the proof is standard, however some care has to be taken to deal with closure under parallel composition.

Lemma 19. If P ≈ Q, and ∅ R, then P | R ≈ Q | R.
Proposition 20 (Substitutivity for active contexts).

If P ≈ Q, then E[P ] ≈ E[Q] for any active context E.
Theorem 21 (Labelled characterisation).

P ≈ Q iff P ∼ = e Arn Q.
In reference bisimilarity, the tested processes are complete: hence all their references must explicitly appear as allocated, and when a reference is accessed, an extension of the store is made so to remain with complete processes (and if such an extension introduces other new references, a further extension is needed). The goal of the bisimilarity ≈ ip below is to allow one to work on processes with open references, and make the extension of the store only when necessary. The definition of the bisimulation exploits an inductive predicate to accommodate finite extensions of the store, one step at a time. This predicate can be thought of as an inductive game, in which the 'verifier' can choose rule Base and close the game, or choose rule Ext and a reference ; in the latter case the 'refuter' chooses the value stored in .

Definition 22 (Inductive predicate). The predicate ok(∆, R, P, Q, µ) (where ∆ is a set of names, R a process relation, P, Q processes, and µ an action) holds if it can be proved inductively from the following two rules: The names in ∆ ∪ ∆ are the reference names that appear in output subject position in P or Q. Therefore, when using rule Ext of the inductive predicate, the condition / ∈ ∆ ensures us that the message at can be added without breaking typability.

Base Q | n m = ⇒ Q for µ = n m Q µ = ⇒ Q otherwise P R Q ok(∆, R, P , Q, µ) Ext / ∈ ∆ ∀ m : ok((∆, ), R, P | m , Q | m , µ) ok(∆,
The following up-to technique allows us to erase common messages on reference names along the bisimulation game.

For this, we use the notation M s , where s is a finite list of pairs ( ,m), to describe parallel compositions of outputs on reference names (i.e., M s def = ( ,m)∈s m ), and ∆ s M s where ∆ s contains all first components of pairs of s. Intuitively, M s represents a chunk of store.

Definition 24 (≈ ip -bisimulation up to store). An ≈ ip -bisimulation up to store is defined like Base-Up

≈ ip -
P ≡ P | M s Q | n m = ⇒≡ Q | M s for µ = n m Q µ = ⇒≡ Q | M s otherwise P R Q ok (∆, R, P , Q, µ)
Rule Base-Up makes it possible to erase common store components before checking that the processes are related by R.

Proposition 25. If R is a ≈ ip -bisimulation up to store, then R⊆ ≈ ip .
Proposition 26 (Soundness of ≈ ip ). ≈ ip ⊆ ≈.

Intuitively, the inclusion holds because a ≈ ip -bisimulation is closed by parallel composition with M s processes. We leave the opposite direction, completeness, as an open issue.

Examples

We now give examples of uses of the various forms of labelled bisimulation (≈ a , ≈, ≈ ip , ≈ ip up to store) for Aπ to establish equivalences between processes with references. In some cases, we use the 'up-to structural congruence' (≡) version of the bisimulations -a standard 'up-to' technique. In the examples we consider barbed equivalence; the results can be lifted to barbed congruence using closure under substitutions.

The first example is about a form of commutativity for the write construct. We can derive P 1 ≈ a P 2 , using the singleton relation R def = {(P 1 , P 2 )}, and showing that R is an asynchronous bisimilarity up-to context and structural congruence [START_REF] Pous | Advanced Topics in Bisimulation and Coinduction[END_REF] (this known 'up-to' technique allows one to remove additional processes created from the replications after a transition). We can then conclude by Lemma 14.

We now consider Examples 3 and 4 from Section 2.

Proof of Example 3.

Let R 1 , R 2 be the encodings of P 1 , P 2 in the example:

R 1 def = (ν ) a | E P | ! (_). a | ! (_). b R 2 def = (ν ) b | E P | ! (_). a | ! (_). b We then have R 1 =⇒≡ R 2 and R 2 =⇒≡ R 1 , which implies R 1 ≈ a R 2 (
where ≈ a is asynchronous bisimilarity), as {(R 1 , R 2 )} ∪ I, where I = {(P, P )} is the identity relation, is an asynchronous bisimulation up to ≡. We can then conclude by Theorems 8 and 17.

Proof of Example 4.

Let R 1 , R 2 be the encodings of P 1 , P 2 in the example:

R 1 def = (_). ( b | E P ) | ! (_). b | ! (x). ( x | (_). x ) R 2 def = E P | ! (_). b | ! (x). ( x | (_). x ) C O N C U R 2 0 2 0

31:14 On the Representation of References in the pi-calculus

Then for all m, processes m | R 1 and m | R 2 are complete. We define

R def = { R 1 | m | B X , R 2 | m | B X } ,
where X def = {x 1 , . . . , x n } is a possibly empty finite set of names, and

B X def = (_). x 1 | . . . | (_). x n Then R ∪ I is a ≈ ip -bisimulation.
Reusing the same notations,

R def = { R 1 | B X , R 2 | B X } is an ≈ ip -bisimulation up to
store: this up-to technique allows us to remove the m particles.

The following example shows some benefits of using ≈ ip and ≈ ip up to store in the proof of a property that generalises (the Aπ version of) law ( 1), which involves a 'useless read'.

Example 28. Consider ∅ P 0 R Q 0 , where R is an asynchronous bisimulation, ObType( ) ∈

RefTypes, and x is a fresh name. Then ∅ (x).

(P 0 | x ) ≈ Q 0 .
In general, (x). (P 0 | x ) and Q 0 are not related by ≈ a (take

P 0 = Q 0 = a n ), thus
the inclusion in Lemma 14 is strict.

To prove (x). (P 0 | x ) ≈ Q 0 using a ≈-bisimulation, we need a relation such as

R 1 def = {( (x). (P 0 | x ), Q 0 )} ∪ {( (x). (P 0 | x ) | | m , Q 0 | | m ) for any m} ∪ {( (x). (P 0 | x ) | | m | M s , Q 0 | | m | M s ) for any m, M s } ∪ {P | | m | M s , Q | | m | M s ) for any m, M s , with P R Q} and prove that R 1 ∪ R -1 1 (where R -1 1 is the inverse of R 1 ) is a ≈-bisimulation.
We can simplify the proof and avoid the several quantifications in R 1 (in particular on M s , whose size is arbitrary), and prove that R 2 is an ≈ ip -bisimulation, for

R 2 def = R ∪ {(P | m , Q | m ), for any m, with P R Q} ∪ {( (x). (P 0 | x ), Q 0 ), (Q 0 , (x). (P 0 | x ))}.
The last component of R 2 is dealt with using rule Ext of the inductive predicate (Definition 22), and this brings in the second component (the closure of R under messages on ).

We can simplify the proof further, by removing such second component, and show that R 3 is an ≈ ip -bisimulation up to store, for

R 3 def = R ∪ {( (x). (P 0 | x ), Q 0 ), (Q 0 , (x). (P 0 | x ))}.

Future work

In languages with store, which are usually sequential languages, bisimulation is commonly defined on configurations. In π ref , a configuration would be written (ν n) P, s , where s is an explicit store and n is a set of private names shared between process P and store s. We could in principle read back ≈ onto π ref , and define a behavioural equivalence between π ref configurations. The LTS on configurations would then have specific actions to describe how an observer may act on the visible part of the store. The labelled transition semantics for π ref and π ref configurations would however be more complex than those for Aπ; for instance the forms of actions, expressing external observations, would be much broader.

The swap operation arises naturally in the encoding into Aπ. We do not know if and how swap increases the discriminating power of external observers. We believe that, without swap, the two processes in Example 5 could not be distinguished. This point deserves further investigation, which we leave for future work. Similarly we leave for future work proving or disproving the completeness of the bisimilarity with an inductive predicate (Definition 23).

It would be interesting to see if the labelled bisimilarities we have considered, whose bisimulation clauses are different from those of ordinary bisimilarity, can be recovered in an abstract setting, e.g., using coalgebras [START_REF] Jacobs | Introduction to coalgebra. towards mathematics of states and observations[END_REF][START_REF] Bonchi | A general account of coinduction up-to[END_REF][START_REF] Rot | Enhanced coalgebraic bisimulation[END_REF]. This would be particularly interesting for ≈ ip -bisimulation, whose definition involves a mixture of induction and coinduction.

Equivalences for higher-order languages with state are known to be hard to establish.

Various approaches exist, from Kripke logical relations to trace semantics and game semantics [START_REF] Hur | The marriage of bisimulations and kripke logical relations[END_REF][START_REF] Jaber | Trace semantics for polymorphic references[END_REF][START_REF] Murawski | Full abstraction for reduced ML[END_REF][START_REF] Castellan | Non-angelic concurrent game semantics[END_REF]. It would be interesting to compare the proof techniques offered by these approaches with those shown in this paper, and developments of them. More generally, more experimentation is needed to test the bisimilarities proposed in this paper and the associated proof techniques, on examples from high-level languages that include higher-order features, mutable state, and concurrency.

A Additional Material for the Examples in Section 2.2

Proof of Example 5. To get a idea of how P s and Q s evolve, let us consider first

E def = (ν = z)[ ]. Then E[Q s ]
can reduce to one of the following:

1. (ν = z)(νt) a. (t | !t. b. (c | a. (t | c))) 2. (ν = a)(νt)(t | !t. b. (c | a. (t | c))) | c n | c n 3. (ν = a)(νt)( b. (c | a. (t | c)) | !t. b. (c | a. (t | c))) | c n | c n 4. (ν = b)(νt)( a. (t | c) | !t. b. (c | a. (t | c))) | c n | c n+1 .
Similarly, E[P s ] can reduce to those four processes but with the role of a and b swapped.

Notice that when E[Q s ] =⇒ Q , then there is a correspondence between the value stored in (i.e a or b) and the presence of more c processes than c processes (or the same number).

We now consider the following context:

E 0 def = (ν = z)([ ] | z(x). [x = b]s 0 . s 1 . (P 11 | P 12 ) | s 0 | s 1 ) P 11 def = (x). [x = z]s 11 | s 11 P 12 def = c. (x). [x = z]s 12 | s 12
with s 0 , s 11 , s 12 fresh names.

At first s 0 and s 1 are the only observables, meaning E 0 [P s ] ↓ s0 and E 0 [P s ] ↓ s1 , but then

E 0 [P s ] -→-→-→ (ν = z)((νt)(t | !t. a. (c | b. (t | c))) | s 1 . (P 11 | P 12 ) | s 1 ) def = P
where the three reductions have been derived using rules R-Write, R-Swap, and R-Comm respectively. Finally, we have P ⇓ s0 , whereas P ↓ s1 .

Thus, to avoid the observable s 0 , process E 0 [Q s ] must reduce to a process with b stored in before doing the swap in E 0 . This implies that the swap is executed in a state that corresponds to case 4 above. So for any

Q with E[Q s ] =⇒ Q and Q ↓ s0 and Q ⇓ s1 , such
process Q has one of the following forms:

1. Q 1 def = (ν = a)((νt)(t | !t. b. (c | a. (t | c)) | c n | c n ) | s 1 . (P 11 | P 12 ) | s 1 ) 2. Q 2 def = (ν = a)((νt)( b. (c | a. (t | c)) | !t. b. (c | a. (t | c)) | c n | c n ) | s 1 . (P 11 | P 12 ) | s 1 ) 3. Q 3 def = (ν = b)((νt)( a. (t | c) | !t. b. (c | a. (t | c)) | c n | c n+1 ) | s 1 . (P 11 | P 12 ) | s 1 ) 4. Q 4 def = (ν = z)((νt)( a. (t | c) | !t. b. (c | a. (t | c)) | c n | c n+1 ) | s 1 . (P 11 | P 12 ) | s 1 )
Then we use either P 11 or P 12 depending on the form of Q . If Q is of the first three forms, then we use P 11 .

Indeed, P -→-→ (ν = z)((νt)(t | !t. a. (c | b. (t | c))) | P 12 ) def = P using rules
R-Read and R-Comm respectively. Notice that P ⇓ s11 . On the other hand, z does not appear anywhere else than in a matching in Q , thus there is no reduction

Q =⇒ Q with Q ↓ s11
for any Q .

In the other case, it holds that

Q 4 -→-→-→ (ν = z)((νt)( a. (t | c) | !t. b. (c | a. (t | c)) | c n | c n ) | P 11 ) def = Q using rules R-Comm, R-Read, and R-Comm respectively.
Then we have Q ⇓ s12 . However, the only output c is behind a write a in P . Thus, there is no P =⇒ P with P ↓ s12 .

We can finally conclude

P s ∼ =ref Q s .
Proof of Example 6. Recall the definitions of the two processes (we rename the processes that are given in the main text, to ease readability):

P def = (ν 1 = 0, 2 = 0)(R | (νt)(t | !t. 1 1. 1 0. 2 1. 2 0. t)) Q def = (ν 1 = 0, 2 = 0)(R | (νt)(t | !t. 1 1. 2 1. 1 0. 2 0. t)) C O N C U R 2 0 2 0

31:18 On the Representation of References in the pi-calculus

To prove their equivalence, we introduce the following processes:

P def = !t. 1 (_). ( 1 1 | 1 (_). ( 1 0 | 2 (_). ( 2 1 | 2 (_). ( 2 0 | t)))) Q def = !t. 1 (_). ( 1 1 | 2 (_). ( 2 1 | 1 (_). ( 1 0 | 2 (_). ( 2 0 | t)))) P 1 = Q 1 def = t P 2 def = 1 (_). ( 1 1 | 1 (_). ( 1 0 | 2 (_). ( 2 1 | 2 (_). ( 2 0 | t)))) Q 2 def = 1 (_). ( 1 1 | 2 (_). ( 2 1 | 1 (_). ( 1 0 | 2 (_). ( 2 0 | t)))) P 3 def = 1 (_). ( 1 0 | 2 (_). ( 2 1 | 2 (_). ( 2 0 | t))) Q 3 def = 2 (_). ( 2 1 | 1 (_). ( 1 0 | 2 (_). ( 2 0 | t))) P 4 def = 2 (_). ( 2 1 | 2 (_). ( 2 0 | t)) Q 4 def = 1 (_). ( 1 0 | 2 (_). ( 2 0 | t)) P 5 = Q 5 def = 2 (_). ( 2 0 | t)
P and Q are the encodings of the replicated part of P and Q. Then P i and Q i are the processes that can be reached from P and Q .

We now show that the relation R ∪ R -1 is an ≈ ip -bisimulation where we have:

R def = ( 1 n 1 | (νt)(P | P i ), 1 n 1 | (νt)(Q | Q j )) for any n 1 , n 1 ∈ {0, 1}, i, j ∪ ( 2 n 2 | (νt)(P | P i ), 2 n 2 | (νt)(Q | Q j ))
for any n 2 , n 2 ∈ {0, 1}, i, j

∪ ( 1 n 1 | 2 n 2 | (νt)(P | P i ), 1 n 1 | 2 n 2 | (νt)(Q | Q j )) for any n 1 , n 1 , n 2 , n 2 ∈ {0, 1}, i, j
First, note that the only free names appearing in those processes are 1 and 2 . Thus for any P R Q, the only actions to consider are τ, i n and i n , for i = 1, 2.

For any P R Q, we have:

If P τ -→ P 0 , then P 0 R Q If P i n ---→ P 0 , then P 0 R Q | i n If P i n ---→ P 0 , then either Q i n ---→ Q 0 and P 0 R Q 0 , or Q i 1-n -----→ Q 0 .
In this case, we use rule Ext (from Definition 22) to add the other location if ∆ = 1 , 2 . Then after at most 5 internal transitions (by cycling around the P i or Q j ), we obtain a process Q 0 that can make the required transition

Q 0 i n ---→ Q 0 with P 0 R Q 0 . As R ∪ R -1 is an ≈ ip -bisimulation, we have R ⊆ ≈. Moreover, (ν 1 , 2 )(E R | [ ]) is
an active context, so this implies E P ≈ E Q . By Theorems 21 and 17, we can conclude

P ∼ = e ref Q.
To extend this result to barbed congruence, we notice that for all σ,

1. either P σ = (ν 1 = 0, 2 = 0)(Rσ | (νt)(t | !t. 1 1. 1 0. 2 1. 2 0. t) 2. or P σ = (ν 1 = 0, 2 = 0)(Rσ | (νt)(t | !t. 1 0. 1 0. 2 0. 2 0. t) 3. or P σ = (ν 1 = 1, 2 = 1)(Rσ | (νt)(t | !t. 1 1. 1 1. 2 1. 2 1. t)
As P ∼ = e ref Q holds for any R, it also holds for any Rσ, which prove the first case. Moreover, the proof never uses the fact that 0 and 1 are distinct, so we can prove in the same way that cases 2 and 3 hold.

We conclude P ∼ =ref Q.

We now present an additional example, which corresponds to a generalisation of Example 6.

Example 29. Here we remove the assumption that the two references can only hold values 0 and 1. This enables the context to store fresh names in references. If used with the original processes, these are distinguished by using those fresh values to block transition along the lines of Example 5. To make these processes equivalent again, we could add in parallel a buffer as in Example 4. However, by making these additions, we would also enable P 1 to desynchronise the content in 1 and 2 and have [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF][START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF]. The solution is to prevent those buffers from writing at a different 'time' than the 'time' they have read. For this we introduce a more complex buffer B j i . Consider the following processes:

B j i def = r(x j
). 0 !r(x j ). t i . j x j (y j ). (r y j | t i )

S j i def = !t i . j (x j ). (t i | (νr)(r x j | B j i )) P def = (νt 1 , t 2 , t 3 , t 4 ) t 1 !t 1 . 1 1. t 2 | S 1 1 | S 2 1 !t 2 . 1 0. t 3 | S 1 2 | S 2 2 !t 3 . 2 1. t 4 | S 1 3 | S 2 3 !t 4 . 2 0. t 1 | S 1 4 | S 2 4 Q def = (νt 1 , t 2 , t 3 , t 4 ) t 1 !t 1 . 1 1. t 2 | S 1 1 | S 2 1 !t 2 . 2 1. t 3 | S 1 2 | S 2 2 !t 3 . 1 0. t 4 | S 1 3 | S 2 3 !t 4 . 2 0. t 1 | S 1 4 | S 2 4
We have P ∼ =ref Q. If we take

E def = (ν 1 = 0)(ν 2 = 0)[ ],
we have

E[Q] -→-→ (ν 1 = 1)(ν 2 = 1
)Q for some Q . However, there is no sequence of reductions such that E[P ] =⇒ (ν 1 = 1)(ν 2 = 1)P for any P .

If we forget all S j i 's, then these processes are similar to the 'loop' used in the previous example but split into multiple replications. Those S j i 's help to equate the two processes even if the context can write any value in 1 , 2 .

Process S j i can only be activated when t i is available. It then reads the content of j to initialise a new buffer B j i .

Process B j i contains value x j i that is the object of r x j i . Process B j i can be stopped by making the communication with the first input on r, or can be used to swap its content with the content of j . Note that this swap can only be done when t i is available, so it cannot be used to desynchronise the content in 1 , and 2 .

B Definitions and Results about Aπ with references B.1 Operational Semantics of Aπ: Reduction and Labelled Transitions Reduction

Structural congruence is defined as the smallest congruence that satisfies the following axioms:

P | 0 ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R !P ≡ P P | (νn)Q ≡ (νn)P | Q if n /
∈ fn(P ) (νn)(νm)P ≡ (νm)(νn)P (νn)0 ≡ 0

[x = x]P ≡ P C O N C U R 2 0 2 0 6. if µ = (ν )
, then (∆ -), P .

Proof. We note the type of P as ∆ .

For µ = n m , we have P ≡ (ν a, )(n(x For µ = τ , we look at the interaction that has occurred. This can be mimicked using two transitions, one for the output and one for the input for which we have already proven the resulting typing. Proof. We construct R by induction on the structure of P , we only discuss the two cases below, the other cases are immediate.

For ∅ (ν )P , we know that P so we have two cases according to Lemma 9: Up-to techniques ease the task of proving bisimilarity between processes. Informally, the general idea is to use an extra relation (for instance ≡), and when we need to prove that P R Q, instead of proving that P R Q (for some P , Q that satisfy the required conditions), we show P ≡ R ≡ Q . This often leads to smaller relations, which are easier to check.

P
We

= ⇒ Q and P ≡R≡ Q for some Q 2. or α is an input a m and Q | a m = ⇒ Q with P ≡R≡ Q for some Q . Proposition 31. If R is a reference bisimulation up to ≡, then R ⊆ ≈.
Proof. ≡R≡ is a reference bisimulation and R ⊆ ≡R≡.

that Q α = ⇒ Q , P ≡ (ν n)P , Q ≡ (ν n)Q with P R Q for some P , Q , Q , n 2. or α is an input a m and Q | a m = ⇒ Q with P ≡ (ν n)P , Q ≡ (ν n)Q with P R Q for some P , Q , Q , n.
Lemma 34. If R is a reference bisimulation up to restriction and up to ≡, then R ⊆≈.

Proof. R def = {((ν n)P, (ν n)Q) s.t P R Q} is a reference bisimulation up to ≡.
The following lemma uses notation M s , which has been introduced before Definition 24.

Lemma 35 (Extractable store). Let ∆ P , then P ≡ (ν n)(M s | P ) with ∅ P for some M s .

Proof. We reason by induction on the structure of P . There are two cases depending on the size of ∆.

If ∆ = ∅, then nothing has to be done.

If ∆ = ∆ , , then by Lemma 9, P ≡

(ν n)( m | Q) with ∆ , ∆ Q. By induction, Q ≡ (ν n )(M s | Q ) with ∅ Q . Therefore, P ≡ (ν n, n )(M s | Q ) with M s = m | M s .
For P , this lemma can be strengthened to P ≡ (ν n)( m | M s | P ) with ∅ P .

We can now prove substitutivity for ≈ under parallel composition.

Lemma 19. If P ≈ Q, and ∅ R, then P | R ≈ Q | R.
Proof. We show that R is a bisimulation up to restriction, with

R def = {(P | R, Q | R) s.t P ≈ Q, ∅ R} R is

B.4.2 Completeness

We prove completeness. For this, we need the following lemmas. However this can only be done by doing a communication on n, thus we must have

Q ⇓ n .
Take an active context E completing for P and Q, we assume s is fresh for E, then = ======= ⇒ Q so we are done.

π

  ref . These examples will be formally treated in Section 4.2 for Examples 3 and 4, and in Appendix A for Examples 5 and 6.

1 |C

 1 P 2 (νn)P [n = m]P of References in the pi-calculus The reduction semantics, as well as barbed equivalence and congruence (written ∼ = e a and ∼ =a, respectively), are standard (defined as in π ref , and recalled in Appendix B.1). We recall the standard definition of asynchronous bisimilarity, ≈ a , from [1]. To define ≈ a , as well as the other forms of bisimilarity we introduce in Section 4, we rely on the early transition system for Aπ. In this LTS, which is presented in Appendix B.1 labels are either free inputs of the form n m (reception of name m on n), output (n m ), bound output ((νm)n m ) or internal communication (τ ). Definition 7. A symmetric relation R between processes is an asynchronous bisimulation if whenever P R Q and P µ -→ P , one of these two clauses hold:

1 . 2 . 3 .

 123 and there is no unguarded output at in Q.The following standard property relies on the standard LTS for Aπ, which is given in Appendix B.Proposition 10 (Subject reduction). If ∆ P and P µ -→ P , then C O N C U R 2 0 2 0 31:10 On the Representation of References in the pi-calculus 1. if µ = τ , µ = a m , µ = a m or µ = (νb)a b , then ∆ P . if µ = (ν )a then ∆, P . if µ = m and / ∈ ∆, then ∆, P 4. if / ∈ ∆, then ∆, P | m .

Definition 11 (

 11 Open references and complete processes). The open references of P such that ∆ P are the names in frn(P ) \ ∆; similarly the open references of processes P 1 , . . . , P n is the union of the open references of the P i 's. P is complete if it contains no open reference. frn(P ) ⊆ ∆ and ∆ P , for some ∆. A context C is completing for P if C[P ] is complete. (Note that an Aπ complete process might have free reference names, if these are not open references; in contrast, a π ref reference-closed process does not have free references.) Lemma 12. P is complete iff ∅ (ν n)P where n def = frn(P ).Completing contexts are the only contexts in which processes should be tested. We constrain the definitions of typed barbed congruence and equivalence accordingly. The grammar for the active contexts in Aπ is as expected:E ::= [ ] E | P (νn)E .Definition 13 (Barbed congruence and equivalence in Aπ with reference names). Barbed congruence is the largest symmetric relation ∼ =Arn in Aπ such that whenever P R Q then P, Q are: closed under reductions whenever they are complete; closed under the contexts that are completing for P, Q; compatible on barbs whenever they are complete. Barbed equivalence, ∼ = e Arn , is defined analogously except that one uses active contexts in place of all contexts.

  for any n such that P | n and Q | n are well-typed. We write P n [m] -----→ P if P n ---→ P and P = m | P , for some P ; similarly for P (νn) n [m]

1 .

 1 either there exists Q such

Example 27 .

 27 We wish to establish ! a. b ∼ = e ref ! b. a. For this, we prove the law ! a. b ∼ = e ref ! a | ! b, which will be enough to conclude, by commutativity of parallel composition. The two given processes are mapped into Aπ as P 1 def = ! (_). ( a | (_). b ) and P 2 def = (! (_). a ) | (! (_). b ).

B. 3

 3 P with P = (νb)P . We have ∆ P then ∆ (νb)P .P (ν )a-----→ a --→ P with P = (ν )P . We have ∆, P then ∆ (ν )P → P . We have / ∈ ∆ after the output, so we can subject reduction for the input transition. P with P = (νb)P . We have ∆ P then ∆ (νb)PP (ν )------→ ---→ P with P = (ν )P . We have ∆, P then ∆ (ν )P Properties of the encoding Lemma 16. If ∅ P , then there exists R in π ref such that E R ≈ a P .

  ≡ m | P . Thus (ν )P ≡ (ν )( m | P ) with ∅ P . By induction, we have Q with E Q ≈ a P . Therefore we have E (ν = m)Q ≈ a (ν )P . P ≡ (νm)( m | P ). We reason by induction on the type of . If m is a plain name, we can conclude as above with E (νm)(ν = m)Q . Otherwise, m is reference name and there exists R such that (νm)(ν )( m | P ) ≡ E R . As (ν )P ≡ (νm)(ν )( m | P ), we are done. For ∅ (x). P , we know that P then either P ≡ m | P with ∅ P . By induction, we have E Q ≈ a P in which case we take (x). Q or m(x). Q depending on whether m = x or not, C O N C U R 2 0 2 0 31:22 On the Representation of References in the pi-calculus or P ≡ (νm)( m | P ) and then (x). P ≈ a (νm) (x). ( m | P ) and we can refer to the first case.

Lemma 32 .

 32 If P ≈ Q, then (νn)P ≈ (νn)Q. Proof. R def = {((νn)P, (νn)Q) s.t P ≈ Q}∪ ≈ is a reference bisimulation up to ≡. Definition 33 (Bisimulation up to restriction and up to ≡). A symmetric relation R ≡-closed under allocation is a reference bisimulation up to restriction and up to ≡ if whenever P R Q with P, Q complete, ∆ P, Q and P α -→ P with ∆ α, then 1. either there exists Q such

  closed by allocation. Suppose P | R and Q | R are complete, and P | R α -→ P with ∆ α we distinguish according to the last rule used (Par, Comm or Close)If P | R α -→ P | R, first note that P, Q are complete, so either Q α = ⇒ Q and P ≈ Q or α = a m and Q | a m = ⇒ Q and P ≈ Q . In both cases, we have P | R ≈ Q | R. If P | R α -→ P | R , then Q | R α -→ Q | R . For α = τ, a m , a m , (νb)a b , we have ∅ R . The only remaining case is when α = (ν )a(by typing, R cannot perform an output on a reference). In that case,R . Thus R ≡ (ν n)(M s | R ) with ∅ R . By definition P | M s ≈ Q | M s hence P | M s | R R Q | M s | R , which is sufficient as P | R ≡ (ν n)(P | M s | R ) and Q | R ≡ (ν n)(Q | M s | R ). If P | R τ -→ P | R ,we distinguish according to the action performed by P : * For P a n ---→ P or P a n ---→ P , then R a n ---→ R and R a n ---→ R respectively, so ∅ R . The remaining part of the proof is standard π-calculus reasoning. * For P n ---→ P , then R n ---→ R with R . By Lemma 35, R ≡ (ν n)( m | M s | R ) with ∅ R . By definition, P | M s ≈ Q | M s . Moreover both processes are complete and P | M s n [m] -----→ P | m | M s . So Q | M s n [m] = ==== ⇒ Q and P | m | M s ≈ Q . As all names in subject position in M s are fresh for Q, we have Q | R τ = ⇒≡ (ν n)(Q | R ). Moreover we have P | R ≡ (ν n)(P | m | R ), thus we are done. If P | R τ -→ (νn)(P | R ), then the reasoning is similar.

Lemma 36 . 2 .

 362 If (νn)(P | s n ) ∼ = e Arn (νn)(Q | s n ) with s fresh for P and Q, thenP ∼ = e Arn Q.Proof. We show that the following relation R is included in barbed equivalence.R = {(P, Q) (νn)(P | s n ) ∼ = e Arn (νn)(Q | s n ) with s fresh} We will note P 1 = (νn)(P | s n ) and Q 1 = (νn)(Q | s n ) If P -→ P , then P 1 -→ (νn)(P | s n ) so Q 1 =⇒ Q 2 with (νn)(P | s n ) ∼ = e Arn Q But we have Q 2 ≡ (νn)(Q | s n ) and Q =⇒ Q .If P ↓ a , then we have two cases:a = n, then P 1 ↓ a so Q 1 ⇓ a meaning that Q ⇓ a as a = s. C O N C U R2 0 2 0 31:24 On the Representation of References in the pi-calculus a = n, then we consider E def = [ ] | s(x). x(_). s for a fresh s . E[P 1 ] -→-→ (νn)(P | s ) so (νn)(P | s ) ↓ s . Therefore, E[Q 1 ] =⇒=⇒⇓ s which just means that E[Q 1 ] ⇓ s .

E=→ P 1 .. 2 .. 3 . 4 . 5 . 6 .

 123456 def E | s(x). s x with s fresh is also completing for P 1 and Q 1 , soE [P 1 ] ∼ = e Arn E [Q 1 ]. We then have E [P 1 ] -→ (νn)(E[P ] | s n ), so E [Q 1 ] =⇒ Q with (νn)(E[P ] | s n ) ∼ = e Arn Q , meaning in particular that Q ↓ s and Q ⇓ s which is only possible is Q ↓ s .Moreover, we have thatE [Q 1 ] -→ (νn)(E[Q] | s(x). s x ) =⇒ Q . The same also apply symmetrically for E [Q 1 ] -→ (νn)(E[Q] | s (x). s x ) ∼ = eArn P for some P . Thus we have (νn)(E[P ] | s x ) =⇒ P ∼ = e Arn (νn)(E[Q] | s x ) =⇒ Q ∼ = e Arn (νn)(E[P ] | s x ) which implies (νn)(E[P ] | s x ) ∼ = e Arn (νn)(E[Q] | s x ).Lemma 37.If P | [x = y]s ∼ = e Arn Q | [x = y]s with x = y, then P ∼ = e Arn Q.Proof. We have [x = y]s ≈ a 0 so P | [x = y]s ≈ a P and similarly for Q. Thus by Lemma 14,P ∼ = e Arn P | [x = y]s ∼ = e Arn Q | [x = y]s ∼ = e Arn Q.This result can be extended to an arbitrary number of [x = y]s in parallel.Proof ofCompleteness. We show that ∼ = e Arn is a reference bisimulation: It is closed by allocation Take P, Q complete with F def = fn(P ) ∪ fn(Q), P ∼ = e Arn Q and P α -When α = τ , we take E def = [ ]. Then E[P ] -→ P . So we have Q =⇒ Q with P ∼ = e Arn Q When α = a(n), we take E def = [ ] | a n . Then E[P ] -→ P . So we have Q | a n =⇒ Q with P ∼ = e Arn Q When α = a n , we take E def = [ ] | a(x). [x = n]s | s with s fresh. Then E[P ] -→-→ P with E[P ] ↓ s and P ↓ s . This implies that E[Q] =⇒ Q with P ∼ = e Arn Q . So we haveQ ↓ s , which is only possible if Q a n = == ⇒ Q . When α = (νn)a n , we take E def = [ ] | a(x). (s | s x | m∈F [x = m]s) | s with s, s fresh. Then E[P ] -→-→ (νn)(P | m∈F [n = m]s | s n ). This implies that E[Q] =⇒ Q with (νn)(P | m∈F [x = m]s | s n ) ∼ = e Arn Q . As Q ↓ s , we necessarily have Q ≡ (νn)(Q | m∈F [n = m]s | s n ).By Lemmas 36 and 37, thismeans that P ∼ = e Arn Q . But then Q (νn)a n = ===== ⇒ Q so we can conclude. When α = n [m],we takeE def = [ ] | (x). ( m | [x = n]s) | s. Then E[P ] -→-→ P with P ↓ s . This implies that E[Q] =⇒ Q with P ∼ = e Arn Q . As Q ↓ s we have Q n [m] = ==== ⇒ Q . When α = (νn) n [m],we takeE def = [ ] | (x). ( m | s | s x | m∈F [x = m]s) | s. Then E[P ] -→-→ (νn)(P | m∈F [n = m]s | s n ). This implies E[Q] =⇒ Q with(νn)(P | m∈F [n = m]s | s n ) ∼ = e Arn Q . As Q ↓ s , we necessarily have Q ≡ (νn)(Q | m∈F [n = m]s | s n ). By Lemmas 36 and 37, this means P ∼ = e Arn Q . But then Q (νn) n [m]

2 0 2 0 31:6 On the Representation of References in the pi-calculus

  We write P ⇓ a if P =⇒ P 1 and P 1 ↓ a for some P 1 .

	P exhibits a barb at a (so a is in Names), written P ↓ a , if P ≡ (ν b)(ν L)(a m | P ) with
	a / ∈ b. Definition 1. Given a relation R on processes, and P R Q, we say that P, Q (in R) are
	-closed under reductions if P -→ P implies there is Q s.t. Q =⇒ Q and P R Q ;
	-preserved by a set C of contexts if C[P ] R C[Q] for all C ∈ C;
	-compatible on barbs if P ↓ a implies Q ⇓ a , for all a.
	A process P is reference-closed if fr(P ) = ∅. A context C is closing on the references of
	a process P if C[P ] is reference-closed; similarly, C is closing on the references of P, Q if it
	closing on the references of both P and Q. Since reductions may only decrease the set of
	free names of a process, the property of being reference-closed is preserved by reductions.
	Definition 2 (Barbed congruence and equivalence in π ref ). Barbed congruence is the largest
	symmetric relation ∼ =ref in π ref such that whenever P R Q then P, Q are: closed under
	reductions if P, Q are reference-closed; preserved by the contexts that are closing on references
	for P, Q; compatible on barbs if P, Q are reference-closed. Barbed equivalence, ∼ = e

ref , is defined in the same way, but using active contexts in place of all contexts.

  Typing conditions for reference names in Aπ processesNotations. We use , . . . to range over reference names, a, b, . . over plain names, n, m, . . .

			νa)P	TResR	∆, ∆ (ν )P P
	TRefO	m	TRefI	∅	P (x). P
	Figure 2

over the set of all names. ∆ ranges over finite sets of reference names. We sometimes write

Prebet and D. Sangiorgi 31:13 defined

  by a modified version of rule Ext where ok is used instead of ok, both in the premise and in the conclusion, and the following modified version of the Base rule:

bisimulation (Definition 23), using a predicate ok (∆ ∪ ∆ , R, P , Q, µ). This predicate is D. Hirschkoff, E.

  ). P 1 | P 2 ) and P ≡ (ν a, )(P 1 {m/x} | P 2 ) for some a, , P 1 , P 2 with m / ∈ a ∪ .We take ∆ 1 P 1 and ∆ 2 P 2 . This means ∆ 2 = ∆ . Depending on whether n is a reference name or not, we have that ∆ 1 = n or ∆ 1 = ∅ respectively. In both cases,∆ 1 P 1 {m/x} and ∆ 1 ∆ 2 P 1 {m/x} | P 2 . Thus ∆ = ∆ 1 ∆, meaning that ∆ = ∆, nif n is a reference name and ∆ = ∆ otherwise.For µ = n m , we have P ≡ (ν a, )(n m | P 2 ) and P ≡ (ν a, )P 2 for some a, , P 1 , P 2 \ ∆ 1 . Thus ∆ = ∆ -if n is a reference name and ∆ = ∆ otherwise.For µ = (νm)n m , we have P ≡ (ν a, , m)(n m | P 2 ) and P ≡ (ν a, )P 2 for some a, , P 1 , P 2 with n / ∈ a ∪ ∪ {m}. With the same notation, we have that ∆ 2 = ∆ , and if m is a plain name then ∆ 1 ∆ 2 = ∆ and ∆ 1 ∆ 2 = ∆ , m otherwise. Thus we have four cases for ∆ shown in the table below:

	with n, m / ∈ a ∪ .
	We take ∆ 1 n m and ∆ 2 P 2 . This means ∆ 1 ∆ 2 = ∆	, and ∆ 2 = ∆	. As
	n / ∈ , ∆ = ∆ n\m plain reference
	plain	∆	∆, m
	reference ∆ \ n ∆, m \ n

  say that a relation R is ≡-closed under allocation if P R Q implies P | n ≡R≡ Q | n for any n such that P | n and Q | n are well-typed.

Definition 30 (Reference Bisimulation up to ≡). A symmetric relation R that is ≡-closed under allocation is a reference bisimulation up to ≡ if whenever P R Q with P, Q complete, ∆ P, Q and P α -→ P with ∆ α, we have 1. either there exists Q such that Q α

Funding Hirschkoff and Prebet acknowledge support from the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157), and from LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" ANR-11-IDEX-0007. Sangiorgi acknowledges support from the MIUR-PRIN project 'Analysis of Program Analyses' (ASPRA, ID: 201784YSZ5_004), and from the European Research Council (ERC) Grant DLV-818616 DIAPASoN. and Davide Sangiorgi;

Inp: n(x). P

Match:

Active contexts in Aπ are defined by:

Reduction is defined by the following rules:

Labelled Transition Semantics

Actions of the LTS are defined as follows:

Transitions are defined in Figure 3

B.2 Type System for Output Receptiveness: Proof of Subject Reduction

We prove subject reduction, which we first recall:

Proposition 10 (Subject reduction). If ∆ P and P µ -→ P , then

B.5 Proofs about ≈ ip

We show soundness of ≈ ip -bisimulation up to store with respect to ≈ ip -bisimilarity, and of ≈ ip -bisimilarity with respect to reference bisimilarity.

Proof of Proposition 25. We show that

-→ P , we distinguish the sub-processes of P that have changed:

-→ P , and ok (∆∪∆ , R, P , Q, µ). We show by induction on the proof of ok

In short, we prove that

(Base-Up)

In short, we prove that ok (∆, R, P , Q, µ)

(Base-Up)

so we can conclude with rule Base.

(Ext) We use for the name used in that rule here. We use an induction on the size of s .

If s is empty, then / ∈ ∆ ∆ s , and we can apply rule Ext.

If / ∈ ∆ ∆ s , we can apply rule Ext as before. Otherwise, M s = m | M t for some m, t . Moreover, we know that ok ((∆, ), R,


Valentin Antuori
email: vantuori@laas.fr

Emmanuel Hebrard
email: hebrard@laas.fr

Marie-José Huguet
email: huguet@laas.fr

Siham Essodaigui
email: siham.essodaigui@renault.com

Alain Nguyen
email: alain.nguyen@renault.com

A constraint programming approach for planning items transportation in a workshop context

Keywords: Constraint Programming, Single-machine Scheduling, TSP

Introduction and related works

We are interested in transporting items in a workshop, from their production spots, to their consumption spots. For each type of items, there is one consumption machine, one production machine and four dedicated carriage trolleys, of limited capacity. Initially, there is one full trolley and one empty trolley in front of each machine. This problem comes from a real industrial problem, in the context of a car manufacturer workshop. When a trolley is full, an operator must transport it. He can transport several trolleys at the same time, making a train with them, but there is a limit on the maximal size on the train he can form. The production rate, and the consumption rate for a type of item is the same, therefore, when a carriage is full at a production spot, another carriage is empty at the associated consumption spot. The operator is also in charge of bringing back empty trolleys from their consumption machines, to production machines. The production rate, and the capacity of the trolley, permit to define a production cycle for each pair of machine. A production cycle is the time taken by a production (resp. consumption) machine, to fill (resp. empty) a trolley. The end time of a production cycle correspond to the beginning of the next cycle. For each pair of machines, and for each of their cycles considered until the time horizon, the goal is to deliver the trolleys which have been filled during the previous cycle to their consumption spots, and the trolleys which have been emptied during the previous cycle to their production spots.

The aim is to plan a route of the operator in order to satisfy pickup and delivery requests with time windows constraints. A particularity of this problem is the periodicity of the requests. Indeed, all the pickups and deliveries of a given item are almost completely sequenced. However, the relative order of pickups and deliveries of distinct items still need to be decided, potentially over a very long planning horizon. This problem can be seen as a Pickup and Delivery Problem, with a single capacited vehicle and time windows. It is part of the one-to-one pickup and delivery family (which means that each pickup has a unique destination and conversely, each delivery has a unique source) [START_REF] Cordeau | Recent models and algorithms for one-to-one pickup and delivery problems[END_REF]). The single vehicle case comes from a Traveling Salesman Problem (TSP) in which precedences were added between clients. Since then, several additional constraints have been considered, such as time windows, limited capacity or LIFO loading (deliveries must respect a last-in-first-out rule). One can find complete survey on pickup and delivery problem in [START_REF] Parragh | A survey on pickup and delivery problems[END_REF]) and [START_REF] Berbeglia | Static pickup and delivery problems: a classification scheme and survey[END_REF]). There are temporal specificities in our problem. Indeed, each request has a twin request with the same time window: for each request from point A to point B to transport a full (resp. empty) trolley, there is a request from B to A for the empty (resp. full) trolley to do during the same time. Moreover, each request is repeated over time until the horizon, that is, each due date corresponds to a release date for the next request on the same pair of machine.

Routing problems can often be seen as scheduling problems with sequence-dependent setup times. In fact, time windows and precedences constraints, as well as the fact that there is no objective to optimize might suggest that the problem more adapted to scheduling technologies [START_REF] Beck | Vehicle routing and job shop scheduling: What's the difference?[END_REF]. From a scheduling point of view, it is a single resource (the driver of the train) scheduling problem. We have 4 types of activities: pickup and delivery of a full and an empty trolley which can't overlap. There is a precedence between a pickup and its delivery, and each activity has a time window. Travel times between two activities are then sequence-dependent. Finally the length of the train can be seen as a reservoir resource with limited capacity, which is filled by pickups, and emptied by deliveries.

Constraint Models

We propose two constraint models to deal with this problem. One TSP-oriented based on next variables, and one scheduling oriented. In the scheduling model, for each operation i ∈ T = {1, 2, ..., n}, we define the variable start i as the starting date of the operation i. Moreover we introduce for each pair of operations i, j ∈ T , a Boolean variable x ij which represent the relative ordering of the two operations. The link between these two sets of variables is made with with the following constraint:

x ij = 1 ⇔ start j ≥ start i + tt ij + p i 0 ⇔ start i ≥ start j + tt ji + p j
with tt ij , the travel time between operation i and j, and p i the processing time of i. In fact, we do not need a Boolean variable for every pair of tasks, and can easily reduce the model. For all pair of operation i, j ∈ T , such as i precede j, we avoid creating the variable x ij , and directly post the following constraint :

start j ≥ start i + tt ij + p i .
Since production cycles are often much shorter than the planning horizon, the problem involves a lot of precedences. Therefore, we can drastically reduce the size of the model. Moreover, we observe that there are only two sensible ways to schedule the four activities of a production cycle (pickup of the full trolley, pickup of the empty trolley, and the corresponding deliveries). First, obviously pickups must precede their respective deliveries. Second, since the second pickup and the first delivery take place at the same spot, it is always preferable (w.r.t. the capacities and the time windows) to do the first delivery before the second pickup. Therefore, there are only two possible orders: the operator may either first pickup and deliver the full trolley, or first pickup and deliver the empty trolley. Hence, only one variable is needed for these four tasks. In order to deal with the constraint on the length of the train, we use the balance constraint introduced in [START_REF] Laborie | Algorithms for propagating resource constraints in ai planning and scheduling: Existing approaches and new results[END_REF].

The other model is inspired by the constraint model for TSP with time windows proposed in [START_REF] Ducomman | Alternative Filtering for the Weighted Circuit Constraint: Comparing Lower Bounds for the TSP and Solving TSPTW[END_REF]. For each operation i, there is a variable next i that indicates which operation directly follows i. Additional variables are needed in order to post redundant constraints. pos i indicates the position of the operation i in the sequence of operations, and x ij has the same semantic than in the first model. We add another variable trainL i which represent the length of the train before the operation i. Our model only differ by the adding of the following constraints :

trainL nexti = trainL i + l i ∀i ∈ T ∪ {0} (1) trainL 0 = 0 (2) pos deli > pos i ∀i ∈ P (3)
with l i , the length of the trolley of the operation i (negative length for delivery), del i is the associate delivery of the operation i, and P is the set of pickup operations. Constraint (1) and ( 2) represent the accumulation on the train length during the sequence of operations and use the Element constraint. The last constraint (3) ensures that each pickup precedes its delivery. In addition, we use the Circuit constraint to enforce the Hamiltonian circuit.

Experiments

In order to compare the two models, and in addition to the industrial instances, we generated random instances1 . We tried to generate only feasible instances, but we cannot guaranty that all instances are. There are 4 categories of instances (A, B, C, D). Instances A contain the least dense instances, i.e. with the least number of operations. They have also more pairs of machines with the same production cycle. Conversely, instances D are the most dense, and most asynchronous. We generate 10 instances of each category, and for each of them we consider 3 different temporal horizons, leading to 120 instances in total. The two models were implemented in the constraint solver Choco2 .

We observed that variable orderings following the chronological sequence tend to be more efficient. For instance, in the TSP model, building a tour by selecting the nodes from the first to be visited (pos 1 ) to the last to be visited (pos n ) was more effective than assigning the positions in a different order. In the case of the scheduling model, we use the following strategy: we say x ij dominate x kl , iff min(start i ) ≤ min(start k ) and min(start j ) ≤ min(start l ) with at least one strict inequality or min(start i ) ≤ min(start l ) and min(start j ) ≤ min(start k ) with at least one strict inequality, with min(start i ) the minimum value of start i . When choosing a variable to assign, we look for the boolean variables which is not dominated by any other variables, ties are broken randomly. We noticed a slight improvement when in addition we gave priority to the variables which order operations in the same pair of machines before the other ones. That is, we don't deal with a variable x ij if the variable ordering the three remaining activities linked to operation i, and the variable ordering the three remaining activities linked to operation j are not instantiated. Generic heuristics such as dom/wdeg [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF]) were significantly less effective than these simple orderings.

Similarly, we explore first the branch that minimizes the start time of the next operation. In the TSP model, it means assigning pos i to j such that the minimum value of start j is minimal. In the scheduling model, it means assigning x ij to 1 iff minimum value of start i is lower than the minimum value of start j . For both, and thanks to the propagation on the start's variables, this heuristic acts more or less like a nearest neighborhood approach and takes advantage of the travel time between activities.

We ran each instance 10 times with randomized heuristics: if there are ties, they are broken randomly, and if not, one of the two best choices is chosen randomly with equal probabilities. We also used a restart strategy (the Luby sequence [START_REF] Luby | Optimal speedup of las vegas algorithms[END_REF])) to improve the result. Each run has a timeout of 1 hour.

Table 1 shows the results. The first column denotes the category of the instance and second column denotes the temporal horizon. For the two models (denoted by Scheduling and TSP), 3 indicators are given, the number of solved instances (in average on 10 runs), the average time, and the numbers of fails for solved instances. We observe that the schedulingbased model can solve more instances in every category, and is faster in average. The average number of fails for the TSP model shows the relative slowness of that model. Most of the instances are unsolved.

Conclusions

We introduced a one machine scheduling problem with several additional constraints. That problem is not new in the definition of its constraints, but the temporal structure of the instances makes it challenging. We proposed a randomly generated set of benchmark instances, whose a large number stay unsolved. We observed that a light model based on ordering pair of activities works better than a TSP-based model, which does not scale to industrial instances.

As a large number of the generated instances remains unsolved, there are still works to do. We are currently working on a Large Neighborhood Search (LNS) in order to improve these results. In this scheme, we relax the due date of each task, and instead we minimize the maximum lateness. Then during a LNS move, a subset of operations can be withdrawn from the sequence and re-inserted so as to minimize this objective. We also aim to deal with the entire problem, which is the team sizing for the whole shop. The goal is to plan a route through the pair of machines, minimizing the number of trains in the shop.

Table 1 .

 1 Comparison of the two models on the generated instances

	Cat. Hor.	Scheduling NbSolve Time NbFail NbSolve Time NbFail TSP	Nb Inst.
		15000 9.3	44.11 174195 9.0	18.39 13081	10
	A	25000 8.5	52.74 143564 7.9	140.92 9445	10
		40000 8.0	36.48 29665	7.1	149.71 3803	10
		15000 4.8	390.61 301231 2.1	943.88 18340	10
	B	25000 2.5	381.94 203849 0.7 1017.76 2015	10
		40000 2.0	402.88 419479 0.1 1929.71 283	10
		15000 4.3	534.60 387635 2.0	541.68 14549	10
	C	25000 1.4 1264.03 352172 0.1 1693.80 1521	10
		40000 0.0	-	-	0.0	-	-	10
		15000 2.2	495.55 112918 0.8 1271.75 9484	10
	D	25000 0.2 2565.44 45153	0.0	-	-	10
		40000 0.0	-	-	0.0	-	-	10

Available on https://github.com/AntuVal/SPDPTW

Prud'homme, C., Fages, J.-G. & Lorca, X. (2017), Choco Documentation.