Gethin Norman

Catuscia Palamidessi

Peng David Parker

Model checking probabilistic and stochastic extensions of the π-calculus

Model checking probabilistic and stochastic extensions of the π-calculus Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu

Abstract-We present an implementation of model checking for probabilistic and stochastic extensions of the π-calculus, a process algebra which supports modelling of concurrency and mobility. Formal verification techniques for such extensions have clear applications in several domains, including mobile ad-hoc network protocols, probabilistic security protocols and biological pathways. Despite this, no implementation of automated verification exists. Building upon the π-calculus model checker MMC, we first show an automated procedure for constructing the underlying semantic model of a probabilistic or stochastic π-calculus process. This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we demonstrate how for processes of a specific structure a more efficient, compositional approach is applicable, which uses our extension of MMC on each parallel component of the system and then translates the results into a high-level modular description for the PRISM tool. The feasibility of our techniques is demonstrated through a number of case studies from the π-calculus literature.

Index Terms-Verification, Model checking, Markov processes, Stochastic processes

I. INTRODUCTION

T HE π-calculus [1] is a process algebra for modelling concurrency and mobility. It has been used to model, for example, communication protocols for dynamic network topologies, security protocols and biological pathways. For each class of systems, probabilistic and stochastic behaviour are often also key ingredients. Mobile ad-hoc network protocols, for example, can exhibit probabilistic behaviour through either communication failures or random back-off procedures. Similarly, randomisation is frequently applied in security protocols, e.g. for anonymity [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] or contract-signing [START_REF] Even | A randomized protocol for signing contracts[END_REF]. For biological systems, the times between reactions are of a stochastic nature.

Consequently, suitable variants of the π-calculus have been developed: probabilistic versions, for example [START_REF] Herescu | Probabilistic asynchronous π-calculus[END_REF], which extend the original calculus with discrete probabilistic choice, have been proposed as a formalism to model and reason about randomised security protocols [START_REF] Chatzikokolakis | A framework to analyze probabilistic protocols and its application to the partial secrets exchange[END_REF], [START_REF] Bhargava | Probabilistic anonymity[END_REF]; and stochastic extensions, for example [START_REF] Priami | Stochastic π-calculus[END_REF], which augment the calculus with exponential delays, have been shown to be a suitable formalism for modelling and reasoning about complex biological pathways [START_REF] Regev | Representation and simulation of biochemical processes using the π-calculus process algebra[END_REF], [START_REF] Priami | Application of a stochastic name passing calculus to representation and simulation of molecular processes[END_REF].

The benefits of automatic formal verification and tool support in this context are clear: reasoning correctly about the behaviour of such models, particularly interactions between probabilistic and nondeterministic behaviour, is known to be G. Norman non-trivial. Furthermore, the state spaces of probabilistic or stochastic models of realistic systems have a tendency to grow extremely quickly, making manual verification difficult or infeasible.

In this paper, we describe an implementation of probabilistic model checking for models described in two different extensions of the π-calculus. The first, the simple probabilistic π-calculus, is an extension of the π-calculus obtained by introducing a discrete probabilistic choice operator in addition to the existing nondeterministic choice operator. The second, the stochastic π-calculus, extends the original calculus by associating rates (parameters of exponential distributions) with both silent transitions and channels.

Our approach is to adapt and reuse existing tools for verification of mobile systems and of probabilistic and stochastic systems. We first developed an extension of the tool MMC [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF], a logic-programming-based model checker for the πcalculus. This extension, MMC prob , can derive the semantic model for an arbitrary process in the (finite-control) probabilistic or stochastic π-calculus. The semantic model, which is given by a Markov decision process (MDP) or continuous-time Markov chain (CTMC), can then be analysed using standard tools, such as the probabilistic model checker PRISM [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF]. To improve efficiency, when the process has a specific structure, we employ a compositional approach, applying MMC prob to each parallel component of a system, processing the results to produce a high-level modular description in the modelling language of PRISM and then performing probabilistic verification. This avoids a potential blow-up in the size of the intermediate MDP or CTMC representation and allows us to exploit the efficient symbolic model construction and analysis techniques in PRISM. We present experimental results to illustrate the performance of our implementation on a number of case studies. To our knowledge, this paper constitutes the first attempt to implement automated verification in this area.

Related work:

Various tools exist for automatic verification of the (non-probabilistic) π-calculus. The Mobility Workbench (MWB'99) [START_REF] Victor | The Mobility Workbench -a tool for the πcalculus[END_REF] provides a bisimulation checker and a πµ-calculus model checker. MMC (Mobility Model Checker) [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF], a more recently developed tool, also supports the π-µcalculus. The latter places particular emphasis on efficiency and is built using logic programming technology. ProVerif [START_REF] Blanchet | ProVerif: Automatic cryptographic protocol verifier user manual[END_REF] supports verification of the applied π-calculus, a variant of the basic calculus. It is aimed primarily at analysis of cryptographic protocols and is theorem-prover based. Two alternative approaches are the PIPER system [START_REF] Chaki | Types as models: Model checking message-passing programs[END_REF], which verifies π-calculus processes augmented with type signatures based on an extraction of sound models using types and CCS processes, and [START_REF] Wu | Interpreting π-calculus with Spin/Promela[END_REF], [START_REF] Song | Verifying π-calculus processes by Promela translation[END_REF] which translate a subset of the πcalculus to the language Promela for model checking in the SPIN tool. Static analysis techniques have also been applied to the π-calculus, including abstract interpretation [START_REF] Venet | Abstract interpretation of the pi-calculus[END_REF] and control flow analysis [START_REF] Bodei | Static analysis for the pi-calculus with applications to security[END_REF].

A number of existing papers have proposed probabilistic extensions of the π-calculus. The first, [START_REF] Herescu | Probabilistic asynchronous π-calculus[END_REF], extended the asynchronous version of the calculus, which removes the output prefix construct, meaning processes must terminate immediately after sending output. A version was then proposed in [START_REF] Chatzikokolakis | A framework to analyze probabilistic protocols and its application to the partial secrets exchange[END_REF], considering only silent probabilistic transitions. This variant, which is essentially the same as the one used in this paper, was introduced to specify and reason about randomised security protocols. In [START_REF] Bhargava | Probabilistic anonymity[END_REF], the probabilistic π-calculus was used to formalise definitions of anonymity.

A stochastic extension of the π-calculus was first considered in [START_REF] Priami | Stochastic π-calculus[END_REF] in which the action prefix construct was replaced with an action-rate prefix construct. A number of different variants have since been proposed differing in how rates are added to the prefix construct. In this paper, we follow [START_REF] Phillips | Efficient, correct simulation of biological processes in the stochastic π-calculus[END_REF] and parameterise silent (τ ) actions with rates and associate a (fixed) rate with each channel. A number of discrete-event simulators for the stochastic π-calculus are available, e.g. BioSpi [START_REF] Priami | Application of a stochastic name passing calculus to representation and simulation of molecular processes[END_REF] and SPiM [START_REF] Phillips | Efficient, correct simulation of biological processes in the stochastic π-calculus[END_REF], but to our knowledge no model checking tools.

Structure:

The remainder of this paper is structured as follows. Section II introduces the syntax and semantics for probabilistic and stochastic extensions of the π-calculus. Sections III and IV describe our extension of MMC for evaluating these semantics and show how the result of this extension can be processed into input for the PRISM tool. Section V presents experimental results and Section VI concludes the paper.

A preliminary version of this paper (with only the discrete probabilistic case) appeared as [START_REF] Norman | Model checking the probabilistic π-calculus[END_REF].

II. THE π-CALCULUS

The π-calculus is a process algebra for modelling concurrency and mobility. Based on value-passing CCS [START_REF] Milner | Communication and Concurrency[END_REF], a key distinguishing feature of the calculus is that it uses a single datatype, names, for both channels and values, with the consequence that it is possible to communicate channel names between processes.

In this section we present the probabilistic and stochastic extensions of the π-calculus for which we have developed automated model checking procedures. In order to facilitate model checking, we make two simple assumptions. Firstly, we restrict our attention to finite-control π-calculus processes, i.e. where recursion is not permitted within parallel composition. This is necessary to ensure that the resulting models are finitestate and is in fact also imposed by the MMC π-calculus model checker, on which our work relies.

Secondly, we require that the systems to which we apply model checking are closed, intuitively meaning that they receive no inputs from their environment and send no outputs to it. This is due to the nature of the properties that are analysed by probabilistic model checkers such as PRISM. We will discuss this issue further in Section IV-F.

Preliminaries: Before describing the probabilistic variants of the π-calculus, we present some preliminary notation and definitions. Throughout the paper we will assume a countable set N of names, ranged over by x, x i , y, etc.

A match is an equality test on names from N and a condition M is a finite conjunction of matches, i.e. M is of the form

[x 1 =y 1 ] ∧ • • • ∧ [x n =y n ].
We denote by n(M ) the set of names that appear in M (ignoring any trivial equality tests of the form [x=x]).

A substitution σ is a partial mapping from N to N . The simplest substitutions are of the form {y/x} which maps x to y. We let n(σ) denote the set of names that the substitution affects, i.e. n(σ

) = {x | ∃y( =x) ∈ N . σ(x)=y} ∪ {x | ∃y( =x) ∈ N . σ(y)=x}. A substitution σ satisfies the match [x=y], denoted σ |= [x=y] if σ(x)=σ(y).
Satisfaction extends to conjunctions of matches in the obvious way, e.g.

σ |= [x 1 =y 1 ] ∧ [x 2 =y 2 ] if σ |= [x 1 =y 1 ] and σ |= [x 2 =y 2 ].
We will use five different action types for the two extensions of the π-calculus: τ (silent action), r(∈ R) (rate action), x(y) (input), xy (output) and x(y) (bound output). The bound names for an action α, denoted bn(α), are defined as follows: bn(τ ) = bn(r) = bn(xy) = ∅ and bn(x(y)) = bn(x(y)) = {y}. A substitution σ can also be applied to an action α, denoted ασ. The definition of this is:

τ σ = τ , rσ = r, (x(y))σ = σ(x)(y) if y ∈ n(σ), (xy)σ = σ(x) σ(y) and (x(y))σ = σ(x)(y) if y ∈ n(σ).
Note that in the case of input and bound output actions (i.e. those with bound variables), the substitution is only defined when the substitution does not change the bound names.

A. The simple probabilistic π-calculus

We use a probabilistic extension of the π-calculus called the simple probabilistic π-calculus or π prob , which adds a discrete probabilistic choice operator to the basic calculus. This choice operator is blind, meaning that probabilities are associated only with silent τ actions, and not input or output actions.

Syntax: We will let P , P i range over terms and α range over actions. Using, as above, x, y, y i to range over names, the syntax of the simple probabilistic π-calculus is: where I is an index set, p i ∈ (0, 1] with i∈I p i = 1 and A is a process identifier. In the following paragraphs, we provide an informal description of the calculus. The next section presents the formal semantics. The inactive process, denoted 0, can perform no actions. The action-prefixed process α.P can perform action α and then evolve into P , where α is one of three types: x(y) inputs a name on x and stores it in y, xy outputs the name y on x; and τ is the silent action representing internal communication.

α ::= τ x(
There are two types of choice: nondeterministic i∈I P i and probabilistic • i∈I p i τ.P i . The former is standard in the πcalculus (and indeed CCS). The latter is the only new operator in this probabilistic extension of the π-calculus. As mentioned above, branches of the probabilistic choice operator are always prefixed with τ actions. The process • i∈I p i τ.P i randomly selects an index i ∈ I with probability p i , performs a τ action and then evolves to process P i . We use p 1 τ.P 1 ⊕ p 2 τ.P 2 to denote the binary form of probabilistic choice.

The parallel composition P 1 | P 2 can either proceed asynchronously or interact through matching input/output actions. The restriction νx P localises the scope of x in process P , i.e.

x can be considered a new and unique name within P . The match construction [x=y]P can evolve as process P only if the match [x=y] is satisfied, i.e. names x and y are identical. Finally, A(y 1 , . . . , y n ) is a recursive call with a corresponding process definition clause of the form A(x 1 , . . . , x n ) P .

An occurrence of name y in process P is bound if it is in a subexpression of P of the form x(y) (input-bound) or νy (νbound); otherwise, it is free. The sets of free and bound names of P are denoted by fn(P ) and bn(P ), respectively, and the set of all names is n(P ). Without loss of generality, we also make the assumption that bound names are all distinct from each other and from free names. This can always be achieved through alpha conversion. A process which contains no free names is said to be closed.

Symbolic semantics:

The operational semantics for probabilistic extensions of the π-calculus are typically expressed in terms of Markov decision processes (MDPs) or, equivalently, probabilistic automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], which allow both probabilistic and nondeterministic behaviour. Existing presentations of the semantics (for example [START_REF] Chatzikokolakis | A framework to analyze probabilistic protocols and its application to the partial secrets exchange[END_REF], which describe a calculus essentially identical to π prob ) are concrete in the sense that the semantic rules directly define the MDP that corresponds to a process term. In this paper, we use a symbolic presentation of the operational semantics [START_REF] Hennessy | Symbolic bisimulations[END_REF]. This approach is in fact quite common for the π-calculus and is particularly beneficial in the context of automatic tool support, as is the case here, or for development of bisimulation theories [START_REF] Hennessy | Symbolic bisimulations[END_REF], [START_REF] Wu | Symbolic bisimulations for probabilistic systems[END_REF].

The main features of the symbolic semantics, which allow one to obtain compact models, are that:

• As in the late semantics of the π-calculus, the input variable of input transitions is kept as a name variable (in contrast to the early semantics, where a different transition is generated for every possible name instance) • Analogously to the match rule, in the communication rule the match between the input and the output channel is represented by a constraint (condition). In principle it is possible to define an early version of the symbolic semantics, but such a version would differ from a concrete semantics only because it would contain the free variables of the initial process (and conditions on them). Therefore, such a version would lack the "raison d'être" of the symbolic semantics: efficiently representing the effects of the run-time communications.

Consider the simple process a(x) . xb . 0 which inputs a name x on channel a and then uses x as a channel on which to output the name b. A concrete approach to the semantics can establish that this process can accept an input on channel a, but its subsequent behaviour (which is dependent on the input x) can only be captured once it is known which other processes it will be composed with. A symbolic approach allows the semantics of a process to include variables (e.g. x) that can be used in actions (e.g. xb). This allows us to adopt a compositional approach: given a parallel composition of several processes, the semantics of each of them can be computed separately in full, and then composed afterwards.

The symbolic semantics of the π prob calculus is expressed in terms of probabilistic symbolic transition graphs (PSTGs). These are a simple probabilistic extension of the symbolic transition graphs of [START_REF] Hennessy | Symbolic bisimulations[END_REF], previously used for the (nonprobabilistic) π-calculus [START_REF] Lin | Symbolic bisimulation and proof systems for the π-calculus[END_REF]- [START_REF] Ingólfsdóttir | A symbolic approach to value-passing processes[END_REF] and for CCS [START_REF] Hennessy | Symbolic bisimulations[END_REF]. Alternatively, they can be seen as a symbolic extension of Markov decision processes.

Let P be a π prob process. The probabilistic symbolic transition graph (PSTG) representing the semantics of the process P is a tuple (S, s init , T prob ) where:

• S is the set of symbolic states, each of which is a term of the simple probabilistic π-calculus; • s init ∈ S, the initial state, is the term P ; • T prob ⊆ S×Cond ×Act×Dist(S) is the probabilistic symbolic transition relation and is the least relation given by the rules in Fig. 1. In the above,

• Cond denotes the set of all conditions (finite conjunctions of matches) over N ; • Act is a set of actions of four basic types: τ , x(y), xy and x(y), where x, y ∈ N ; • Dist(S) is the set of probability distributions over S.

We use the notation Q M,α ---→ {|p i : Q i |} i for the probabilistic symbolic transition (Q, M, α, µ) ∈ T prob where µ(R) = Qi=R p i for any π prob term R. For simplicity we abbreviate the transition Q

M,α ---→ {|1 : Q ′ |} to Q M,α
---→ Q ′ and omit the trivial condition true. We use multi-sets to ensure that processes with duplicate components such as

Q = 1 2 τ.0 ⊕ 1 2 τ.0 have transitions of the form Q τ -→ {| 1 2 : 0, 1 2 : 0|} as opposed to Q τ -→ { 1 2 : 0}.
Of the four action types in Act, the first three are described in the previous section. The fourth, x(y), denotes output of a bound name and is used by the rules OPEN and CLOSE to extend the scope of the bound name y.

A symbolic state Q encodes a set of π prob terms. More specifically, it encodes the set of terms obtained from Q by applying substitutions to its name variables. A substitution σ is applied to a process Q, denoted Qσ, by replacing each action α in Q with ασ. Consider for example the process Q = a(x).xb.0. We have that Q

a(x) ---→ Q ′ where Q ′ = xb.0. The symbolic state Q ′ represents the terms Q ′ {z/x} for any name z. A symbolic transition Q M,α ---→ {|p i : Q i |} i represents
the fact, that under any substitution σ satisfying M , the process term Qσ can perform action ασ and then with probability p i evolve to process Q i σ. This is formally stated in Lemma 1

PRE α.P α -→ {|1 : P |} PROB ( • i p i τ.P i ) τ -→ {|p i : P i |} i SUM P j M,α ---→ {|p j k : P j k |} j k i∈I P i M,α ---→ {|p j k : P j k |} j k j ∈ I PAR P M,α ---→ {|p i : P i |} i P | Q M,α ---→ {|p i : (P i | Q)|} i bn(α) ∩ fn(Q) = ∅ COM P M,y(z) ----→ {|1 : P ′ |} Q N,xv ---→ {|1 : Q ′ |} P | Q [x=y]∧M ∧N,τ ---------→ {|1 : P ′ {v/z} | Q ′ |} RES P M,α ---→ {|p i : P i |} i νx P νxM,α ----→ {|p i : νx P i |} i x ∈ n(α) CLOSE P M,y(z) ----→ {|1 : P ′ |} Q N,x(v) ----→ {|1 : Q ′ |} P | Q [x=y]∧M ∧N,τ ---------→ {|1 : νv(P ′ {v/z} | Q ′ )|} OPEN P M,ȳx ---→ {|1 : P ′ |} νx P νxM,ȳ(x)
------→ {|1 :

P ′ |} x = y MATCH P M,α ---→ {|p i : P i |} i [x=y]P [x=y]∧M,α -------→ {|p i : P i |} i {x, y} ∩ bn(α) = ∅ IDE P {y 1 , . . . , y n /x 1 , . . . , x n } M,α ---→ {|p i : P i |} i A(y 1 , . . . , y n ) M,α ---→ {|p i : P i |} i A(x 1 , . . . , x n ) P νx (true) = true νx [x=x] = true νx [x=y] = false (x =y) νx [y=z] = [y=z] (x =y ∧ x =z) νx (M ∧ N ) = (νx M ) ∧ (νx N )
Fig. 1. The symbolic semantics for πprob, including (inset) application of operator νx to conditions below, which relates the symbolic (PSTG) semantics of π prob , as given in Fig. 1, and the concrete (MDP) semantics, as presented e.g. in [START_REF] Chatzikokolakis | A framework to analyze probabilistic protocols and its application to the partial secrets exchange[END_REF]. This corresponds to Lemma 2.5 in [START_REF] Lin | Complete inference systems for weak bisimulation equivalences in the pi-calculus[END_REF] which discusses symbolic semantics for the (non-probabilistic) π-calculus. In the lemma, σ M indicates that the substitution σ satisfies the condition M of the transition, and the constraint bn(α)∩(fn(P )∪n(σ)) = ∅ corresponds to the fact that bound names are not substituted in order to prevent possible conflicts between bound and free names.

Lemma 1: Let P be a π prob term.

(a) If P M,α ---→ {|p i : P i |} i , then for any substitution σ such that σ M with bn(α) ∩ (fn(P ) ∪ n(σ)) = ∅, P σ ασ --→ {|p i : P i σ|} i . (b) If P σ α -→ {|p i : P ′ i |} i and bn(α) ∩ (fn(P ) ∪ n(σ)) = ∅, then P M,β ---→ {|p i : P i |} i where σ |= M and (β.P i )σ = α.P ′ i .
Proof: Since the symbolic and concrete semantics of π prob share the same types of actions as the (standard) π-calculus, the proof follows the one for Lemma 2.5 in [START_REF] Lin | Complete inference systems for weak bisimulation equivalences in the pi-calculus[END_REF] which is straightforward by transition induction.

B. The stochastic π-calculus

We now describe a stochastic extension of the π-calculus denoted π stoc , the underlying semantics of which is expressed in terms of continuous-time Markov chains (CTMCs). Each transition will thus be labelled with a rate, representing the parameter of an exponential distribution characterising the delay until the associated transition is enabled. More precisely, for rate r, the probability that the transition is enabled within t time-units is given by 1-e -r•t . As in [START_REF] Phillips | Efficient, correct simulation of biological processes in the stochastic π-calculus[END_REF], stochastic behaviour is introduced at the syntactic level by associating a rate with each channel x, denoted rate(x), and by annotating silent τ actions with the rate r at which they occur, i.e. τ r .

Syntax: Using P , P i to range over terms and α to range over actions, the syntax of the stochastic π-calculus is: where r ∈ R >0 , I is an index set and A is a process identifier.

α ::= τ r x(
As in the probabilistic case, the terms 0, P 1 | P 2 , νx P , [x=y]P and A(y 1 , . . . , y n ) denote inactivity, parallel composition, restriction, match and recursive call. The prefix process τ r .P can (internally) evolve to P with rate r. The choice i∈I P i represents a race condition between the transitions of each P i : the first of these transitions to become enabled is the one that is taken. Race conditions also arise from parallel composition (P 1 | P 2 ) between processes. In this case, when two processes synchronise on matching input/output actions on a channel x, the rate of this transition is rate(x).

Symbolic semantics:

The operational semantics for the stochastic π-calculus is in terms of CTMCs. Usually (as in e.g. [START_REF] Phillips | Efficient, correct simulation of biological processes in the stochastic π-calculus[END_REF], on which our syntax is based), a concrete semantics is presented which maps each process term directly to the CTMC it represents. However, as for the probabilistic case (see the discussion in the previous section), in order to adopt a compositional approach we employ a symbolic semantics based on an extension of symbolic transition graphs [START_REF] Hennessy | Symbolic bisimulations[END_REF].

Let P be a π stoc process. The stochastic symbolic transition graph (SSTG) representing the semantics for the process P is a tuple (S, s init , T stoc ) where:

• S is the set of symbolic states, each of which is a term of the stochastic π-calculus;

PRE τ τ r .P r -→ P PRE IN x(y).P x(y) ---→ P PRE OUT xy.P xy -→ P SUM P j M,α ---→ P ′ j i∈I P i M,α ---→ P ′ j j ∈ I PAR P M,α ---→ P ′ P | Q M,α ---→ P | Q bn(α) ∩ fn(Q) = ∅ COM P M,y(z) ----→ P ′ Q N,xv ---→ Q ′ P | Q [x=y]∧M ∧N,rate(x) -------------→ P ′ {v/z} | Q ′ RES P M,α ---→ P ′ νx P νxM,α ----→ P ′ x ∈ n(α) CLOSE P M,y(z) ----→ P ′ Q N,x(v) ----→ Q ′ P | Q [x=y]∧M ∧N,rate(x) -------------→ νv(P ′ {v/z} | Q ′ ) OPEN P M,ȳx ---→ P ′ νx P νxM,ȳ(x) ------→ P ′ x = y MATCH P M,α ---→ P ′ [x=y]P [x=y]∧M,α -------→ P ′ {x, y} ∩ bn(α) = ∅ IDE P {y 1 , . . . , y n /x 1 , . . . , x n } M,α ---→ P ′ A(y 1 , . . . , y n ) M,α ---→ P ′ A(x 1 , . . . , x n ) P νx (true) = true νx [x=x] = true νx [x=y] = false (x =y) νx [y=z] = [y=z] (x =y ∧ x =z) νx (M ∧ N ) = (νx M ) ∧ (νx N ) Fig. 2.
The symbolic semantics for πstoc, including (inset) application of operator νx to conditions

• s init ∈ S, the initial state, is the term P ; • T stoc ⊆ S×Cond ×Act×S is the stochastic symbolic transition multi-relation and is the least multi-relation given by the rules in Fig. 2. In the above,

• Cond denotes the set of all conditions (finite conjunctions of matches) over N ; • Act is a set of actions of four basic types: r, x(y), xy and x(y), where r ∈ R >0 and x, y ∈ N . The fact that we have used a multi-relation is standard for stochastic process algebras [START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF] and ensures that multiple transitions are generated for expressions with identical components, such as τ r .P + τ r .P . This requirement is because the choice operator is interpreted as a race condition: the first transition to become enabled is the one that is taken. More precisely, since the minimum of two exponential distributions with rates r 1 and r 2 is an exponential distribution whose rate is the sum r 1 +r 2 , the behaviour of the process τ r .P + τ r .P should be the same as that of τ 2r .P . This is captured in the semantics by the inclusion of two separate transitions labelled r in the multi-relation T stoc .

Analogously to the case for PSTGs, discussed in the previous section, a stochastic symbolic transition Q M,α ---→ Q ′ of an SSTG represents the fact that, under any substitution σ satisfying M , the process term Qσ can perform action ασ and then evolve to process Q ′ σ. This is formally stated in Lemma 2 below, which relates the symbolic (SSTG) semantics of π stoc , as given in Fig. 2, and the concrete (CTMC) semantics, as found in [START_REF] Phillips | Efficient, correct simulation of biological processes in the stochastic π-calculus[END_REF]. Again, this corresponds to Lemma 2.5 in [START_REF] Lin | Complete inference systems for weak bisimulation equivalences in the pi-calculus[END_REF] for the standard (non-probabilistic) π-calculus. ---→ P ′ , then for any substitution σ such that σ M with bn(α)

∩ (fn(P ) ∪ n(σ)) = ∅, P σ ασ --→ P ′ σ. (b) If P σ α -→ Q ′ and bn(α) ∩ (fn(P ) ∪ n(σ)) = ∅, then P M,β ---→ Q where σ |= M and (β.Q)σ = α.Q ′ .
Proof: Straightforward by transition induction. The details are almost identical in structure to Lemma 2.5 of [START_REF] Lin | Complete inference systems for weak bisimulation equivalences in the pi-calculus[END_REF] except that the action τ in the π-calculus is replaced by numerical rates r in π stoc , which do not influence names.

Strictly speaking, the concrete semantics used above do not correspond precisely to the usual definition of a CTMC, since transitions can be associated with either rates (for τ actions) or inputs/output actions (which have yet to be matched). Furthermore, multiple transitions can occur between the same pair of states (due to the use of a multi-relation in the definition of an SSTG). In the semantics of a closed π stoc process, however, only rate-labelled transitions remain and multiple transitions between states are simply summed.

III. GENERATING PSTGS AND SSTGS USING MMC

In this section we describe the automatic generation of the symbolic transition graph for an arbitrary process expressed in either the simple probabilistic π-calculus or stochastic πcalculus. This is achieved with an extension of the (nonprobabilistic) π-calculus model checker MMC [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF], which from this point on we refer to as MMC prob . In the next section we will build upon this, presenting a more efficient, compositional scheme for processes of a specific structure.

MMC prob is based on only a subset of MMC's functionality: essentially the capability to construct the full set of reachable states of a π-calculus process. The restrictions placed on the syntax of the calculus by MMC are the same as we impose in Section II.

MMC works by (and derives its efficiency from) exploiting the similarity between the way in which resolution-based Fig. 3. XSB code for the trans predicate encoding the πprob symbolic semantics logic programming techniques handle variables and the way in which the symbolic semantics of the π-calculus handles names [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF]. It is implemented in the logic programming system XSB, which is a dialect of Prolog. π-calculus names are represented by XSB variables. MMC then uses a direct encoding of the symbolic semantics of the calculus into XSB rules, based on the definition of a predicate called This approach has several benefits: firstly it gives a clear and intuitive implementation; secondly, and more importantly, this encoding is provably correct [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF].

Our implementation is a direct extension of this approach. We have a straightforward encoding of the syntax of both π prob and π stoc into the language of XSB, with names and process identifiers represented by XSB variables and constants, respectively. We then adapt MMC's predicate trans to represent the symbolic semantics of each calculus. We first describe the case for the simple probabilistic π-calculus and then discuss the differences in the stochastic case.

The probabilistic case: We begin with the encoding of the syntax of π prob into the language of XSB. Letting X, Y, Y i range over variables, P range over processes and denoting commadelimited lists of processes as -→ P , the syntax of π prob in the input language of MMC prob is given by the following BNF grammar: where Ā is the lower case form of process identifier A, with the definition clause of the form def( Ā(X 1 , . . . , X n ), P).

Assuming that ρ is a one-to-one function mapping XSB variables to π prob names, the following function f ρ relates the MMC prob representation of the key components of π prob (conditions, actions and processes) into their corresponding π prob notation:

Conditions: fρ(true) = true fρ(X = Y) = [ρ(X) = ρ(Y)] fρ((M, N)) = fρ(M) ∧ fρ(N)
Actions:

fρ(tau) = τ fρ(in(X, Y)) = ρ(X)(ρ(Y)) fρ(out(X, Y)) = ρ(X)ρ(Y) fρ(out bound(X, Y)) = ρ(X)(ρ(Y))
Processes: fρ(zero) = 0 fρ(pref(act, P)) = fρ(act).fρ(P) fρ(choice( -→ P )) = P n i=1 fρ(Pi) fρ(prob choice( -----------→ pref(tau(p), P))) = P n i=1 piτ.fρ(Pi) fρ(par(P1, P2)) = fρ(P1)|fρ(P2) fρ(nu(X, P)) = νρ(X)fρ(P) fρ(match((X = Y), P)) = [ρ(X) = ρ(Y )]fρ(P) fρ(proc( Ā(Y1, . . . , Yn))) = A(ρ(Y1), . . . , ρ(Yn))

where

- → P ≡ [P1, . . . , Pn] -----------→ pref(tau(p), P) ≡ [pref(tau(p1), P1), . . . , pref(tau(pn), Pn)]
and A is defined with A(ρ(X 1 . . . , ρ(X n )) f ρ (P).

Using the function f ρ we can now define the XSB predicate trans, which represents the direct encoding of the symbolic semantics of π prob (see Fig. 1) into XSB. A tuple trans(P, PSteps, M), where PSteps is a list of compound structures psteps(p i , act, P i ), represents a symbolic probabilistic transition:

f ρ (P) fρ(M),fρ(act) --------→ {p : f ρ (P i )} i
The definition of trans is shown in Fig. 3. The predicates prob branch, set par steps and set nu steps are defined to construct the list PSteps according to the operational semantics rules PROB, PAR and RES. Other auxiliary predicates used in Fig. 3 are given in Fig. 4. Note the close correspondence between the definitions in Fig. 3 and the rules of the symbolic semantics in Fig. 1.

The soundness and completeness of the encoding can be established by induction on the length of derivations of a query answer of trans and a symbolic transition in π prob , respectively. The proof details are similar to Theorems 2 and 3 in [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF].

Finally, we add an extra XSB predicate stg(P), which uses query-evaluation on trans to derive the PSTG of process P and output it in a simple textual format. This is done through a depth-first traversal of the graph, followed by an enumeration of all its symbolic states and transitions. The XSB code for this can be found in [START_REF] Norman | Translating the probabilistic π-calculus to PRISM[END_REF].

Example: Consider the simple π prob process T oss:

T oss(x) x(y). pτ.ȳhead.0 ⊕ (1p)τ.ȳtail.0 which receives a name y on channel x and then sends out, on channel y, either head or tail, with probability p or 1-p, respectively. Fig. 5 shows the application of MMC prob to the process T oss. The first four lines illustrate the encoding of the π prob syntax into XSB. Below that is the output of the tool, i.e. the application of the rule stg. Lines starting #i show the π prob term for the ith state, lines starting * j and ′ k enumerate transitions and the individual edges of transitions, respectively. All bound names are given unique names (e.g. h417) and displayed on lines beginning >. All free names used are listed at the end, plus other statistics for the PSTG. The stochastic case: The generation of the SSTG for a π stoc process proceeds in almost identical fashion. Since the calculus has no probabilistic choice operator, the list PSteps in the representation trans(P, PSteps, M) of each symbolic transition contains only a single item of the form pstep(r i , act, P i ), where r i now represents a real-valued rate, instead of a probability.

The encoding of a rate-labelled prefix process τ r .P is treated as a special case of the probabilistic choice operator for π prob with a singleton operand. Input and output actions over a channel x are given dummy rates of 1 which will be replaced with the channel rate rate(x) subsequently. Since MMC prob simply enumerates all matching transitions when evaluating the symbolic semantics (and does not remove any duplicates), no special treatment is required to deal with the multi-relation in the definition of SSTGs.

IV. TRANSLATING PSTGS AND SSTGS INTO PRISM

We use the probabilistic model checker PRISM (which supports both MDPs and CTMCs) to perform analysis of the semantic models derived from π prob or π stoc processes. The scheme described in the previous section can be used to translate an arbitrary process described in either the simple probabilistic π-calculus or stochastic π-calculus into the probabilistic or stochastic symbolic transition graph representing its semantics. We apply model checking to closed processes (this issue is discussed further in Section IV-F), for which the symbolic (PSTG or SSTG) semantics and concrete (MDP or CTMC) semantics coincide. The list of states and transitions produced by MMC prob , as illustrated by the example in Fig. 5, can hence easily be imported directly into PRISM for analysis.

However, for processes of a specific structure, we instead propose to adopt a compositional translation, using the highlevel modelling language supported by PRISM. This results in a much more efficient translation procedure. More specifically, we consider the case where systems are of the form P = νx 1 . . . νx k (P 1 | • • • | P n ) and each P i contains no instances of the ν operator (including inside recursive definitions). The basic idea is to generate the symbolic transition graph for subprocess P i (as described in the previous section), map each individual symbolic transition graph to a PRISM module (a component of a PRISM language model), and then use PRISM to construct the semantics of P through the parallel composition of these modules. Note that the compositional nature of this approach is reliant on our use of symbolic semantics. Without this, we would not be able to generate the full semantics of P i in isolation.

The overall process structure we impose (a parallel composition of a set of processes, optionally enclosed inside a restriction of one or more names) is actually fairly typical: systems are generally modelled as a parallel composition of multiple components and, since we assume that P is closed, it is likely that free names used as channels between processes will be restricted in this way. Furthermore, in most cases a process can be rearranged to a structurally congruent process which is of the correct form, by pushing ν operators to the outside. We have, for example, that P 1 | νx P 2 and νx (P 1 | P 2 ) are structurally congruent under the assumption that x does not occur in P 1 . The only class of processes which cannot be renamed in this way are those that include ν inside recursive definitions. In this case, the process can in principle generate an infinite number of new names. This can be resolved in the context of a parallel composition with other processes, and therefore in such a case we can resort to the basic approach: use MMC prob to construct the symbolic transition graph for the full system and import this directly into PRISM.

There are two principal challenges regarding the translation of symbolic transition graphs into PRISM: (1) mapping the name datatype into PRISM's basic type system; and (2) mapping binary (CCS-style) communication of names over channels to PRISM's multi-way (CSP-style) synchronisation without value passing. In brief, (1) is handled by enumerating the set of all free names, assigning each an (identically named) integer constant to represent it, and ( 2) is handled by introduc-ing an action label for each required combination of process sender/receiver pair, channel and name. Communication of names between processes is handled by including in each receiver process with a bound input variable x, an identically named local (integer) variable which will be used to store the name assigned to x.

Before discussing the details of this compositional translation, we give both an overview of the PRISM syntax and semantics and a simple example which illustrates the key aspects of the translation.

A. PRISM semantics

A PRISM model comprises a set of n modules, the state of each being given by a set of finite-ranging local variables. The global state of the model is determined by the union of all local variables, which we denote V . The behaviour of each module is defined by a set of guarded commands. When modelling MDPs, these commands take the form:

[act] guard → p 1 : u 1 + • • • + p m : u m ;
where act is an (optional) action label, guard is a predicate over V , p i ∈ (0, 1] and u i are updates of the form:

(x ′ 1 =u i,1 ) & . . . & (x ′ k =u i,k
) where u i,j is a function over V . Intuitively, in global state s of the PRISM model, the command is enabled if s satisfies guard . If a command is executed, the module will, with probability p i update its local variables according to the update u i , by setting the value of each local variable x j to u i,j (s).

When modelling CTMCs, commands are of the form:

[act] guard → r : u;

where act is an (optional) action label, guard is a predicate over V , r ∈ R >0 and u is an update (of the form shown above). In this case, when the guard is satisfied, there is a transition with rate r that updates the local variables according to u. When multiple commands with the same update are enabled, the corresponding transitions are combined into a single transition whose rate is the sum of the individual rates.

In practice (see for example Fig. 6), we omit probabilities (or rates) equal to one and elements of updates that are of the form (x ′ =x). The semantics of the whole PRISM model is the parallel composition of all modules using the standard CSP parallel composition [START_REF] Roscoe | The theory and practice of concurrency[END_REF] (i.e. modules synchronise over all their common actions). For transitions arising from synchronisation between multiple processes, the associated probability or rate is obtained by multiplying those of each component transition. See [START_REF]Online PRISM documentation[END_REF] for the full semantics of the PRISM language.

B. Example Translation

Consider the following parallel composition of two processes expressed in the simple probabilistic π-calculus:

• Q νa (Q 1 | Q 2 ) • Q 1 νc νd 1 2 τ.āc.c(v).0 ⊕ 1 2 τ.ād.d(w).0 • Q 2 νb a(x). bx.0 | b(y).ȳe.0 1.
const int a = 1; const int b = 2; const int c = 3; 2.

const int d = 4; const int e = 5; 3.

module P1 4.

s1 : [1..6] init 1; 5.

v : [0..5] init 0; 6.

w : [0..5] init 0; 7.

[] (s1 = 1) → 0.5 : (s ′ 1 = 2) + 0.5 : (s ′ 1 = 3); 8.

[a P1 P2 c] (s1 = 2) → (s ′ 1 = 4); 9.

[a P1 P2 d] (s1 = 3) → (s ′ 1 = 5); 10.

[c P3 P1 e] (s1 = 4) → (s

′ 1 = 6); & (v ′ = e) 11.
[d P3 P1 e] (s1 = 5) → (s ′ 1 = 6); & (w ′ = e) 12. endmodule 13.

module P2 14.

s2 : [1..3] init 1 15.

x : [0..5] init 0; 16.

[a

P1 P2 c] (s2 = 1) → (s ′ 2 = 2) & (x ′ = c); 17. [a P1 P2 d] (s2 = 1) → (s ′ 2 = 2) & (x ′ = d); 18. [b P2 P3 x ] (s2 = 2) → (s ′ 2 = 3); 19. endmodule 20. module P3 21. s3 : [1..2] init 1 22. y : [0..5] init 0; 23. [b P2 P3 x ] (s3 = 1) → (s ′ 3 = 2) & (y ′ = x ); 24. [c P3 P1 e] (s3 = 2) & (y = c) → (s ′ 3 = 3); 25. [d P3 P1 e] (s3 = 2) & (y = d) → (s ′ 3 = 3); 26.
endmodule Noting that c and d do not occur in Q 2 and that b does not occur in Q 1 , we can rewrite Q as the structurally congruent process P , defined as follows:

• P νa νb νc νd (P 1 | P 2 | P 3 ) • P 1 1 2 τ.āc.c(v).0 ⊕ 1 2 τ.ād.d(w).0 • P 2 a(x). bx.0 • P 3 b(y).ȳe.0 and the corresponding PSTGs are given by:

• P 1 : Q 1 1 τ -→ {| 1 2 :Q 1 2 , 1 2 :Q 1 3 |}, Q 1 2 āc -→ Q 1 4 c(v) --→ Q 1 6 and Q 1 3 ād -→ Q 1 5 d(w) ---→ Q 1 6 • P 2 : Q 2 1 a(x) ---→ Q 2 2 bx -→ Q 2 3 • P 3 : Q 3 1 b(y) --→ Q 3 2 ȳe -→ Q 3 3
In the above, we omit probabilities that are 1 and conditions true. The PSTGs for P 1 , P 2 and P 3 have the sets of bound names {v, w}, {x} and {y}, respectively, and the combined set of free names is {a, b, c, d, e}. The resulting PRISM model is shown in Fig. 6. This example will be referred to in the full explanation of the translation given below.

C. Formal translation

We assume that the set of all names in the system is N , which is partitioned into disjoint subsets: N fn , the set of all free names appearing in processes P 1 , . . . , P n , and N bn 1 , . . . , N bn n , the sets of input-bound names for processes P 1 , . . . , P n .

For clarity, we will retain wherever possible identical notation between the π-calculus terms and the resulting PRISM language description. Thus, each of the n subprocesses (or symbolic transition graphs) P i becomes a PRISM module P i and the (finite) set of terms If the value of variable x i j is equal to one of the these constants, then the corresponding bound name has been assigned the appropriate free name (by an input action). If x i j =0, no input to the bound name has occurred yet.

S i = {Q i 1 , . . . , Q i ki }
In this way, the conditions which label transitions of the symbolic transition graph can be translated directly into PRISM. For example, if condition M equals In addition, when translating stochastic π-calculus processes, for each free name x we add to the PRISM description a constant rate x whose value is equal to rate(x), i.e. the rate associated with the channel x.

For each transition in the symbolic transition graph for P i , we will include a set of corresponding PRISM commands in the module P i . We consider each type of transition separately below. Note that, if P i is a simple probabilistic π-calculus term, then from the semantics (see Fig. 1) the only transitions which can include multiple probabilistic choices are internal, therefore the remaining types of transitions (input and output) can be written in the simplified form

Q i M,α ---→ R i .
For the stochastic case, since PRISM multiplies the rates of synchronising transitions and synchronisation in the π-calculus is always binary, we associate rates (e.g. rate x for channel x) with the "output" transitions and set the rates for "input" transitions to 1 (which is the default so can be omitted). Case 2 (stochastic internal transition). For a transition:

Case 1 (probabilistic internal transition). For a transition:

Q i M,τ ---→ {|p 1 : R i 1 , . . . , p m : R i m |} we add the command: [] (s i =Q i ) & M → p 1 :(s ′ i =R i 1 ) + • • • + p m :(s ′ i =R i m ); See
Q i M,r --→ R i we add the command: [] (s i =Q i ) & M → r : (s ′ i =R i );
Case 3 (output on free name). For a transition:

Q i M,xy ---→ R i where x ∈ N fn
when translating simple probabilistic π-calculus processes we add, for each j ∈ {1, ..., n}\{i}, the command:

[x P i P j y] (s i =Q i ) & M → (s ′ i =R i )
; while for stochastic π-calculus processes we add, for each j ∈ {1, ..., n}\{i}:

[x P i P j y] (s i =Q i ) & M → rate x : (s ′ i =R i );
The channel x, sender P i , receiver P j and sent name y are all encoded in the action label. See Fig. 6 lines 8 and 18 for examples of sending free and bound names y, respectively.

Case 4 (output on bound name). For a transition:

Q i M,xy ---→ R i where x ∈ N bn i
in the probabilistic case we add, for each a ∈ N fn and j ∈ {1, ..., n}\{i}:

[a P i P j y] (s i =Q i ) & M & (x=a) → (s ′ i =R i );
while, in the stochastic case, for each a ∈ N fn and j ∈ {1, ..., n}\{i} the command:

[a P i P j y] (s i =Q i ) & M & (x=a) → rate a : (s ′ i =R i );
is added. This is similar to Case 3 except that we include a command for each possible value a of x. See for example lines 24 and 25 of Fig. 6.

Case 5 (input on free name). For a transition:

Q i M,x (z)
----→ R i where x ∈ N fn in both cases we add, for each y ∈ N \N bn i and j ∈ {1, ..., n}\{i}, the command:

[x P j P i y] (s i =Q i ) & M → (s ′ i =R i ) & (z ′ =y);
For input actions, we add a line for each possible received name y. The assignment (z ′ =y) models the update of the bound name z to y. See for example lines 16 and 17 of Fig. 6 which match the output commands from lines 8 and 9. Notice that this translation also works in the case where y is a bound name in another process P j (see for example line 23 of Fig. 6).

Case 6 (input on bound name). For a transition:

Q i M,x(z)
----→ R i where x ∈ N bn i when translating both simple probabilistic and stochastic processes, we add for each a ∈ N fn , y ∈ N \N bn i and j ∈ {1, ..., n}\{i} the command:

[a P j P i y] (s i =Q i ) & M & (x=a) → (s ′ i =R i ) & (z ′ =y);
This case combines elements of Cases 4 and 5: we add a command for each possible pairing of channel a that x may represent and name y that may be received.

Finally, we need to remove some spurious commands added in Cases 5 and 6, since they correspond to input actions which will never occur. More precisely, for each module P j we identify labels x P i P j y which appear on a command of P j but which do not appear in any of the commands in module P i . Commands with such action labels are removed from P j .

For example, in Fig. 6 since process P 1 only outputs c or d on channel a, there is no label of the form a P 1 P 2 e in module P 1 , and therefore commands with this label have been removed from module P 2 .

D. Correctness of the translation

By assumption, the term being translated is finite control, is closed and of the form

P = νx 1 . . . νx k (P 1 | • • • | P n ).
The first step in the proof is to show that any term in the derivation tree of P is of the form νx

1 . . . νx k (Q 1 σ 1 | • • • | Q n σ n )
where, for any 1≤j≤n, Q j is a state of the symbolic transition graph for the process P j and σ j is a substitution from the bound names of P j to the free names of P 1 , . . . , P n . The proof is by induction on the (concrete) transition rules using Lemma 1 or Lemma 2, depending on whether we are considering π prob or π stoc .

Using this result, we now show that the translation is correct by constructing a mapping between these terms and the states of the PRISM model and demonstrating that, for any term in the derivation tree of P , there is a transition in the (concrete) semantics if and only if the corresponding PRISM state has a matching transition. For any term νx

1 . . . νx k (Q 1 σ 1 | • • • | Q n σ n ) the state
in the PRISM model is constructed as follows: for any 1 ≤ j ≤ n, the values of the variables of module P j are given by s j =Q j , x j 1 =i j 1 , . . . , x j kj =i j kj where if σ(x j l )=z ∈ N fn , then i j l is the integer constant corresponding to the free variable z and otherwise (i.e. σ(x j l )=x j l ) i j l equals 0. The remainder of the proof is dependent on whether we are in the probabilistic or stochastic setting.

1) Probabilistic case: Consider any π prob term Q in the derivation tree, where

Q = νx 1 . . . νx k (Q 1 σ 1 | • • • | Q n σ n ) and the transition Q τ -→ {|p m : R m |} m .
From the transition rules and the conditions we have imposed on the structure of π prob terms, there are the following two cases to consider.

Internal transition. Q j σ j τ -→ {|p m : R j ′ m |} m and R m = νx 1 . . . νx k (Q 1 σ 1 | • • • | R j ′ m | • • • | Q n σ n ). From Lemma 1(b), we have Q j Mj ,τ ---→ {|p m : R j m |} where σ j |= M j and R j m σ j = R j ′ m .
Hence, by construction in the module P j there is a command of the form:

[] (s j =Q j ) & M j → p 1 :(s ′ j =R j 1 ) + • • • + p m :(s ′ j =R j m )
; Finally, since σ j |= M j and by definition of the mapping between π prob terms and PRISM, it follows that the PRISM state corresponding to Q satisfies the guard (s j =Q j ) & M j and that the transition is preserved in the translation.

Communication. Q j σ j x(z) ---→ R ′ j , Q l σ l xy -→ R ′ l , j = l, and {|p m : R m |} m = {|1 : R|} where R = νx 1 . . . νx k (Q 1 σ 1 | • • • | R ′ j {y/z} | • • • | R ′ l | • • • | Q n σ n ).
From Lemma 2(b), assuming without loss of generality that z is fresh:

• Q j Mj ,xj (zj )
------→ R j where σ j |=M j and (x j (z j ).R j )σ j = x(z).R ′ j ;

• Q l M l ,x l y l -----→ R l where σ l |=M l and (x l y l .R l )σ l = xy.R ′ l .
Now, since z is fresh, it follows that z=z j and, because σ l is a substitution from bound to free names of P 1 , . . . , P n , it follows that y ∈ N \N bn j . In addition, since σ j is a substitution from bound to free names, either x j is free and equals x, and hence in module P j we have the command:

[x P l P j y] (s j =Q j ) & M j → (s ′ j =R j ) & (z ′ j =y)
; or x j is bound and, since x j σ j = x, it follows that x is free, and therefore the command:

[x P l P j y] (s j =Q j ) & M j & (x j =x) → (s ′ j =R j ) & (z ′ j
=y); appears in module P j . Employing similar arguments, if x l is free, then x l = x and the command:

[x P l P j y] (s l =Q l ) & M l → (s ′ l =R l )
; appears in module P l . While, if x l is bound, then module P l includes the command:

[x P l P j y] (s l =Q l ) & M l & (x l =x) → (s ′ l =R l ); Since σ j |= M j , σ l |= M l , x j σ j = x and x l σ l = x, it follows that the guards (s j =Q j ) & M j , (s j =Q j ) & M j & (x j =x), (s l =Q l ) & M l and (s l =Q l ) & M l & (x l =x)
hold in the PRISM state encoding Q. Finally, since the encoding of R ′ j {y/z} can be obtained from the encoding of R j σ j by setting the variable z to value y, it follows that the transition is preserved by the translation.

To complete the proof it remains to show that for any transition of the PRISM model there is a matching transition in the corresponding π prob term. The result follows in a similar manner to the above using Lemma 1(a) instead of Lemma 1(b).

2) Stochastic case: Consider any π stoc term Q in the derivation tree, where

Q = νx 1 . . . νx k (Q 1 σ 1 | • • • | Q n σ n ) and the transition Q r -→ νx 1 . . . νx k R.
From the transition rules and the conditions we have imposed on the structure of π stoc terms, there are the following two cases to consider.

transition. Q j σ j r -→ R ′ j and R = Q 1 σ 1 | • • • | R ′ j | • • • | Q n σ n . From Lemma 2(b), we have Q j Mj ,r
---→ R j where σ j |= M j and R j σ j = R ′ j . Hence, by construction in the module P j there is a command of the form:

[] (s j =Q j ) & M j → r : (s ′ j =R j ); Finally, since σ j |= M j and by definition of the mapping between π stoc terms and PRISM, it follows that the PRISM state corresponding to Q satisfies the guard (s j =Q j ) & M j and that the transition is preserved in the translation.

Communication. Q j σ j x(z) ---→ R ′ j , Q l σ l xy -→ R ′ l , j = l, R = Q 1 σ 1 | • • • | R ′ j {y/z} | • • • | R ′ l | • • • | Q n σ n
and rate(x) = r. From Lemma 2(b), assuming without loss of generality that z is fresh:

• Q j Mj ,xj (zj )
------→ R j where σ j |=M j and (x j (z j ).R j )σ j = x(z).R ′ j ;

• Q l M l ,x l y l -----→ R l where σ l |=M l and (x l y l .R l )σ l = xy.R ′ l .
We employ the same arguments used in the probabilistic case. If x j is free, module P j contains the command:

[x P l P j y] (s j =Q j ) & M j → (s ′ j =R j ) & (z ′ j =y);
while if x j is bound, it contains the command:

[x P l P j y] (s j =Q j ) & M j & (x j =x) → (s ′ j =R j ) & (z ′ j =y);
Similarly, if x l is free, the command:

[x P l P j y] (s l =Q l ) & M l → rate x : (s ′ l =R l );
appears in module P l and, if x l is bound, then the command:

[x P l P j y] (s l =Q l ) & M l & (x l =x) → rate x : (s ′ l =R l );
appears in module P l . The remaining arguments are the same as in the probabilistic case, using additionally the fact that the PRISM constant rate x has been given the value rate(x).

E. Optimisations

The translation from symbolic transition graphs to PRISM code described in this section can be optimised to reduce the size of the generated code and the resulting model. The basic idea is to compute an over-approximation of the possible values that each symbolic transition graph's bound name can take and, thus, the channels it can send out on and the values that can be sent on those channels. With this information, we can decrease the range of the PRISM local variables corresponding to each bound name and remove unnecessary commands corresponding to combinations of channel, value and processes that can never occur. The over-approximation is computed iteratively, starting with an empty set of possible values for each bound name, and at each step adding any name that can be received upon any channel that can be used to assign to the bound name. The iterations required is bounded by the number of processes n. For clarity of presentation, the example in Fig. 6 has in fact been optimised in this way. This optimisation could be improved by employing more complex techniques based on those developed in [START_REF] Bodei | Static analysis for the pi-calculus with applications to security[END_REF] which use control flow analysis to establish an over-approximation of the set of channels a name may be bound to and the set of names that may be sent along a given channel.

F. Properties

For probabilistic model checking of MDPs and CTMCs, properties are typically specified using the temporal logics PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF], [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF] and CSL [START_REF] Aziz | Verifying continuous time Markov chains[END_REF], [START_REF] Baier | Model-checking algorithms for continuous-time Markov chains[END_REF], the key components of which are timed and untimed probabilistic reachability. Examples of expressible properties include the maximum probability of a failure occurring (P max=? [F failure]), the minimum probability of a process successfully completing (P min=? [F success]), the probability that a message is delivered by time t(∈ R) (P =? [F ≤t delivered ]) and the probability of a reaction occurring in the time interval [t 1 , t 2 ](⊆ R) (P =? [F [t1,t2] reaction]). In practice, a wide range of useful properties can be expressed in this way.

Most probabilistic model checking tools, including PRISM, use state-based property specifications, i.e. the atomic propositions (failure, delivered , etc.) in the examples above are quantifier-free predicates identifying a set of states in the model. Also, the models that are checked are closed: there are no inputs/outputs between the model and its environment, only between components included within the model. This is our reason for only performing probabilistic model checking on closed π-calculus processes.

In terms of the translation from π-calculus description to PRISM model, we simply need to be able to identify the particular set of target states specified in the reachability property. This is done through the MMC prob translator when it constructs a PSTG or SSTG: either by identifying which symbolic states correspond to a particular process term; or those in which a particular action is available (in the latter case, such actions can be added purely for the purposes of identifying states, and then removed through restriction).

For example, consider a distributed randomised algorithm executed between n parallel components, P 1 , . . . , P n . A typical property to be checked is that algorithm always terminates with probability 1 (for any possible scheduling of the n components). In this case, we would identify the term in the π-calculus description of each process P i that corresponds to that process finishing its execution of the algorithm. From the output of the MMC prob translator, we can identify the corresponding local state Q i of the process. We would then compute (in PRISM) the (minimum probability) of reaching the state s

1 = Q 1 ∧ • • • ∧ s n = Q n .
Although not considered in the case studies used in this paper, our implementation could also be extended to allow for the computation of cost-or reward-based properties, which are also supported by PRISM. This allows expression of properties such as the "maximum expected number of messages sent before termination" or "the minimum expected power consumption within t time units". Typically the cost/reward information needed for these properties is added to the model (MDP or CTMC) by annotating either transitions labelled with particular actions (for example the action-label which corresponds to a message being sent between two components) or states with real values. Since our translation of the probabilistic or stochastic π-calculus to PRISM preserves both information about the state and channel communications of a process, information of this kind could be incorporated into the translation in a relatively straightforward fashion.

More general temporal properties, for example that a certain sequence of actions is performed, could be encoded through the addition of a test/watchdog process [START_REF] Goldsmith | Watchdog transformations for property-oriented model-checking[END_REF]. Model checking for specification formalisms more specifically tailored to the mobile aspects of the π-calculus, such as spatial logic [START_REF] Caires | A spatial logic for concurrency (part i)[END_REF], will be an area of future work.

V. IMPLEMENTATION AND RESULTS

Our implementation of model checking for the simple probabilistic π-calculus and stochastic π-calculus is fully automated and comprises three parts: (1) MMC prob , an extension of MMC (as described in Section III), which constructs the sym-bolic transition graphs for a simple probabilistic or stochastic π-calculus process, (2) the translator from the symbolic transition graph to PRISM code (as described in Section IV), implemented in Java, and (3) the probabilistic model checker PRISM [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF] which builds the MDP/CTMC from part (2) and performs verification of PCTL/CSL properties. We based our implementation on MMC 1.0 and PRISM 3.1.1.

Firstly, we consider the dining cryptographers protocol (DCP) [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], Chaum's randomised solution to the classic anonymity problem in which a group of N parties collectively establish whether either one of the group or an independent party has to make a payment. If the former, this is achieved without any of the N -1 non-paying parties knowing the identity of the paying one. This was previously modelled in the probabilistic π-calculus in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. To check anonymity, we compute the probability of reaching each of the possible outcomes of the protocol (from the point of view of an individual party) and establish that they are identical.

Secondly, we study the partial secret exchange (PSE) algorithm of [START_REF] Even | A randomized protocol for signing contracts[END_REF] for anonymous contract signing between two parties. A probabilistic π-calculus model of PSE was given in [START_REF] Chatzikokolakis | A framework to analyze probabilistic protocols and its application to the partial secrets exchange[END_REF]. The protocol was independently analysed in PRISM [START_REF] Norman | Analysis of probabilistic contract signing[END_REF], where a potential flaw of the protocol was identified, in that one party always has an advantage over the other. Several modifications to the protocol were proposed and shown to have a lower probability of this occurring. We used a π prob model of both the original and a modified version to demonstrate the same flaw.

Thirdly, we constructed both a probabilistic and stochastic model of a mobile communication network (MCN), based on the (non-probabilistic) π-calculus model in [START_REF] Orava | An algebraic verification of a mobile network[END_REF]. The system comprises N base stations with fixed communication links to a mobile switching centre and a mobile station which can be connected to each of the base stations via radio links. The mobile station roams between the base stations. When it changes base station, the mobile communication network acts as an intermediate party, controlling the handover protocol and exchange of communication links between stations. This case study was analysed using MMC in [START_REF] Yang | A logic encoding of the π-calculus: model checking mobile processes using tabled resolution[END_REF]. In both this and the original paper, though, the occurrence of a failure during the handover protocol was modelled as a nondeterministic choice. In the probabilistic version we are able to correctly model this as a random event. For the stochastic model, we used the adapted version of [START_REF] Priami | Stochastic analysis of mobile telephony networks[END_REF]. This allows both correct modelling of the failure event and also timing characteristics of the network. We check the probability of a handover operation completing successfully, within a given number of communications (for the probabilistic case) or within a fixed time deadline (for the stochastic case).

Our final case study is a CTMC model of the Fibroblast Growth Factor (FGF) signalling pathway. We consider a slightly simplified version of the model from [START_REF] Heath | Probabilistic model checking of complex biological pathways[END_REF], comprising interactions between a mixture of FGF ligands and receptors. In the π stoc formulation, the ν operator is used to give each FGF ligand a unique channel name. The binding between a particular FGF ligand and receptor is modelled by this name being passed between the two. Unbinding occurs through a communication over this private channel. We check the probability that all FGF receptors have relocated (are no longer active) by a certain time bound.

Table I shows the performance of our implementation on the case studies. Experiments were run on a 2 GHz PC with 2 GB RAM running Linux. For each case study, we analysed several models of increasing size by varying a parameter N . For the DCP model, N represents the number of parties; for PSE (we consider two variants: the original protocol EGL and the modified version EGL3 from [START_REF] Norman | Analysis of probabilistic contract signing[END_REF]) N is the size of contract; for the MCN models, N represents the number of base stations; and for FGF, N is the number of FGF ligands (the number of receptors remains fixed). The table shows the size of the resulting MDPs/CTMCs (number of states/transitions) and corresponding storage in PRISM (MTBDD nodes, where 1 node uses 20 bytes). We also give the time required for each stage of the process, i.e. constructing: the PSTGs (using MMC prob ); the PRISM code (using the translator); and the MDP or CTMC model (using PRISM). Finally, we give the time to check a single (quantitative) PCTL/CSL property for each using PRISM (with the fastest available engine).

The results are very encouraging. We see that our techniques are scalable to the construction and analysis of π prob and π stoc models with extremely large state spaces and that the times required for all stages of the process are relatively small. Furthermore, the compositional approach to the translation proved to be essential. On the FGF model (N =3), for example, constructing the full model in MMC prob took more than 100 times as long as the compositional technique. For larger parameter values, it was not feasible to directly construct the full model.

The MCN case study, although smallest in terms of state space, is a particularly good example of the applicability of this implementation since it fully exploits all mobile aspects of the calculus. The most obvious area for improvement in our results concerns MTBDD sizes. As is often the case with automatically generated code, the PRISM models resulting from our technique do not always exhibit the kind of structure and regularity that can be exploited by PRISM's symbolic implementation. We are confident that performance can be improved in this area.

VI. CONCLUSIONS

In this paper we have demonstrated the feasibility of implementing model checking for probabilistic and stochastic extensions of the π-calculus. Furthermore we have shown, through its application to several large examples, the efficiency of the approach. The probabilistic version of the π-calculus we used (with only blind probabilistic choice) has proved to be expressive enough for the appropriate application domains (probabilistic algorithms for security and dynamic communication protocols with failures and/or randomisation) and yet amenable to analysis with extensions and adaptions of existing verification tools. Similarly, the version of the stochastic πcalculus we used (with rates assigned to τ transitions and to channels) is both a natural formalism for modelling biological systems and well suited for the model checking techniques we have proposed.

We would like to extend this work in several directions. For convenience of modelling, we plan to add support for polyadic communication over channels. We also hope to add support for more flexible property specifications using watchdog processes. Finally, we will investigate ways to further improve the efficiency of our implementation, in particular, with regards to the automatically generated PRISM code. Possibilities include optimisations to reduce the resulting symbolic (MTBDD) storage in PRISM and bisimulation minimisation techniques.

Lemma 2 :

 2 Let P be a π stoc term. (a) If P M,α

  act ::= tau | in(X, Y) | out(X, Y) P ::= zero | pref(act, P) | choice( -→ P ) | prob choice( -----------→ pref(tau(p), P)) | par(P, P) | nu(X, P) | match((X = Y), P) | proc( Ā(Y1, . . . , Yn))

  complement(out(X, W), in(Y, W), W, true) :-X == Y. complement(out(X, W), in(Y, W), W, (X=Y)) :-X \== Y. complement(in(X, W), out(Y, W), W, true) :-X == Y. complement(in(X, W), out(Y, W), W, (X=Y)) :-X \== Y. comp_bound(outbound(X, W), in(Y, W), W, true) :-X == Y. comp_bound(outbound(X, W), in(Y, W), W, (X=Y)) :-X \== Y. comp_bound(in(X, W), outbound(Y, W), W, true) :-X == Y. comp_bound(in(X,W), outbound(Y, W), W, (X=Y)) :-X \== Y. not_in_any(_, []). not_in_any(Z, [pstep(_, A, _)|L]) :-not_in(Z, A), not_in_any(Z, L). not_in(_, tau). not_in(Z, in(X,Y)) :-Z \== X, Z \== Y. not_in(Z, out(X,Y)) :-Z \== X, Z \== Y. not_in(Z, outbound(X,Y)) :-Z \== X, Z \== Y. not_in(Z, outbound1(X,Y)) :-Z \== X, Z \== Y. not_in_constraint(_, true). not_in_constraint(X, (Y=Z)) :-X \== Y, X \== Z. not_in_constraint(X, (M, N)) :-not_in_constraint(X, M), not_in_constraint(X, N). upto(N, N) :-N > 0. upto(N, I) :-N > 0, N1 is N -1, upto(N1, I).

Fig. 4 . 1 Fig. 5 .

 415 Fig. 4. Auxiliary XSB code for the trans predicate def(toss(X), pref(in(X, Y), prob_choice([pref(tau(p), pref(out(Y, head), zero)), pref(tau(1-p), pref(out(Y, tail), zero))]))).| ?-stg(toss(try)). #1: proc(toss(try)) * 1: 1 == #2: prob_choice([pref(tau(p),pref(out(_h417,head), zero)),pref(tau(1-p),pref(out(_h417,tail),zero))]) >1: _h417 '1: --'1':in(try,_h417) --> 2 * 2: 2 == #3: pref(out(_h417,head),zero) '2: --'p':tau --> 3 #4: pref(out(_h417,tail),zero) '3: --'1 -p':tau --> 4 * 3: 3 == #5: zero '4: --'1':out(_h417,head) --> 5 * 4: 4 == '5: --'1':out(_h417,tail) --> 5 [1: try] [2: head] [3: tail] +++ Statistics of toss(try) +++ Nodes:5, Edges:5, P-Steps:4, Free Names:3, Bound Names:1

Fig. 6 .

 6 Fig.6. PRISM code for the example Process 1 includes two names c and d, available within the of Q 1 , representing private channels. It makes a random choice, outputting with equal probability either the name c or d on channel a. It then attempts to receive an input on the corresponding channel (c or d, respectively) and terminates. Process Q 2 is the parallel composition of two subprocesses which communicate over a channel b. The first subprocess inputs a name on channel a (which will be one of the two private channels from Q 1 ) and re-outputs it on channel b. The second subprocess inputs on channel b and then outputs e on whichever channel it received.Noting that c and d do not occur in Q 2 and that b does not occur in Q 1 , we can rewrite Q as the structurally congruent process P , defined as follows:

  [x=a]∧[y=b] where x, y are bound names and a, b free names, then the translation of M into PRISM is identical: (x=a)&(y=b), where x, y are integer variables and a, b integer constants.

Fig. 6

 6 line 7 for an example.

  and D. Parker are with the Oxford University Computing Laboratory, C. Palamidessi is with INRIA Saclay and École Polytechnique, and P. Wu is with University College London.

  that constitute states of the symbolic transition graph of P i becomes a set of integer indices Q i 1 , . . . , Q i ki uniquely representing each one. Module P i has |N bn i | + 1 local variables: its local state (i.e. the state of the corresponding symbolic transition graph) is represented by variable s i , with range Q i |N fn |. The model also includes |N fn | integer constants, one for each free name, which are assigned (in some arbitrary order) distinct, consecutive non-zero values.

	each bound name x i j ∈ N bn i x i j with range 0, . . . ,	1 , . . . , Q i ki , and has a corresponding variable

ACKNOWLEDGMENTS

Authors Norman and Parker were in the School of Computer Science at the University of Birmingham and Wu was at CNRS and LIX when parts of this work were first carried out. Norman and Parker are supported in part by EPSRC grants GR/S11107 and GR/S46727 and Microsoft Research Cambridge contract MRL 2005-44 and Palamidessi and Wu were supported in part by the INRIA/ARC project ProNoBis.

We thank the anonymous referees for their valuable comments.