Marco Bernardo

Davide Sangiorgi

Valeria Vignudelli

On the Discriminating Power of Passivation and Higher-Order Interaction

Keywords: F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs-logics of programs; F.3.2 [Logics and Meaning of Programs]: Semantics of Programming Language-operational semantics higher-order pi-calculus, lambda-calculus, CCS, contextual equivalence, passivation, probabilistic processes

This paper studies the discriminating power offered by higherorder concurrent languages, and contrasts this power with those offered by higher-order sequential languages (à la λ-calculus) and by first-order concurrent languages (à la CCS). The concurrent higherorder languages that we focus on are Higher-Order π-calculus (HOπ), which supports higher-order communication, and an extension of HOπ with passivation, a simple higher-order construct that allows one to obtain location-dependent process behaviours.

The comparison is carried out by providing embeddings of firstorder processes into the various languages, and then examining the resulting contextual equivalences induced on such processes. As first-order processes we consider both ordinary Labeled Transition Systems (LTSs) and Reactive Probabilistic Labeled Transition Systems (RPLTSs).

The hierarchy of discriminating powers so obtained for RPLTSs is finer than that for LTSs. For instance, in the LTS case, the additional discriminating power offered by passivation in concurrency is captured, in sequential languages, by the difference between the call-by-name and call-by-value evaluation strategies of an extended typed λ-calculus.

Introduction

Higher-order languages have been widely studied in functional programming, following the λ-calculus. In a higher-order language, variables may be instantiated with terms of the language. When multiple occurrences of the variable exist, this mechanism results in the possibility of copying the terms of the language.

Higher-order concurrency combines functional programming and concurrent programming: the ability of exchanging values, common in concurrency, is enhanced by allowing values to include terms of the language itself, the distinguishing feature of functional languages. Calculi of this kind include CHOCS [START_REF] Thomsen | Plain CHOCS, a second generation calculus for higherorder processes[END_REF] and the Higher-Order π-calculus [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF].

An important extension to concurrent higher-order languages concerns distribution. This is usually achieved by means of constructs for expressing and operating on locations. As a consequence, the observable behaviour of a system of processes depends not only on the behaviour of the constituent processes, but also on the locations in which these processes are run. This can have a deep impact on the behavioural theory and algebraic laws for the language.

One of the simplest constructs that show these phenomena is passivation. Passivation offers the capability of capturing the content of a certain location, and then restarting the execution in a different context. The semantics of passivation has been the subject of a number of papers, usually in extensions of the Higher-Order πcalculus [START_REF] Koutavas | Symbolic bisimulation for a higherorder distributed language with passivation[END_REF][START_REF] Lenglet | Howe's method for calculi with passivation[END_REF][START_REF] Lenglet | Normal bisimulations in calculi with passivation[END_REF][START_REF] Lenglet | Characterizing contextual equivalence in calculi with passivation[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF]. Passivation is also featured in the Homer calculus [START_REF] Godskesen | Extending Howe's method to early bisimulations for typed mobile embedded resources with local names[END_REF] and the M-calculus [START_REF] Schmitt | The M-calculus: a higher-order distributed process calculus[END_REF]; a similar construct appears in the Seal calculus [START_REF] Castagna | The Seal calculus[END_REF] and in Acute [START_REF] Sewell | Acute: High-level programming language design for distributed computation[END_REF]. Passivation has also been advocated to support run-time system updates, fault recovery and fault tolerance (by providing the basis for mechanisms for checkpointing computations and replicating them), and to support adaptive behaviours.

The goal of this paper is to shed light into the discriminating power offered by higher-order concurrent languages and contrasting this power with those offered by higher-order sequential languages (which are deprived of all concurrency) and by first-order concurrent languages (which are deprived of all higher-order features). The comparison is carried out by considering embeddings of first-order processes into the languages, and then examining the equivalences induced by the resulting contextual equivalences on the first-order processes. In other words, the discriminating power of a language refers to the existence of appropriate contexts of the language that are capable of separating the behaviours of first-order processes.

The higher-order sequential languages are typed λ-calculi extended with a kell construct [START_REF] Schmitt | The kell calculus: A family of higherorder distributed process calculi[END_REF] akin to a store location of imperative λ-calculi. The λ-calculi offer constructs for reading the kell, overriding it, and, if the kell contains a process, for consuming such a process (i.e., performing observations on the process actions). The higher-order concurrent languages are HOπ, which allows higher-order communication, and HOπpass, an extension of HOπ with passivation (similar to the languages in [START_REF] Koutavas | Symbolic bisimulation for a higherorder distributed language with passivation[END_REF][START_REF] Lenglet | Characterizing contextual equivalence in calculi with passivation[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF]). Both languages also admit first-order communications, to be able to interact with the embedded first-order processes. The first-order concurrent language that we consider is CCS -, a CCS-like calculus.

The λ-calculi also allow us to observe the inability for a process to perform a certain action. In concurrency, this possibility is referred to as action refusal. For a thorough comparison, we therefore also consider both restrictions of the λ-calculi without the refusal observation (though at the price of allowing computations that may get stuck) and extensions of HOπ, HOπpass, and CCS -with the refusal capability.

Concerning the tested first-order processes, embedded into the above languages, we consider both ordinary LTSs (which exhibit internal nondeterminism, e.g., a process that has multiple transitions with the same label) and reactive probabilistic LTSs (which exhibit probabilistic choices on transitions with the same label, hence admit no internal nondeterminism). We simply call LTSs the former and RPLTSs the latter.

We show that, on LTSs, the difference between the discriminating power of HOπ and HOπpass is captured, in the λ-calculi, through the difference between the call-by-name and call-by-value evaluation strategies, both with and without refusals.

The correspondence between the HOπpass calculi and the callby-value λ-calculi appears robust, and is maintained in all scenarios examined. The same does not hold between the HOπ calculi and the call-by-name λ-calculi, whose correspondence breaks on RPLTSs. The case of RPLTSs is more involved also when we consider the first-order language CCS -. For instance, the discriminating power of CCS -is strictly in between that of the call-by-name λ-calculus and HOπ. In contrast, the three languages are equally discriminating on LTSs.

We also discuss variations of the above settings. In languages with locations, communication may or may not be affected by spatial proximity. This is the difference between global vs. local communications. This difference is important for the semantics of the languages but, as we shall see, does not impinge on their discriminating power.

The contextual equivalences that we consider are may-like (a test, i.e., a context, is successful on a process if there is at least one successful computation). We also discuss the contextual preorders, and 'must' forms of success (all computations are successful). We isolate a few scenarios in which, surprisingly, the may and must forms of contextual equivalence coincide.

There are analogies between our results on the contextual equivalences induced by higher-order languages on ordinary LTSs and results in the literature on the equivalences on LTSs that characterize the coarsest congruences contained in trace equivalence for operators whose operational rules comply with certain rule formats. Some of these formats allow negative premises in the rules, with which refusals may be encoded, or allow rules in which an argument of an operator may end up, in the derivative of the rule, within a predefined context; when the context is polyadic, this yields a form of copying. In higher-order languages, in contrast, copying is achieved through the variable binding mechanisms of the languages. Passivation or, in the λ-calculi, call-by-value, are necessary to obtain the discriminating power of powerful formats such as GSOS [START_REF] Bloom | Bisimulation can't be traced[END_REF] and tyft/tyxt [START_REF] Groote | Structured operational semantics and bisimulation as a congruence[END_REF] (which give ready simulation equivalence and simulation equivalence, respectively).

Rule formats for probabilistic processes include [START_REF] Bartels | GSOS for probabilistic transition systems[END_REF][START_REF] Lee | Probabilistic transition system specification: Congruence and full abstraction of bisimulation[END_REF][START_REF] Lanotte | Probabilistic bisimulation as a congruence[END_REF], where the emphasis is on ensuring congruence properties for bisimilarity. Testing of reactive probabilistic processes is studied in [START_REF] Kwiatkowska | A testing equivalence for reactive probabilistic processes[END_REF], obtaining an equivalence strictly coarser than bisimilarity, though the comparison with the equivalences induced by our contextual equivalences is unclear. Testing equivalences in which the testers are allowed to make copies of the tested RPLTSs have been studied by Larsen and Skou [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] and Van Breugel et al. [START_REF] Van Breugel | Domain theory, testing and simulation for labelled Markov processes[END_REF] to recover bisimilarity. Our characterizations of bisimilarity in higher-order languages exploit these results: in one direction of the proofs, we essentially implement in higher-order languages the tests needed in [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF][START_REF] Van Breugel | Domain theory, testing and simulation for labelled Markov processes[END_REF] to distinguish non-bisimilar RPLTSs. In contrast, copies of the tested process are not possible in our CCS-like languages.

Paper structure: Section 2 presents background material: LTSs, RPLTSs, equivalences on them. Section 3 considers the embeddings of LTSs and RPLTSs into λ-calculi. Section 4 shows the syntax and operational semantics of the concurrent languages (CCSand HOπ-like), whose discriminating power is studied in Sections 5 and 6. Section 7 discusses variations of the scenarios examined. Section 8 reports conclusions and possible future work.

Notation: In examples, we sometimes use a CCS-like notation, with prefixing and choice, to describe the processes of an LTS or RPLTS.

First-Order Processes and Equivalences

In this section, we introduce the two LTS-like models used in the paper to formalize respectively fully nondeterministic processes (LTSs) and reactive probabilistic processes (RPLTSs), and we recall a number of behavioural equivalences for these first-order processes. Then, we define contextual equivalences induced on such processes by their embedding into algebraic languages.

Fully Nondeterministic Processes

The behaviour of a fully nondeterministic process can be represented through a labeled transition system. DEFINITION 2.1. A labeled transition system (LTS) is a triple (S, A, -→) where S is a countable set of states (usually called processes), A is a countable set of transition-labeling actions, and

-→ ⊆ S × A × S is a transition relation. The LTS is image-finite if {P ′ ∈ S | P a -→ P ′ } is
finite for all P ∈ S and a ∈ A.

We will characterize the contextual equivalences induced on LTSs in terms of simulation equivalence [START_REF] Milner | Communication and Concurrency[END_REF], ready simulation equivalence [START_REF] Bloom | Bisimulation can't be traced[END_REF][START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], trace equivalence [START_REF] Brookes | A theory of communicating sequential processes[END_REF], failure equivalence [START_REF] Brookes | A theory of communicating sequential processes[END_REF], and failure-trace equivalence [START_REF] Phillips | Refusal testing[END_REF][START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF]. DEFINITION 2.2. Let (S, A, -→) be an LTS and R be a relation over S. Relation R is a simulation if, whenever (P1, P2) ∈ R, then for all a ∈ A it holds that for each P1 a -→ P ′ 1 there exists

P2 a -→ P ′ 2 such that (P ′ 1 , P ′ 2 ) ∈ R. Relation R is a ready simu- lation if, additionally, P1 a -→ implies P2 a -→.
Processes P1, P2 ∈ S are simulation equivalent (P1 ∼S P2) -resp., ready simulation equivalent (P1 ∼RS P2) -if there exist two simulationsresp., ready simulations -R and R ′ such that (P1, P2) ∈ R and (P2, P1) ∈ R ′ .

A trace is an element σ of A * . We let CC(P, σ) denote the set of σ-compatible computations from P , i.e., the computations starting from P and labeled with σ. We call failure pair an element ϕ ∈ A * × 2 A composed by a trace σ and a refusal set F . We denote by F CC(P, ϕ) the set of ϕ-compatible computations from P , i.e., the computations starting from P and labeled with σ whose last state has no outgoing transitions labeled with an action in F . We call failure trace an element φ ∈ (A × 2 A ) * given by a sequence of n ∈ N pairs of the form (ai, Fi). We indicate with F T CC(P, φ) the set of φ-compatible computations from P , i.e., the computations starting from P and labeled with trace a1 . . . an such that the state reached after the i-th step, 1 ≤ i ≤ n, has no outgoing transitions labeled with an action in the refusal set Fi. DEFINITION 2.3. Let (S, A, -→) be an LTS. Processes P1, P2 ∈ S are:

• trace equivalent, written P1 ∼Tr P2, if CC(P1, σ) = ∅ ⇐⇒ CC(P2, σ) = ∅ for all σ ∈ A * ; • failure equivalent, written P1 ∼F P2, if F CC(P1, ϕ) = ∅ ⇐⇒ FCC(P2, ϕ) = ∅ for all ϕ ∈ A * × 2 A ; • failure-trace equivalent, written P1 ∼FTr P2, if F T CC(P1, φ) = ∅ ⇐⇒ F T CC(P2, φ) = ∅ for all φ ∈ (A × 2 A ) * .
For instance, consider the processes defined in Examples 3.1 and 3.2: P and P ′ are failure-trace (and hence trace) equivalent but not simulation equivalent, while P ′ is simulation but not failuretrace equivalent to P ′′ ; processes Q, Q ′ are not ready simulation equivalent, but they are both simulation and failure-trace equivalent.

Reactive Probabilistic Processes

A reactive probabilistic process features probabilistic choices but no internal nondeterminism. Its behaviour can be described as a variant of LTS [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF]. The set of discrete probability distributions over a set S is denoted by Distr (S). Given a transition P a -→ ∆, a process P ′ ∈ S is not reachable from P via that a-transition if ∆(P ′ ) = 0, otherwise it is reachable with probability p = ∆(P ′ ). The reachable states form the support of ∆, i.e., supp(∆) = {P ′ ∈ S | ∆(P ′ ) > 0}. The choice of the action to be performed by an RPLTS process is made by the external environment, and then the target state is selected internally, purely probabilistically.

We will compare the equivalences induced on RPLTSs with probabilistic bisimulation equivalence [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] and probabilistic variants of trace equivalence and failure-trace equivalence. DEFINITION 2.5. Let (S, A, -→) be an RPLTS. An equivalence relation B over S is a probabilistic bisimulation if, whenever (P1, P2) ∈ B, then for all a ∈ A it holds that P1 a -→ ∆1 implies P2 a -→ ∆2 with ∆1(S ′ ) = ∆2(S ′ ) for all S ′ ∈ S/B. Processes P1, P2 ∈ S are probabilistic bisimilar, written P1 ∼PB P2, if there exists a probabilistic bisimulation B such that (P1, P2) ∈ B.

In the RPLTS setting, each state-to-state step P a -→ P ′ of a computation is derived from a state-to-distribution transition P a -→ ∆. DEFINITION 2.6. Let L = (S, A, -→) be an RPLTS and P, P ′ ∈ S. The sequence

c ≡ P0 a 1 -→ P1 a 2 -→ P2 . . . Pn-1 an -→ Pn is a computation of L of length n from P = P0 to P ′ = Pn if for all i = 1, . . . , n there exists a transition Pi-1 a i -→ ∆i such that Pi ∈ supp(∆i), with ∆i(Pi) being the execution probabil- ity of step Pi-1 a i -→ Pi conditioned on the selection of transition Pi-1 a i -→ ∆i of L at state Pi-1.
We denote by C fin (P ) the set of finite-length computations from P .

Given a computation c ∈ C fin (P ), its conditional execution probability prob(c) can be defined as the product of the conditional execution probabilities of the individual steps of c. This notion is lifted to a set C ⊆ C fin (P ) of identically labeled computations by letting prob(C) = c∈C prob(c). DEFINITION 2.7. Let (S, A, -→) be an RPLTS. Processes P1, P2 ∈ S are:

• probabilistic trace equivalent, written P1 ∼PTr P2, if prob(CC(P1, σ)) = prob(CC(P2, σ)) for all σ ∈ A * ; • probabilistic failure-trace equivalent, written P1 ∼PFTr P2, if prob(F T CC(P1, φ)) = prob(F T CC(P2, φ)) for all φ ∈ (A × 2 A ) * .
In Example 3.4, P is not probabilistic trace equivalent to P ′′ and is probabilistic trace (but not probabilistic failure-trace) equivalent to P ′ . Finally, Q and Q ′ are probabilistic failure-trace equivalent, but they are not probabilistic bisimilar.

Contextual May-Equivalence

Given a set of processes as states of an LTS or RPLTS L, and an algebraic language AL (i.e., generated by a grammar), the equivalence induced by AL equates the L processes P1 and P2 if C[P1] and C[P2] behave the same for all contexts C of AL. Here 'behave the same' is formalized as in ('may') contextual equivalence: C[P1] is as successful as C[P2] with respect to a special success observation, indicated with ω. The context C is an AL-expression with a single occurrence of the hole [•] in it.

In the remainder of the paper, L is always the LTS or RPLTS of tested first-order processes, and P, Q range over L processes. Moreover, in these tested processes each transition represents a visible action, i.e., there is a corresponding coaction with which the action can synchronize and produce a reduction; and the actions available for L do not include the success signal ω. We write AL(L) for the extension of AL with the L processes; i.e., the grammar for AL is extended so to include the L processes. In a language AL(L), reductions are represented as τ -transitions τ -→ (or simply -→, in λ-calculi). Each language AL used will have constructs for testing the action capabilities of L processes; thus, the set of action names for L is supposed to appear in the grammar for AL. We emphasize that probabilities may appear in the tested L processes, but they may not appear in the AL languages that test the processes.

The operational semantics of AL(L) will be based on different LTS-like models depending on the nature of L. A finite-length computation c from a term M ∈ AL(L) is successful if each step of c is labeled with τ , the last state of c can perform ω, and no preceding state of c can perform ω. We denote by SC(M ) the set of successful computations from M . In the fully nondeterministic case, when L is an LTS, the semantic model underlying AL(L) is again an LTS. DEFINITION 2.8. Let L be an LTS, P1 and P2 two processes of L, and AL an algebraic language. In AL(L):

• P1 is contextually may-less than P2, written P1 ≤ L AL P2, if SC(C[P1]) = ∅ =⇒ SC(C[P2]) = ∅ for all contexts C of AL. • P1 is contextually may-equivalent to P2, written P1 ≃ L AL P2, if P1 ≤ L AL P2 and P2 ≤ L AL P1.
In the case that L is an RPLTS, the definition of contextual equivalence is more involved because the semantic model underlying AL(L) is a nondeterministic and probabilistic LTS (NPLTS for short), an extension of RPLTS in which internal nondeterminism is allowed (i.e., the constraint at the end of Definition 2.4 is removed).

For NPLTS computations, using probabilities conditioned on actions is not sufficient, because a state may have several outgoing transitions labeled with the same action. As is standard in the NPLTS setting, we thus resort to resolutions. A resolution of a state M of an NPLTS W is the result of a possible way of resolving nondeterminism, which is obtained by unfolding from M the graph structure underlying W while selecting from the current state at most one of its outgoing transitions. DEFINITION 2.9. Let W = (S, A, -→) be an NPLTS and M ∈ S. An NPLTS Z = (Z, A, -→Z ) is a resolution of M if there exists a state correspondence function corr Z : Z → S such that M = corr Z (zM ), for some zM ∈ Z, and for all z ∈ Z it holds that:

• If z a -→Z ∆, then corr Z (z) a -→ ∆ ′ with corr Z being injective over supp(∆) and ∆(z ′ ) = ∆ ′ (corr Z (z ′ )) for all z ′ ∈ Z. • If z a 1 -→Z ∆1 and z a 2
-→Z ∆2, then a1 = a2 and ∆1 = ∆2.

Z is maximal if, for all z ∈ Z, whenever z has no outgoing transitions, then corr Z (z) has no outgoing transitions either. We respectively denote by Res(M ) and Resmax(M ) the sets of resolutions and maximal resolutions of M .

As Z ∈ Res(M ) is fully probabilistic, the probability prob(c) of executing c ∈ C fin (zM ) is the product of the (no longer conditional) execution probabilities of the individual steps of c. This notion is lifted to C ⊆ C fin (zM ) by letting prob(C) = c∈C prob(c) whenever none of the computations in C is a proper prefix of one of the others.

The contextual equivalence defined below is inspired by [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF][START_REF] Segala | Testing probabilistic automata[END_REF][START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF]. Intuitively, P1 is worse than P2 if, for all contexts C, the maximum probability of reaching success in an arbitrary maximal resolution of C[P1] is not greater than the maximum probability of reaching success in an arbitrary maximal resolution of C[P2]. To correctly quantify success, we restrict ourselves to Resτ,max(C[P ]), the set of maximal resolutions obtained from C[P ] by forbidding the execution of actions not resulting in interactions (i.e., τ actions). DEFINITION 2.10. Let L be an RPLTS, P1 and P2 be two processes of L, and AL be an algebraic language. Indicating with ρi the predicate Zi ∈ Resτ,max(C[Pi]) for i = 1, 2, we say that in AL(L):

• P1 is contextually may-less than P2, written P1 ≤ L AL P2, if for all contexts C of AL it holds that:

ρ 1 prob(SC(z C[P 1 ] )) ≤ ρ 2 prob(SC(z C[P 2 ] )) • P1 is contextually may-equivalent to P2, written P1 ≃ L AL P2, if P1 ≤ L AL P2 and P2 ≤ L AL P1.
We sometimes abbreviate 'contextual may equivalence' as 'contextual equivalence' or even 'may equivalence'.

λ-Calculi

Syntax

Figure 1 shows the syntax of the (typed) λ-calculus KΛ into which we embed the processes of a (first-order) LTS or RPLTS L. The grammar of the language resulting from the embedding, KΛ(L), has therefore the additional production M := . . . | P where P is an L process; moreover, in the action test, r is supposed to range over the actions in L. A λ-term M is evaluated in an environment that may contain another λ-term N , written N ; M . The environment will correspond, in the concurrent calculi of the next section, to a location, and therefore, following the concurrency terminology, we call such an environment the kell. The language includes a construct pass for obtaining the content of the kell, and a construct N ; M for creating the kell. The action-test construct allows us to check whether the process that the kell evaluates to can perform a certain action. The remaining constructs are common constructs of typed λ-calculi. We assume that the set of constants includes the boolean values true and false and the unit value ⋆. For lack of space we omit the type system (simply-typed with recursive types; for simplicity, the expressions in the kell may only have process type). In contrast to the usual operators for kells in concurrency, in KΛ the kell is persistent: pass reads the kell without destroying it. This simplifies the typing system and does not affect the results presented.

Reduction is defined on terms that are closed (i.e., without free variables) and equipped with the kell, i.e., of the form M1 ; M2 . As a consequence, the contexts in which the L processes are tested have the form M ; C or C ; M .

Fully Nondeterministic Processes

We consider both call-by-name and call-by-value reduction strategies. We call KΛN(L) the call-by-name language, KΛV(L) its callby-value version, as usual omitting L when referring to the pure languages (without L processes). When L is an LTS, a reduction step has the form M1 ; M2 -→ M ′ 1 ; M ′ 2 , saying that the evaluation of M2 with kell M1 produces a new term M ′ 2 with kell M ′ 1 . The rules for reduction are in Figure 2 (in rule EVALKELL, Q is some predefined specific process from L that is used to initialize the kell; it does not matter which particular Q is used for thisanyone would do). In KΛN(L), only the functional part of an application is evaluated, hence rule BETA-V and the production V C for evaluation contexts are omitted. In KΛV(L), both the function and the argument of an application are evaluated, hence rule BETA-N is omitted. In all these languages, although the operators of the λ-calculi themselves are sequential, nondeterministic computations are possible because the process in the kell may present internal nondeterminism. As usual, =⇒ is the reflexive and transitive closure of -→.

In the call-by-name calculus KΛN(L), during a computation an L process may be moved around, may be copied, and may be placed into the kell. However, once placed into the kell for evaluation, the process cannot be stopped and later re-evaluated. In call-by-value, by contrast, the PASS rule may be used by the argument of a function, and then the process so obtained may be passed onto the function; as a consequence, the process may later be evaluated. This gives us more sophisticated process tests than call-by-name. Example 3.1 shows how the terms in KΛN and KΛV can test the existence of 'barbed traces' in the behaviour of a process placed in the kell, and how some tests are available only in call-by-value. EXAMPLE 3.1. Below, a test is encoded in KΛV as a thunked boolean expression λ.M and (λ.M )⋆ is its 'unthunking' (thunking is useful in composition of tests). A test λ.M is successful on a process P if there is a run in which true is produced, i.e., P ; (λ.M )⋆ =⇒ N ; true for some N . Test Ta checks the possibility of performing action a (i.e., P a -→), whereas T a checks its impossibility. Function Seq composes the two argument tests sequentially. Thus M1 checks the existence of an a-derivative that cannot perform c but can perform b (i.e., P a -→ P ′ with P ′ c -→ and P ′ b -→, for some P ′ ). Function And makes the conjunction of the two argument tests. Thus M2 checks the existence of an a-derivative that can perform both b and c, while Terms:

M ::= x (variables) | if M 1 then M 2 else M 3 (if-then-else) | λx.M (functions) | pass (passivation) | M 1 M 2 (applications) | M 1 ; M 2 (kell creation) | c (constants) | r? (action test) Figure 1. Syntax of KΛ BETA-N N ; (λx.M 1 )M 2 -→ N ; M 1 { M 2/x} BETA-V V is a value N ; (λx.M )V -→ N ; M { V /x} IF1 N ; if true then M 1 else M 2 -→ N ; M 1 IF2 N ; if false then M 1 else M 2 -→ N ; M 2 NEWKELL N ; M 1 ; M 2 -→ M 1 ; M 2 PASS M ; pass -→ M ; M EVALKELL Q ; M -→ Q ′ ; M ′ M ; r? -→ M ′ ; r? ACT P r -→ P ′ (in L) P ; r? -→ P ′ ; true REFACT P r -→ (in L) P ; r? -→ P ; false EVCON C is an evaluation context N ; M -→ N ′ ; M ′ N ; C[M ] -→ N ′ ; C[M ′ ]
Evaluation contexts: In λ-calculi, well-typed terms are supposed to produce computations that never get stuck. To maintain this property, we have to ensure that the action-test construct a? returns a value even when the process in the kell is unable to perform the requested action a. That is, we are allowed to observe the inability for the kell process to perform a certain action, in concurrency referred to as action refusal and usually omitted. We therefore consider also variants of the above λ-calculi without the refusal capability. Formally, rule REFACT is omitted. Of course the price to pay is that computations from a well-typed term may get stuck. The call-by-name calculus without REFACT is called KΛ N-ref (L), whereas call-by-value without REFACT is KΛ V-ref (L). Proof [Sketch] The proofs are different for inductive and coinductive equivalences. For the inductive equivalences, we discuss failure-trace equivalence and KΛN. In one direction, one shows that for every failure trace φ there is a context C of KΛN such that P has the failure trace φ iff C[P ] produces true.

C := [•] | if C then M 1 else M 2 | CM | V C Values: V :: = c | λx.M | P | x
For the opposite direction, suppose P and Q have the same failure traces, and suppose C[P ] =⇒ ω -→. We show that there is also To analyze what happens to the context and the processes inside them during the computation, we adopt an annotated operational semantics (equivalent to the original one) in which, when a hole reaches a redex position (whereby the process in the hole may be evaluated), the hole is marked and the observations made on its process (the transition performed, the actions refused) are annotated. One then shows that the observations so annotated can only be failure traces. Hence process Q, which has the same failure traces as P , can mimic the computation C[P ] =⇒ ω -→. As an example for the coinductive equivalences, we consider ready simulation equivalence and KΛV(L). In one direction, suppose P is not ready simulated by Q. We exploit the assumption of image-finiteness for the LTS L and the inductive characterization of ready simulation via stratification approximants. Thus there is a minimal n such that P and Q are distinguished at the n-th approximant. Proceeding by induction on n we define a context of the language that separates P and Q, in the sense that only C[P ] may reduce to true.

a computation C[Q] =⇒ ω -→,
For the opposite direction, one shows that the relation

R def = {(C[P ], C[Q]
) | P is ready simulated by Q} where C is a polyadic (and runnable) context, is a strong simulation on reductions (in the sense that if M R N and M -→ M ′ then there is N ′ with N -→ N ′ and M ′ R N ′ ). As a consequence, any successful computation from C[P ] may be mimicked by C[Q]. ✷

Reactive Probabilistic Processes

The reduction relation for KΛ(L) when L is an RPLTS is the expected probabilistic modification of the system for the nondeterministic case. A probability distribution reached from a process in the kell is propagated to a λ-term by using the rule ACT P r -→ ∆ P ; r? -→ ∆ ; true For any term M , M is the Dirac probability distribution on M , i.e., M (M ) = 1 and M (M ′ ) = 0 if M = M ′ . For all probability distributions ∆1, ∆2 on the terms of the language,

∆1 ; ∆2 (M ) def = ∆1(M1) • ∆2(M2) if M = M1 ; M2 0 otherwise
Since the tested processes do not feature internal nondeterminism, all terms of KΛN, KΛ N-ref , KΛV and KΛ V-ref are reactive probabilistic processes. Hence, for any context C of these languages and for any reactive probabilistic process P the term C[P ] has only one maximal resolution on reductions. We write prob(SC(C[P ])) to denote prob(SC(z C[P ] )), where z C[P ] is the state associated with C[P ] in the resolution. EXAMPLE 3.4. Consider the processes and λ-terms defined below, where Seq , And , Ta , T a are as in Example 3.1. In all four λ-calculi, the test M1 separates between P and P ′′ , since the resulting success probabilities are 0.5 and 0.25, respectively. The term M2 distinguishes P and P ′ both in KΛN and in KΛV, since prob(SC( P ; M2⋆ )) = 0.5 and prob(SC( P ′ ; M2⋆ )) = 0. The same processes are distinguished by M3 in KΛ V-ref , which shows that the refusal operator is not necessary if the tested processes can be copied. Proof [Sketch] For the inductive equivalences, the proof schemata are as in the nondeterministic case. For item [START_REF] Bartels | GSOS for probabilistic transition systems[END_REF], in one direction we exploit a result in [START_REF] Van Breugel | Domain theory, testing and simulation for labelled Markov processes[END_REF]. Let T be the language of tests t defined as follows:

t ::= ω | r.t | (t1, t2)
Let P(t, P ) be the success probability for a test t on a reactive probabilistic process P . The test ω succeeds with probability 1, while a.t checks whether P can perform an a-labeled transition, and then executes t. Formally, if P a -→ ∆ then P(r.t, P ) = P ′ ∈ supp(∆) ∆(P ′ ) • P(t, P ′ ), else P(r.t, P ) = 0. Finally, P((t1, t2), P ) = P(t1, P ) • P(t2, P ), i.e. (t1, t2) checks P 's probability of passing both t1 and t2. On reactive probabilistic processes, P ∼PB Q iff P(t, P ) = P(t, Q) for every test t in T [START_REF] Van Breugel | Domain theory, testing and simulation for labelled Markov processes[END_REF]. We show that these tests are encodable in KΛ V-ref (some hints are provided by Example 3.1 and Example 3.4); i.e., for every test t in T there is a term Mt such that for every P , P(t, P ) = prob(SC( P ; Mt )). Hence, if P ∼PB Q then there is a context of KΛ V-ref that distinguishes P and Q. The same holds for the language KΛV, since it includes KΛ V-ref .

For the other direction, the proof is in two steps, analogously to the case of nondeterministic processes: we first prove that if P, Q are probabilistic bisimilar L processes and C is a λ-context, then also C[P ] and C[Q] are probabilistic bisimilar when the bisimulation game is only played on reductions and success (ω) transitions. We then prove that, if two λ-terms M, N are probabilistic bisimilar in this sense, then prob(SC(M )) = prob(SC(N )). A difficulty here is that M and N could have infinitely many successful computations, whose length is unbounded (e.g., Example 3.6). We then resort to a fixed-point approach. ✷ EXAMPLE 3.6. Let P def = a.(b +0.5 0) and M be λy.(λx. Seq Ta λ. if b? then true else x ; yy⋆ )pass In KΛV, the term P ; M M ⋆ with probability 0.5 reports success and with probability 0.5 becomes again P ; M M ⋆ . Thus, there are infinitely many successful computations from P ; M M ⋆ , and the overall success probability is 1. (Note that the typing of M requires recursive types.)

Concurrency: Syntax and Operational Rules

We present here the concurrent languages used to test the first-order processes taken from an LTS or RPLTS L. This section gives the syntax and operational rules. The following two sections study the equivalences induced by the languages. To simplify the presentation, we assume that also first-order communications exchange values, namely the unit value ⋆. Names include channels a, b, . . . and locations l, m, . . .. The operators are those common to CCS and higher-order π-calculi. The special prefix ω indicates success of a computation. We add the basic constructs of calculi with passivation, namely the kell [[M ]] l and the passivation prefix pass l (x).M . The refusal prefix r l .M , where l is a location containing L processes, succeeds if the process in l is unable to perform the action r. (The addition of other operators is discussed in Section 7.3.) Kells may be nested, and the kell structure is transparent with respect to communications. In the remainder, unless otherwise stated, all mentioned processes are supposed to be closed (without free variables). A channel or prefix is first-order or higher-order depending on whether the exchanged value is ⋆ or is a process. We sometimes abbreviate first-order prefixes a(x).M and a ⋆ .M as a.M and a.M , and omit the trailing 0 in α.0.

The language with all operators, HOπ pass,ref , is given in Figure 3. The subset without the refusal prefix is HOπpass; the subset without passivation is HOπ ref ; the subset without passivation and refusal is HOπ. These are the higher-order concurrent languages. In a first-order concurrent language, in contrast, all channels and prefixes are first-order (i.e., unit is the only communicable value) and the passivation prefix is disallowed. The resulting language is CCS - ref ; when also refusal is disallowed, the language is CCS -. (The '-' sign emphasizes the lack of the choice operator; see however Section 7.3.)

As usual, for any language, say AL, we write AL(L) for the extension of AL with the first-order processes from the LTS or RPLTS L, i.e., with the additional grammar production M := . . . | P where P is an L process. In the languages without passivation, the presence of kells is irrelevant; e.g., a process N | [[M ]] l behaves like N | M .

To avoid run-time errors in interactions, we assume a basic type system, that distinguishes three types of values: the unit value ⋆, the set PrL of tested L processes, and arbitrary processes Pr all , with the subtyping PrL ≤ Pr all . As a consequence, there are three types of names and variables. We distinguish the tested L processes from arbitrary processes because we allow refusal to act only on the former processes (this simplifies the operational rules, though it is not essential). For lack of space, we omit the (expected) typing rules.

Fully Nondeterministic Processes

The operational rules for the full language HOπ pass,ref (L), when L is an LTS, are presented in Figure 4. The grammar for action labels is:

µ := τ | a M | a M | ω | pass l M | pass l N | r l | r l
where a M , pass l M , and r l are the dual of, and synchronize with, a M , pass l N , and r l . The dual of µ is µ. In the languages without refusal (HOπpass(L), HOπ(L), CCS -(L)), rules REFLOC and REFPRE are missing; in the languages without passivation (HOπ ref (L), HOπ(L), CCS -(L), CCS - ref (L)), rules PASSLOC and PASSPRE are missing. Further, in the CCS languages the only value exchanged is ⋆.

Reactive Probabilistic Processes

If L is an RPLTS, the rules for parallel composition (Figure 5) propagate the probability distributions reached from the processes in L. For any ∆1, ∆2, we define the distribution:

∆1 | ∆2(M ) def = ∆1(M1) • ∆2(M2) if M = M1 | M2 0 otherwise
Differently from the contexts of λ-calculi, now the contexts are nondeterministic. Therefore, in general C[P ] is a nondeterministic and probabilistic term (i.e., an NPLTS).

CCS Languages: Separation Results

In the results on the concurrent languages, we include, in parenthesis, reference to the results for the λ-calculi to ease the comparison.

Fully Nondeterministic Processes

When L is an LTS, ≃ L CCS -coincides with ordinary may-testing equivalence [START_REF] De Nicola | Testing equivalences for processes[END_REF] and hence with ∼Tr, because the canonical tests of [START_REF] De Nicola | Testing equivalences for processes[END_REF] can be encoded without resorting to the choice operator. For a similar reason, ≃ L CCS - ref coincides with the refusal testing equivalence of [START_REF] Phillips | Refusal testing[END_REF] and hence with ∼FTr.

Reactive Probabilistic Processes

When L is an RPLTS, the contextual equivalences induced by CCS -and CCS - ref are comprised between ∼PB and ∼PFTr. THEOREM 5.1. If L is an RPLTS, then:

∼PB ≃ L CCS - ref ≃ L CCS - ∼PFTr ( = ≃ L KΛ N ) Proof [Sketch]
To prove the first inclusion, we exploit the congruence of ∼PB, and we observe that a probabilistic bisimulation relating C[P1] and C[P2] induces projections that are probabilistic bisimulations over pairs of maximal resolutions. Corresponding maximal resolutions turn out to have the same success probability, from which the result follows. The second inclusion is immediate.

To prove the third inclusion, given an arbitrary failure trace φ of length n, we consider the failure trace φ ω obtained from φ by replacing every pair (ai, Fi), 2 ≤ i ≤ n, with (a ω i , Fi). Moreover, starting from the processes P1 and P2 under consideration, we relabel with a ω i each transition executable after i steps, 2 ≤ i ≤ n, which departs from a process that does not enable any action in Fi-1. The result stems from the fact that the relabeling proceeds in the same way for P1 and P2 because, should this not be the case at step i, then the test with a single computation labeled with the first i -1 coactions and terminating with the parallel composition of the various coactions in Fi-1 followed by ω would separate the two processes.

The inclusion of ≃ L CCS -, and hence of ≃ L The different timing of the initial choices in R and R ′ is visible under bisimilarity but is not under the may semantics. (Intuitively, in the may semantics Q and Q ′ can only be distinguished by tests that exhibit success probabilities 1 and 0.5, respectively; we would need however a richer range of success probabilities to be able to separate R and R ′ .) ✷ 6. HOπ Languages: Separation Results

Fully Nondeterministic Processes

The proof schemata for Theorem 6.1 are as those for the analogous results in λ-calculi; in one direction we essentially encode the (higher-order) separating tests of the λ-calculi into the Higher-Order π-calculi. THEOREM 6.1. If L is an image-finite LTS, then:

1. ≃ L HOπ pass,ref = ∼RS ( = ≃ L KΛ V ); 2. ≃ L HOπ ref = ∼FTr ( = ≃ L KΛ N ); 3. ≃ L HOπpass = ∼S ( = ≃ L KΛ V-ref ); 4. ≃ L HOπ = ∼Tr ( = ≃ L KΛ N-ref
-→ ∆ 2 M 1 | M 2 τ -→ ∆ 1 | ∆ 2

Reactive Probabilistic Processes

The proof of Theorem 6.3(1) is analogous to the proofs for the λcalculi KΛV and KΛ V-ref . Again, in one direction we essentially encode the separating tests of the λ-calculi. For the opposite direction, we use a fixed point-point approach, but unlike in λ-calculi, now the definition of may-equivalence through suprema (Definition 2.10, following [START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF][START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF], as opposed to the definitions in [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF][START_REF] Segala | Testing probabilistic automata[END_REF]) is important, because of a potentially infinite number of resolutions.

Extensions and Variations

Global vs. Local Communications

In our concurrent languages, communications are network transparent, in the sense that they take place irrespective of the locations in which the interacting processes are placed. In the literature, this approach to communication is sometimes called global, as opposed to the local approach, where communication is subject to physical proximity. Under local communications, locations form communication barriers, because they confine where interactions can occur, with a finer control over communication interferences. We have checked that this extra precision in communications does not affect the discriminating power of the languages, when formalizing local communications as in the Kell calculus [START_REF] Schmitt | The kell calculus: A family of higherorder distributed process calculi[END_REF].

May vs. Must Equivalences

In the contextual equivalences we have used, success is in the 'may' style. The 'must' variants focus on the success of maximal τ -computations (i.e., whose steps are all labeled with τ ). In the LTS case, with respect to Definition 2.8 the preorder ≤ L AL,must is introduced by requiring that, if all maximal τ -computations from C[P1] are successful, then so are those from C[P2]. In the RPLTS case, the definition of ≤ L AL,must is obtained from Definition 2.10 by simply

DEFINITION 2 . 4 .

 24 A reactive probabilistic labeled transition system (RPLTS) is a triple (S, A, -→) where S is a countable set of states (usually called processes), A is a countable set of transitionlabeling actions, and -→ ⊆ S × A × Distr (S) is a transition relation such that P a -→ ∆1 and P a -→ ∆2 imply ∆1 = ∆2 for all P ∈ S and a ∈ A.

  Ta def = λ. if a? then true else false T a def = λ. if a? then false else true Seq def = λx.λy.λ. if x ⋆ then y ⋆ else false M1 def = Seq Ta ( Seq T c T b ) And def = λx.λy.λ.((λz. if x⋆ then z ; y⋆ else false)pass) M2 def = Seq Ta ( And T b Tc ) M3 def = Seq Ta ( And ( Seq T b Tc )( Seq T b T c ))

Figure 2 .

 2 Figure 2. The reduction rules of KΛ(L)

EXAMPLE 3 . 2 .

 32 (We reuse P ′ , M1, M3 from Example 3.1.) The processes P ′ and P ′′ def = a.(b + c) are distinguished in KΛN and KΛV (via the test M1), but they are equivalent in KΛ N-ref and KΛ V-ref . In contrast, only in KΛV the processes Q def = a.b.c + a.b and Q ′ def = a.(b.c + b) can be separated via test M3. Theorem 3.3 summarizes the results on the discriminating power of the four λ-calculi when the embedded processes are fully nondeterministic. Definition 2.8 of contextual equivalence is adapted to the λ-calculi supposing that the reduction relation -→ is labeled with τ and adding the rule: OMEGA N ; true ω --→ THEOREM 3.3. If L is an image-finite LTS, then: 1. ≃ L KΛ V = ∼RS (ready simulation equivalence); 2. ≃ L KΛ N = ∼FTr (failure trace equivalence); 3. ≃ L KΛ V-ref = ∼S (simulation equivalence); 4. ≃ L KΛ N-ref = ∼Tr (trace equivalence).

  proceeding as follows. Consider the computation C[P ] =⇒ ω -→. During this computation the hole may get duplicated, and therefore the context may become polyadic.

=

  Finally, only in KΛ V-ref and KΛV the test M4 distinguishes Q and Q ′ . P def = a.((b + c.d) +0.5 (f + c.e)) P ′ def = a.((b + c.e) +0.5 (f + c.d)) P ′′ def = a.(((b + c.d) +0.5 c.d) +0.5 (f + c.e)) Q def = a.(b.c +0.5 b) Q ′ def = a.b.(c +0.5 0) M1 def = Seq Ta ( T b ) M2 def = Seq Ta ( Seq T f ( Seq Tc T d )) M3 def = Seq Ta ( And T b ( Seq Tc T d )) M4 def = Seq Ta ( And ( Seq T b Tc )( Seq T b Tc )) THEOREM 3.5. If L is an RPLTS, then: ∼PB (probabilistic bisimilarity); 2. ≃ L KΛ N = ∼PFTr (probabilistic failure trace equivalence); 3. ≃ L KΛ N-ref = ∼PTr (probabilistic trace equivalence).

  is strict: the ∼PFTr-equivalent processes P def = a.((b.d + c.e) +0.5 (b.f + c.g)) P ′ def = a.(b.(d +0.5 f ) + c.(e +0.5 g)) are distinguished by the CCS -context [•] | a.(b.d.ω | c.g.ω)(calling C this context, the maximum probability of succeeding forC[P ] is 1, whereas that of C[P ′ ] is 0.5). The inclusion of ≃ L CCS - ref in ≃ L CCS -isstrict as well: the processes Q, Q ′ in Example 3.4 are not distinguished in CCS -, but they are distinguished by the CCS - ref context [[[•]]] l | a.(b.c.ω | b. c l .ω) (the maximum probabilities of success are respectively 1 and 0.5). Finally, probabilistic bisimilarity is strictly included in ≃ L CCS - ref , since the non probabilistic bisimilar processes R def = d.(e.Q +0.5 e.Q ′ ) R ′ def = d.e.(Q +0.5 Q ′ ) cannot be distinguished by any CCS - ref -context.

Figure 5 . 1 def=′ 2 def=

 512 Figure 5. The rules for parallel composition in the probabilistic setting

THEOREM 6 . 3 ..

 63 If L is an RPLTS, then: 1. ≃ L HOπ pass,ref = ≃ L HOπpass = ∼PB (= ≃ L The following processes witness the strictness of the inclusion of ≃ L HOπ in ≃ L CCS -: P def = d.Q + e.(f +0.5 0) P ′ def = d.Q ′ + e.(f +0.5 0) for Q, Q ′ as in Example 3.4. Processes P, P ′ , different under ∼PB, are identified by ≃ L CCS -. They are also separated in HOπ, via the context C def = h [•] | h(x).(x | d.a.(b.c.ω | b.(x | e) | f .ω)). Intuitively, this context uses higher-order communication to make copies of the tested process at the beginning, and then exploits the right-hand branch e.(f +0.5 0) of the process itself in order to test the left-hand branch.Analogously, let R, R ′ be as in Section 5.2 and define the processesS def = R + f.(g +0.5 0) + h.(i +0.6 0) S ′ def = R ′ + f.(g +0.5 0) + h.(i +0.6 0). It follows from R ≃ L CCS - ref R ′ that S ≃ LCCS - ref S ′ , while the HOπcontext C ′ distinguishes S and S ′ C ′ def = j [•] | j(x).(x | d.(e.a.T | e.(x | h.i.ω))) T def = b.c.ω | b.(x | f .g.ω). Since HOπ ⊆ HOπ ref , the example shows the strictness of the inclusion of ≃ L HOπ ref in ≃ L CCS - ref .

  The test M ′ 1 , below, in HOπ ref performs the same test as the term M1 in KΛN discussed in Example 3.1, while M ′

	µ

). EXAMPLE 6.2. In this example, we test a process P by placing it in a kell and then running a test M in parallel, as in [[P ]] l | M . The tests a.ω and a l .ω check whether P a -→ and P a -→, respectively.

Acknowledgments

The authors acknowledge support from the MIUR-PRIN project 'CINA', and the ANR project 12IS02001 'PACE'.

using ⊓ in place of ⊔, i.e., by considering the minimum probability of reaching success in the various maximal τ -resolutions.

The must-equivalences coincide with the may-equivalences when the tested processes are RPLTSs and the testing language is a λ-calculus, because internal nondeterminism does not occur. In contrast, nondeterminism may spring up when the testing language is concurrent, or when the tested processes are LTSs rather than RPLTSs. We discuss below a few scenarios in which must-and may-equivalences coincide despite the presence of nondeterminism.

Let us start with LTSs. Due to the absence of divergence, in CCS - ref the must-equivalence coincides with the refusal testing equivalence of [START_REF] Phillips | Refusal testing[END_REF] and hence with ∼FTr; thus, it coincides with the may-equivalence. In contrast, it follows from [START_REF] Nicola | Extensional equivalences for transition systems[END_REF] that in CCS - the must-equivalence coincides with ∼F and hence is strictly finer than the may-equivalence, which is ∼Tr. However, we can show that, if the testing language is KΛV or HOπ pass,ref , then also the reverse inclusion holds.

The refusal operator (respectively, the REFACT rule in λcalculus) is essential for the reverse inclusion to hold: the processes P

Other Operators

The concurrent calculi we have considered do not include certain common operators, such as restriction, recursion, relabeling, and choice, so to make the operational rules simpler or because often omitted in higher-order languages. The addition of these operators would not change the results presented (we assume that the hole of a context is not allowed to occur in recursive definitions). Some care is necessary with restriction in the presence of passivation, along the lines of [START_REF] Koutavas | Symbolic bisimulation for a higherorder distributed language with passivation[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF], because the lazy scope extrusion on restriction could allow contextual equivalence to make distinctions on processes solely on the basis of their free names [START_REF] Lenglet | Characterizing contextual equivalence in calculi with passivation[END_REF]. In HOπ we only allow communication of processes; the addition of process abstractions, or the name-passing communications of the π-calculus, as in the full HOπ, would not affect the results.

Conclusions and Future Work

We have studied the discriminating power offered by higher-order concurrent languages such as HOπ, without and with passivation, and contrasted it with those offered by higher-order sequential languages à la λ-calculus and by first-order concurrent languages à la CCS. We have measured this discriminating power on the basis of the distinctions that the languages, possibly extended with refusal, allow us to make on first-order processes that are either fully nondeterministic (LTSs) or reactive probabilistic (RPLTSs). The discriminating power of HOπ with passivation coincides with that of the call-by-value λ-calculus (with or without passivation), both on LTSs and on RPLTSs. Intuitively, HOπ with passivation and the call-by-value λ-calculus are both capable of implementing the 'and' of two tests. That is, the equivalence induced by these languages are characterized by modal logics that include the 'and' connective between formulas and are therefore 'branchingsensitive'.

The addition of refusal increases the discriminating power of all the considered languages when testing LTSs. This is not always the case on RPLTSs. One reason is that, similarly to fully probabilistic processes [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF], the spectrum of equivalences for RPLTSs is narrower than for LTSs.

On LTSs, the extra discriminating power offered in concurrency by passivation over higher-order communication corresponds, in λcalculi, to the call-by-value possibility of reducing the argument of a function and then capturing the result. The addition to the λcalculus of a pure sequencing construct M1; M2 akin to command sequentialization of imperative languages would not affect the results; in contrast, parametrized sequencing, e.g., pass(x) in M , would bridge the gap between call-by-name and call-by-value.

On RPLTSs, we do not know exactly what are the equivalences induced by CCS -and CCS - ref , though we know they are strictly in between probabilistic failure-trace equivalence and probabilistic bisimilarity. We are not aware of RPLTS equivalences in the literature with the same property. The lack of any copying facility makes the CCS -equivalence also strictly coarser than those of HOπ and of all other concurrent languages considered. Another question that remains is whether the equivalences induced by HOπ (with or without refusal) coincide, and whether they are strictly coarser than probabilistic bisimilarity.

Figures 6 and7 summarize the relationship among the various equivalences on a first-order LTS or RPLTS, respectively, that have been considered in the paper. In the figures, the name of a language, say AL, stands for the contextual equivalence ≃ L AL . A single arrow denotes a strict inclusion, unless the arrow is coupled with the reverse arrow and the question mark, in which case we do not know whether the inclusion is strict or not.

In the paper we have used LTSs/RPLTSs without internal moves, which means that the induced equivalences are 'strong', and we have looked at 'may' forms of contextual equivalence, discussing only a few instances of 'must' equivalence. Two natural developments of this work are thus (i) to systematically address the must-equivalences and (ii) to admit internal actions in the tested processes and therefore move to 'weak' behavioural relations.

We have admitted probabilities in the tested first-order processes, but not in the testing languages. It would be interesting to see if and how the addition of probabilities to the testing languages affects the results. Likewise, we have examined the equivalences induced on purely nondeterministic processes (LTSs), and on reactive probabilistic processes (RPLTSs), but we have not considered combinations of them; this would amount to studying whether the contextual equivalences induced on NPLTSs coincide with known probabilistic testing equivalences, e.g., [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF][START_REF] Deng | Testing finitary probabilistic processes[END_REF][START_REF] Segala | Testing probabilistic automata[END_REF] (characterized also as variants of simulation), or other behavioural relations are needed.


Charles Raux
email: charles.raux@let.ish-lyon.cnrs.fr

Stéphanie Souche
email: stephanie.souche@let.ish-lyon.cnrs.fr

Researcher

Assistant Professor L E T -Laboratoire D'

PERCEPTION OF THE FAIRNESS OF PRICING

Regulation by means of price in order to remove excess demand is generally perceived as being unfair. This paper empirically tests different principles of regulation including lotteries, rationing, a moral rule and compensation. We start from the postulate that the perception of the fairness of TGV and car park is important for a successful implementation. This perception is analysed through the results of an attitudinal survey held in Lyons area in 2003 (N ≈ 400). We confirm that peak-period pricing as a means of limiting demand is overwhelmingly rejected. Administrative allocation and lotteries are also rejected. The reference transaction can also lead to rejection of waiting line. Price compensation is overwhelmingly considered to be fair and the right to this is demanded both from public or private sector monopoly: it is possible therefore to reinstate pricing in the form of compensation. Those surveyed express rather definite preferences for some principles of regulation (moral rule, compensation) to the detriment of pricing or even the administrative or traditional regulation (queuing). Ways of unfreezing the situation are identified, who could be exploited in order to form coalitions likely to support this kind of policy. Finally, certain dimensions of the equity are revealed through the analysis of the survey.

INTRODUCTION

Since the seminal work of [START_REF] Pareto | Manuel d'Economie Politique[END_REF], [START_REF] Pigou | The Economics of welfare[END_REF][START_REF] Pigou | Economy progress in a stable environment[END_REF] and [START_REF] Samuelson | Foundations of Economic Analysis[END_REF], standard economic theory has established that regulation by means of price is an efficient means of allocating a scarce resource. As [START_REF] Glazer | Regulation by prices and by command[END_REF] and [START_REF] Brueckner | Airport congestion when carriers have market power[END_REF] have shown, this applies in all but very rare circumstances. The issue of regulating access to scarce resources by prices is crucial for public goods which are subjected to congestion, for example in the transport sector where pricing is the accepted means of regulating congestion [START_REF] Dupuit | De l'influence des péages sur l'utilité des voies de communication[END_REF], [START_REF] Pigou | The Economics of welfare[END_REF], [START_REF] Vickrey | Pricing in urban and suburban transport[END_REF]). This use of prices to eliminate excess demand can however be perceived as unfair when the exchange fails to take account of the reference transaction defined by Kahneman, Knestsch, and Thaler (KKT, 1986). Slightly provocatively, [START_REF] Frey | On the fairness of pricing -an emprical survey among the general population[END_REF], and Oberholzer-Gee and [START_REF] Oberholzer-Gee | Pricing road use: politico-economic and fairness considerations[END_REF], hold that economists lay too much emphasis on the role of pricing as a means of regulation and argue that ethical considerations should be taken into account when attempting to gain acceptance for policies involving regulation by prices. Resistance to the introduction of new pricing measures is also observed in the transport sector [START_REF] Raux | The acceptability of urban road pricing: a theoretical analysis applied to experience in Lyon[END_REF]. This resistance has prompted us to test whether, in a context of scarce resources, regulation by prices is actually rejected by the population, and if so, to what extent. We shall attempt to test empirically different principles of regulation including lotteries, rationing, a moral rule and compensation in order to see if these receive more support than regulation by prices. Our results partially invalidate the above findings from the literature. They confirm the role of the reference transaction and also show that other regulation principles may be considered to be less unfair, or even fairer, than pricing on its own. Based on a survey of the empirical and theoretical literature we have formulated questions which we shall go on to test empirically. We shall then present the methodology used in the study which relates to situations in which the supply of rail transport and parking supply is scarce. Last, we shall set out our principal findings showing whether or not they validate our hypotheses.

LITERATURE SURVEY AND TESTED HYPOTHESES

In a seminal paper on this topic, Kahneman, Knestsch, and Thaler (KKT, 1986) established, with empirical backing, the existence of a dual entitlement by which "transactors" have a right over the terms of the reference transaction while the firm also has a right over the reference profits. Slightly provocatively, Frey and Pommerehne (FP, 1993) asked the following question: how can the regulation of excess demand by prices be considered to be unfair when economists recommend it as a principle? In the face of a situation where water is scarce, these authors identified and tested several procedures for allocating resources each of which implemented a different principle of justice. For the rationing of excess demand they found that a classical "first come, first served" procedure or an administrative procedure are considered fairer than a pricing procedure which consists of paying more for resources which have become scarce. On this basis, they conclude that economists should include moral or ethical aspects in their analysis if they wish to increase their ability to guide policy. In connection with a public good, Frey and Oberholzer-Gee (1996) have also shown that when it is necessary to decide on the siting of a public good which is not welcome locally, compensation is insufficient and procedures which are perceived as fair should play an essential role. [START_REF] Vaidyanathan | Who is the fairest of them all? An attributional approach to price fairness perceptions[END_REF] reconsidered the dual entitlement in the reference transaction and showed that a price rise, even one which is justified on the grounds of costs, can be considered to be less fair when it is the result of a deliberate choice on the part of the vendor. [START_REF] Bolton | Consumer perceptions of (un)fairness[END_REF] demonstrated that consumers are sensitive to certain reference points (past prices, competitors' prices, cost of the goods sold) but underestimate the effects of inflation: they overestimated the extent to which price differences are the result of vendor's profits and fail to take account of all the latter's costs. On the basis of the persisting resistance to wider use of pricing for regulating excess demand in the case of transport for example, we firstly wished to test the current validity of the foregoing empirical results and secondly to explore further attitudes to certain principles of allocation. A number of questions emerged from our survey of the theoretical and empirical literature and we shall investigate these empirically. The first question relates to the constancy of the rejection, highlighted by the literature survey, of the use of prices to allocate scarce resources. Question 1: is the principle of allocating scarce resources by prices always rejected? Next, we attempted to explore more fully the terms of this rejection by investigating different situations in which the principle is implemented. The first situation relates to whether the situation of excess demand is foreseeable or not. Frey and Pommerehne have shown that people are less averse to pricing in a recurring situation where they expect supply to be increased than in an exceptional situation where pricing serves to ration demand. For this reason it is important systematically to explore variations in attitudes according to whether the regulation measures are applied in a recurring or an exceptional situation. Second, FP have shown that the regulation of excess demand by pricing, for example in the case of water sales at a tourist site, was more strongly rejected in the case of a public sector supplier than a private supplier. This question is important when a private operator is used to produce a public good, as is the case today with many public services and the increasing interest in public-private partnerships, for example for water or transport. Question 2: is there a difference between a rejection of the principle of regulation by prices depending on whether the supplier belongs to the public or the private sector? If rejection occurs, we can wonder if other procedures, whose underlying principles are easier to explain, would gain better acceptance. FP have shown, for example, that the rule of allocation by pricing was perceived as being less fair than a bureaucratic procedure in which the administration made allocations on the basis of its own judgment; on the other hand this rule was considered to be fairer than a random allocation procedure. [START_REF] Taylor | Lottery or waiting-line auctions?[END_REF] found that in the absence of a system of pricing, the lottery is generally more socially acceptable than queues. According to the economic theory of bureaucracy [START_REF] Niskanen | Bureaucracy and representative government[END_REF] the bureaucratic procedure is considered to be intrinsically particularly unfair. We can therefore assess the degree of acceptance of these procedures in order to use them as reference values for calibrating the other procedures. Question 3: are lotteries or administrative allocation better accepted than regulation by prices as a means of dealing with excess demand? Another factor which may influence the perception of regulation by prices relates to the possibility of controlling the use of revenue. This is a principle of economic justice set forth by Zajac, in the context of the improper power of a monopoly: "The fewer the substitutes for a regulated or monopoly firm's output, and the more the output is considered an economic right, the more the public expects to exert control over the firm. Denial of control is considered unjust." (Zajac, 1995, p. 127). Question 4: does the possibility of controlling the use of revenue derived from pricing moderate the rejection of regulation by prices? With regard to the control of the use of revenue from pricing, given the results of [START_REF] Vaidyanathan | Who is the fairest of them all? An attributional approach to price fairness perceptions[END_REF] and [START_REF] Bolton | Consumer perceptions of (un)fairness[END_REF], it therefore seemed interesting to see whether the proposal of additional supply which justifies the price increase can modify negative attitudes to regulation by prices. Question 5: can providing additional supply which is related to the price increase make this increase more acceptable? The question of compensation naturally arises. It has been established since the work of [START_REF] Hicks | The Foundations of Welfare Economics[END_REF] and [START_REF] Kaldor | Welfare propositions in economics and interpersonal comparisons of Utility[END_REF] that in the context of a standard cost-benefit analysis, hypothetical compensation can justify a policy as long as the benefits accruing to the winners exceed the losses sustained by the losers. So, in principle, effective compensation could counterbalance the rejection of the mechanism of allocation by pricing. Lastly, Zajac's principles of economic justice include the right to insurance: "Society is expected to insure individuals against economic loss because of economic changes. Failure to insure is considered unfair." (Zajac, 1995, p. 123). However, it seems that this principle of compensation will be rejected because the "compensated losers" feel that their votes are beings "bought" (the so-called "bribe effect") in order for the wealthy to be able to benefit from the goods which are thereby made available (Frey et al., 1996;[START_REF] Kunreuther | The role of compensation in siting hazardous facilities[END_REF]. This is why Oberholzer-Gee and [START_REF] Oberholzer-Gee | Pricing road use: politico-economic and fairness considerations[END_REF] suggest that compensation should take a form which is like the purchase of votes as little as possible and attempt to reward those who are willing to reduce their consumption of the scare good in the same "dimension" as the loss because they make a contribution to improving collective wellfare. We have therefore attempted to test explicitly whether a compensation mechanism might change the attitude to the mechanism of allocation by pricing. Question 6: does offering compensation which belongs to the same "dimension" to those whose demand has been removed improve acceptance of regulation by prices? A last set of regulation principles represents what can be considered as the classical basis of the "reference transaction". These principles of regulation are widely used in all administrative or commercial departments: queueing (or the "first come, first served" procedure) is a form of rationing. [START_REF] Barzel | A theory of rationing by waiting[END_REF] shows that the redistribution of a good which is limited in quantity through queueing can be costly and does not systematically benefit the poor. Application of a moral rule, for example giving priority to persons with reduced mobility, may be based on Rawls ' (1971) two principles of equality of chances and difference. Question 7: are the principles which form the classical basis of the reference transaction such as queues and a moral rule, universally perceived as fair? Last, in relation to these principles of allocation, in particular allocation by pricing, it is important to establish whether an individual's economic situation influences his/her attitude. [START_REF] Weitzman | Is the price system or rationing more effective in getting a commodity to those who need it most?[END_REF] has shown that the relative efficiency of pricing or rationing for allocating a scarce resource to those who need it most depends on how the need in question and incomes are distributed. According to [START_REF] Sah | Queues, rations, and market: comparisons of outcomes for poor and the rich[END_REF] the poor would gain more from rationing and the rich from the market. It is therefore legitimate to raise the issue of the relative extent to which attitudes are influenced by income and pricing. Question 8: do attitudes vary according to the economic and social situation of individuals?

The above questions have been the subject of an empirical investigation using the questionnaire and survey which we shall now describe.

METHODOLOGY

The survey was conducted in January 2003 and involved face-to-face interviews of a sample of 400 persons who were representative i of the inhabitants of the Lyon conurbation (population 1.2 million). The respondents were told four different "stories". Although fictional, these stories described situations which were grounded in reality (the Paris-Lyon train or urban parking). Various solutions were proposed for solving excess demand and respondents were asked if they found each of the solutions essentially fair or essentially unfair ii . Two of the stories involved the allocation of seats in the situations of excess demand in the case of the high speed train (TGV) between Paris and Lyon (450 km), which is operated by a public sector company, French National Railways (SNCF). As a general rule, only passengers with reservations can use this train. The first story describes an exceptional situation on a Friday evening: as a result of very bad weather (e.g. a snow storm), only one of the three scheduled trains was able to run. The second story describes a recurring situation of excess demand, in which rising demand has led to intolerable saturation of the service. Two other stories dealt with the problem of assigning parking spaces at the car park of a firm with premises in the centre of a major city in which it is very difficult to find parking in the surrounding area. In one case, the situation was exceptional: construction work lasting several months was necessary in the car park which made two-thirds of the parking spaces temporarily unavailable. In the other case, the situation of excess demand was recurring, the firm was extending its premises by building over part of the existing car park. Each respondent was only told two stories, one about the TGV and the other about parking; in addition, each was told only about the exceptional or the recurring situations. Consequently, each of the four stories was told to half the sample iii . The same regulation principles were proposed for each of the four stories. The regulation principles we tested are based on the questions listed in the previous section. In addition, the scenarios proposed allowed us to test any differences in attitude between the public sector operator (SNCF in the case of the train) and the private sector operator (a company in the case of parking).

• "Peak period pricing with constant supply": for both the TGV and parking, the proposal to cope with excess demand was to pay an additional charge. In the case of parking, two alternative proposals were also made with regard to the allocation of revenue, in one case it was possible to exert control over its use: in one of the alternatives, the revenue was handed over to the firm, and in the other to the firm Works Council iv . • The "unknown administrative rule": in the case of the TGV this consisted of letting the ticket inspectors allocate the available seats, and in the case of parking of letting either the firm management or the Works Council allocate the available seats. These last two alternatives enabled us also to test the impact of the ability to monitor the allocation of demand. • A "lottery": this consisted of distributing the available seats on a random basis in the case of both the TGV and parking. • "Peak period pricing with additional supply": in the case of the TGV, the operator was assumed to have run additional trains which were paid for by the increased price, while in the case of parking, the company rented additional parking spaces in a nearby car park. • "Peak period pricing with compensation" in the case of the TGV, in the exceptional situation, the proposal was to compensate those who were willing to take the train the next day. In the case of recurring excess demand, we suggested reducing the price of the ticket below the normal price for those who were willing to leave earlier or later. In both situations for company parking, we proposed compensating those who were willing not to park in the firm's car park. • "Queues": in the case of the TGV, the train was allowed to fill, and in the case of parking the car park was allowed to fill. • A "moral rule": this consisted in both cases of giving priority to persons with reduced mobility (pregnant women, elderly and handicapped persons).

RESULTS

The rejection of peak period pricing

Peak period pricing with constant supply was overwhelmingly perceived to be unfair in all the situations. For example, for the TGV (10% fair, see v2 in Table 1 in the Appendix) and for parking when revenue adds to the firm's takings both in the exceptional situation (7% fair, see Table 2, v11) and the recurring situation (10% fair).

The situations described here all involve excess demand. However, this excess demand occurs in circumstances in which it is reasonable to assume that individuals consider to be outside their control. This view is supported by the fact that constant supply peak period pricing is significantly perceived as a little less unfair in the recurring situation (see Table 3, v2, in Appendix): it is as though, when faced by a reoccurrence of excess demand, individuals consider that the introduction of peak period pricing is less unacceptable because it would have been possible to take measures beforehand to avoid the peak.

Exceptional administrative regulation

For both the TGV and parking, exceptional administrative solutions in the form of an unknown administrative rule or a lottery are overwhelmingly rejected and considered to be barely less unfair than pricing (see Table 1, v4 andv5). This finding concurs with those of FP for the lottery, but is quite different for the unknown administrative rule as FP found the unknown administrative rule to be better accepted than pricing.

In the case of parking, we wished to test whether there was a difference in attitudes according to the administration in charge of allocating available spaces. To do this, we made a distinction between the Management of the Firm (MF) and the Works Committee (WC). The decisions taken by the works committee could be influenced by members of the workforce who are elected to it by virtue of periodic elections and this can help create some hope of compensation which is absent when it is just the management of the firm that distributes parking spaces. However, contrary to our expectations, our findings indicate that there is no significant difference depending on whether the available spaces are allocated at the discretion of the firm or works committee (see Table 2, confidence intervals for the medians of the variables v16 and v17).

To summarize, neither the activities of the inspector on the train, nor those of the management of the firm, nor those of the works committee find favour with the respondents. This rejection can be explained by the dominant position of the administrative authorities which are perceived as holding a monopoly of power. Individuals have no, or almost no, margin for manoeuvre. As Zajac has explained (1995), use of a monopoly of power is perceived as being extremely unfair (see above). Last, in the case of both TGV and parking, the lottery was widely rejected: we can interpret this as expressing strong risk aversion among individuals or as defiance in the face of an unusual procedure.

The role of the allocation of revenue from pricing

Do attitudes towards the pricing instrument vary according to how the revenue from it is allocated? We have attempted to establish this first of all by considering pricing with constant supply where revenue can be allocated in different ways. In the case of peak period pricing with constant supply the two alternatives for parking were allocation of revenue to the firm and allocation of revenue to the works committee. Peak period pricing with constant supply is perceived as being significantly fairer when the revenue derived from pricing is handed over to the works committee (28% in the case of recurring scarcity, 37% in the case of exceptional scarcity, see Table 2, v12) than when this revenue goes into the firm's coffers (10% in the case of recurring scarcity, 7% in the case of exceptional scarcity, v11) v .

The first lesson we can draw from these results is that the rejection of peak period pricing with constant supply is not intractable. Negative attitudes can be significantly moderated by how the revenue is allocated, as shown by the example of parking.

As our starting point we can interpret these findings with reference to Zajac's principle of economic justice, in connection with the improper power of a monopoly (see above). In this case we have two types of monopoly, a public sector monopoly consisting of the railway company (SNCF), and a private sector monopoly consisting of the company that owns the car park. We can nevertheless see what the problem is with the monopoly. We should bear in mind that our results have shown that attitudes to peak period pricing are intensely negative whether the supplier belongs to the public sector (train) or the private sector (parking). These findings tend to show that negative attitudes to peak period pricing are not influenced by the public or private nature of the entity offering the good or service, as suggested by [START_REF] Frey | On the fairness of pricing -an emprical survey among the general population[END_REF], but more by where the revenue goes, as we have seen in the case of parking.

The increase in supply and the acceptability of pricing

We also tested attitudes towards the pricing instrument in a second context in which the provision of additional supply, either in the form of extra trains or additional parking spaces, incurs additional costs, which may provide a rational justification for price increases. It should not be forgotten that in the case of the parking scenario, the firm was assumed to have rented the lacking parking spaces in a nearby private car park and made those of its employees who used their cars cover the cost of this (v20).

In the case of the TGV, the railway company (the SNCF) was assumed to have paid for extra trains which were funded by charging extra for tickets (v8).

Peak period pricing with additional supply is nevertheless perceived as being unfair: only 29% of respondents consider it to be fair for the TGV in the case of recurring congestion (Table 1,v8), 38% consider it fair for recurring parking congestion and 51% consider it fair in the case of exceptional parking congestion (Table 2, v20) vi . However, these solutions were not as strongly rejected as peak period pricing with constant supply (see above).

The first lesson is that additional supply which accompanies a price rise can, like the way revenue is allocated, reduce opposition among respondents, or even divide those for and those against into two approximately equal groups. Our results are to some extent consistent with those of FP who noted less price aversion in the recurring situation when respondents expect supply to be increased. However, our survey differs from that of the above authors as the solutions proposed to respondents explicitly mention the additional supply which accompanies the price rise. We have observed that this information changes very little in the attitudes of respondents which remained generally unfavourable. Does this mean it would be advisable to provide additional explanations to gain the approval of consumers? This is not what is suggested by the work of [START_REF] Bolton | Consumer perceptions of (un)fairness[END_REF] and [START_REF] Vaidyanathan | Who is the fairest of them all? An attributional approach to price fairness perceptions[END_REF]: however, our results do not prompt the same conclusion as, in the case of the TGV, attitudes towards peak period pricing with additional supply are less negative than towards peak period pricing with constant supply (compare v8 with v2 in Table 1). Moreover, for parking, the provision of additional supply (v20), in both exceptional and recurring congestion situations gives an unexpected result. Peak period pricing with additional supply is considered to be significantly fairer (see Table 4 in the Appendix, v20, test U) in the case of exceptional congestion (51%, see Table 2, v20) than in the recurring situation (38%). It therefore does not seem to be the recurring nature of the situation which makes pricing more acceptable, because in this case people would expect additional supply. It is the very fact of providing additional supply which makes pricing more acceptable, and potentially the recurring nature of the situation in which this solution is applied could even make it less acceptable.

The right to compensation

If negative attitudes to the use of peak period pricing to solve problems of excess demand were to be confirmed, is there any alternative means of pricing which might gain approval? Unlike peak period pricing with constant supply, compensation is overwhelmingly considered to be fair in the case of the TGV in the recurring situation (80%, see Table 1, v7), parking in the recurring situation (89%, see Table 2; v19), parking in the exceptional situation (93%, v19) and the TGV in the exceptional situation (95%, Table 1, v7). The right to compensation is therefore strongly reaffirmed. However, our results go further than this, as compensation is expected not only from society via a public monopoly (the public sector railway company) but also from a private monopoly (the private company that owns the car park). The principle of compensation stands out among our results as it is the principle which is considered to be the fairest, with the principle of a moral rule, in all the situations. Another lesson we can draw relates to the additional supply mentioned above: providing additional supply in the context of peak period pricing can also be regarded as a form of compensation. Our results show that it is perceived as being extremely indirect and hypothetical: support for this type of solution is much lower than support for direct compensation as we can see if we compare the pricing solutions with additional supply with the solutions with direct compensation (compare V8 and V7 in Table 1and V20 and V19 in Table 2). It is of course the case that pricing is overwhelmingly rejected as a means of limiting excess demand. But this does not mean that pricing must be rejected as an instrument in all cases: our results show that its use in the form of compensation may be considered fair by the vast majority of people.

The reference transaction, moral rule and queueing

For KKT (1986), the feeling of unfairness appears when the exchange no longer takes account of the reference transaction. The concept of reference transaction allows us to understand the perception of justice linked to the principles of the moral rule and queueing.

For both the TGV and parking scenarios, the principle by which seats and spaces are allocated on the basis of a moral rule is considered to be very fair (between 70% and 90% in the case of the TGV, more than 90% in the two parking situations; see respectively Table 1, v3 andTable 2, v14). In both cases, the reference transaction involved application and compliance with this moral rule.

In the case of queueing, our findings are slightly different. According to our results, queueing is not always considered to be the fairest means of allocation in the case of a problem of scarcity: this runs counter to the conclusions reached by FP, for whom the traditional "first come, first served" procedure is greatly preferred to pricing. While the principle of queueing is considered to be fair in the case of parking (68% in the exceptional situation, 69% in the recurring situation, see Table 2, v18), it is in contrast considered to be essentially unfair in the case of the TGV where the difference between the different types of situation is significant (only 37% considered queueing fair in the exceptional situation, and 33% in the recurring situation, see Table 1 and Table 3 in the Appendix, v6).

In the case of parking, management by means of queueing seems to be well accepted and has therefore been incorporated into the reference transaction. In contrast, in the case of the TGV, the reference transaction is based on a system of seat reservation which means that the management of scarcity by means of queueing is negatively perceived.

To sum up, the management of scarcity in the case of company parking shows that the reference transaction is constructed on the basis of the combined application of the moral rule and queueing. In the case of the TGV, the reference transaction is based on a moral rule and a system of reservation.

Our results show that the reference transaction modifies the way in which a principle of justice which is commonly considered to be "fair", such as queueing, is perceived. Do these attitudes vary according to the social and economic situation of individuals?

We have conducted systematic (Kruskall-Wallis) tests to see whether attitudes towards these principles of regulation vary as a function of the personal socioeconomic characteristics of the respondents, namely gender, age and educational level(we have used the latter as an approximate guide to an individual's income).

Apart from in two situations, the influence of socioeconomic characteristics is statistically not significant.

These findings therefore do not invalidate the hypothesis that the attitudes expressed here by respondents are of a generic nature and independent of their personal situation. It is as though our respondents had placed themselves behind Rawls' veil of ignorance (1971).

CONCLUSION

Our results confirm the overwhelming rejection of peak period pricing as a means of regulating excess demand. However, the results give the impression that confronted by a repeated situation of excess demand, people find peak period pricing slightly more acceptable because it is possible to take steps beforehand in order to avoid the peak.

The use of administrative procedures or lotteries to allocate seats or parking spaces is also rejected. Our results to some extent invalidate previous work which found that administrative allocation was perceived to be fairer than the pricing solution. It would seem that attitudes towards this principle of allocation depend on how much confidence people have in those managing it. The rejection of peak period pricing with constant supply is not intractable: people's opposition can be reduced if they can influence how the monopoly uses the revenue. However, whether monopoly in question belongs to the public or private sectors does not affect the intensity of opposition to peak period pricing. Accompanying a price rise with an additional service or infrastructure reduces opposition in the same way as the right to influence the use of revenue, but the negative attitudes nevertheless subsist. It is the additional supply which makes pricing more acceptable and not the context of recurring congestion in which this solution is applied, rather the contrary. The moral rule is judged to be very fair in all cases. However, we have shown that managing scarcity with queues, although generally considered to be one of the fairesttool, is not universally considered to be so. The reference transaction may lead to a rejection of the management of scarcity by means of queueing, for example in the case of a service which is generally accessed by means of a reservation system. Last, our results allow us to moderate conclusions which are on first view rather pessimistic from the economic standpoint by showing that compensation, which is overwhelmingly considered to be fair, can radically modify attitudes of rejection with regard to the pricing instrument. The right to compensation is overwhelmingly demanded from the monopoly holder, whether it belongs to the public or private sector: it could therefore be possible to rehabilitate pricing in the form of compensation. ii The initial four possible responses (very unfair, essentially unfair, essentially fair, very fair) were reclassified into two categories (unfair, fair) when presenting the results. For each story, each solution was presented independently of the others. Moreover, the order in which the solutions were presented was systematically varied for each respondent in order to avoid the bias that might arise if the solutions were always presented in the same order.

APPENDIX: STATISTICAL TESTS

iii The full questionnaire (in French) can be obtained from the authors. The survey was conducted by the Lyon-based conslutancy firm Tremplin.

iv This body is elected by the workforce of the firm and therefore assumed to represent its interests.

v It is nevertheless noteworthy that the difference between the exceptional situation and the recurring situation is not significant in the case of the two types of revenue allocation (see Table 4, v11 and v12).

vi Although the difference between the median values of the last two solutions is not significant, as seen in Table 2, the result of the Mann-Whitney test is significant and indicates that the distributions differ, see Table 4 (v20).

Table 1 :

 1 The case of the TGV. Median values with their confidence intervals, % fair

	Context	Median Lowe	Upper %
		r	essentially
			or very fair

Table 2 :

 2 The case of parking, median values with their confidence intervals, % fair

		Our coding:	Context	Median Lowe	Upper %
					r		essentially
							or very fair
	v1	Unknown administrative rule (MF*)	exceptional	3.0	3.0	3.5	8 %
	6
	v1	Peak period pricing with constant supply	exceptional	3.5	3.0	3.5	7 %
	1	(MF)
	v1	Peak period pricing with constant supply	recurring	3.5	3.0	3.5	10 %
	1	(MF)
	v1	Unknown administrative rule (MF)	recurring	3.5	3.0	3.5	10 %
	6
	v1	Unknown administrative rule (WC**)	exceptional	3.5	3.5	3.5	13 %
	7
	v1	Lottery	recurring	3.5	3.5	4.0	12 %
	5
	v1	Lottery	exceptional	3.5	3.5	4.0	17 %
	5
	v1	Unknown administrative rule (WC)	recurring	4.0	3.5	4.0	14 %
	7
	v1	Peak period pricing with constant supply	recurring	5.0	4.5	5.5	28 %
	2	(WC)
	v1	Peak period pricing with constant supply	exceptional	5.5	5.0	6.0	37 %
	2	(WC)
	v2	Peak period pricing with additional supply recurring	6.0	5.0	6.5	38 %
	0
	v2	Peak period pricing with additional supply exceptional	6.5	6.0	7.0	51 %
	0
	v1	Queueing	exceptional	7.5	7.5	8.0	68 %
	8
	v1	Queueing	recurring	8.0	7.5	8.0	69 %
	8
	v1	Compensation	exceptional	8.5	8.5	9.0	93 %
	9
	v1	Moral rule	recurring	9.0	9.0	9.0	91 %
	4
	v1	Compensation	recurring	9.0	9.0	9.0	89 %
	9
	v1	Moral rule	exceptional	9.0	9.0	9.5	96 %
	4
	* MF = Management of the Firm, ** WC = Works Council.

Table 3 :

 3 for the TGV, tests of the differences between a situation of temporary and recurring congestion

			Median:	Transf. Similar	KS Test *	U Test **
			exceptional recurring		distributions ?	p***	p***
	v4 Lottery		2.5	no	yes	0.078	0.03
			2.0
	v5 Unknown	administrative	2.0	Log	yes	0.0001	< 0.0001
	rule		2.5
	v2 Peak period pricing with	2.0	Log	yes	< 0.0001	< 0.0001
	constant supply	3.0
	v6 Queueing		3.5	Log	yes	< 0.0001	< 0.0001
			4.0
	v3 Moral rule		5.5	Log	approx.	< 0.0001	< 0.0001
			6.0
	v7 Compensation	5.5	Log	approx.	< 0.0001	< 0.0001
			6.0

Table 4 :

 4 case of parking, tests of the differences between the temporary and recurring situations of congestion. Whitney test *** bilateral test, the value of p is compared to the significance threshold alpha/2=0.025 i Random selection on the basis of quotas (residential location, age groups, gender, economically active/inactive).

		Our coding:	Median:	Transf.	Similar	Test KS*	Test U**
			exceptional recurring		distributions ?	p***	p***
	v1	Peak period pricing with	3.5	no	yes	0.515	0.264
	1	constant supply (MF)	3.5
	v1	Peak period pricing with	5.5	Log	approx.	0.194	0.052
	2	constant supply (WC)	5.0
	v1	Moral rule	9.0	Log	approx.	0.884	0.253
	4		9.0
	v1	Lottery	3.5	Log	approx.	0.406	0.143
	5		3.5
	v1	Unknown administrative rule	3.0	Log	approx.	0.523	0.038
	6	(MF)	3.5
	v1	Unknown administrative rule	3.5	no	yes	0.385	0.018
	7	(WC)	4.0
	v1	Queueing	7.5	no	yes	0.975	0.270
	8		8.0
	v1	Compensation	8.5	no	yes	0.031	0.009
	9		9.0
	v2	Peak period pricing with	6.5	no	yes	0.031	0.005
	0	additional supply	6.0
	* Kolmogorov-Smirnov test
	** Mann-

ACKNOWLEDGEMENTS

This paper is based on research that was subsidized by the ADEME (French Environment and Energy Conservation Agency, Agreement no. 00 03 040).