On the stochastic operational semantics

The semantics of stochastic languages is usually given in terms of Continuous Time Markov Chains (CTMC in the following). Definition 2.1.1 (Continuous time Markov chain) A CTMC is a triple (S,→, s0) where S is a set of states, s0 ∈ S is the initial state and → is a function from S × S to R>0 called the stochastic transition relation (or also transition matrix). We use s λ−→ s ′ to represent (s, s′ , λ) ∈→, λ is called the rate. In this model a transition between two states s and s ′ is labelled with a stochastic rate λ that determines its sojourn time, that is the time spent in the state s before the transition could be fired. Formally the random variable governing this sojourn time is the exponential law of parameter λ: the probability of the transition being enabled within t time units is 1−e −λ×t . Due to the superposition property of the exponential distribution, in a state with n outgoing transitions of rate λ1, · · · , λn, the probability that the sojourn time is less than t is exponentially distributed with rate P i λi , i.e. Prob{delay < t} = 1−e −t P i ×λi , and in this case the probability that the j-th transition is fired is λj/( P i λi). This is known as the race condition. The operational semantics of a language is usually given in terms of a Labelled transition system[62]: in this approach, roughly speaking there is simply a transition from a state P to a state Q whenever P contains a redex of the language and the rewriting of this redex leads to Q. The derivation of a CTMC however is much more difficult because of the relevance of the number of redexes underlying the same transition. In order to illustrate this point let us consider a toy system where there are two species A and B and one rule ρ : A, A −→ B, B. This means that an occurrence of A, A can be rewritten into B, B. In the classical setting the labelled transition system contains, for instance, the following transitions: (a) A, A, B → B, B, B (b) A, A, A → B, B, A because in both cases the left hand side of the rule is a subterm of the left solutions. If we transfer this example to the stochastic setting, the reaction is equipped with a rate λ. Then in the case of (a) we have A, A, B λ−→ B, B, B and in the case of (b) we have A, A, A 3×λ −→ B, B, A, since there are respectively one and three occurrences of the reaction redex in (a) and (b). Formally, the rate 20 of a transition is the sum of the rates of the redexes underlying the transition. So one needs to count the number of these redexes. In contrast to the classical setting P and P + P are not bisimilar in a stochastic settings. In order to take care of the occurrences of redexes, we compute the stochastic semantics in two steps. First, we decorate the terms of the language with “tags” that permit us to distinguish between the occurrences of redexes. The derived transition relation, called the basic transition relation, is such that each transition corresponds to a unique redex. Then we compute the stochastic semantics by merging the transitions having the same source and target terms and by summing their rates: this is the collective transition relation. This approach is illustrated in the Sections 3.1, 4.2 and 6.3 with the definitions of the stochastic semantics of the nanoκ calculus, nanoπ-calculus and stochastic π-calculus respectively. 

On the infinite rates

In our modelings of nano-devices infinite rates happen to be very useful for representing reactions which are much faster than the others. Since they might introduce non-determinism infinite rates do not fit in the format of the CTMC and their analysis techniques. Nevertheless we want to be able to reuse these models and techniques. So we first use the model of Interactive Markov Chains [42] (IMC in the following) to handle infinite rates and then define the strictly Markovian condition under which we can recover the model of CTMC. But first we need to define the meaning of infinite rates. Intuitively if a transition has an infinite rate, it is infinitely fast: that is it takes no time to be fired. Formally the law governing the sojourn time is an exponential law of infinite parameter: for all t the probability of the transition to be enabled in t time units is 1 − e −∞∗t = 1. In particular it means that infinite rate transitions are always executed before finite rate ones. The model of IMC extends the CTMCs with interactive transitions which can be output or input on a given name or silent action. These transitions are executed under the maximal progress hypothesis which states that interactive transitions have higher priority than regular ones and should be executed first. Thus we can represent our infinite rate transitions by silent interactive transitions. The following definition presents the IMC restricted to silent interactive transitions: Definition 2.2.1 ((silent) Interactive Markov chain.) An interactive Markov chain is a tuple (S, 7−→, ∞7−→, s0) where S is a set of states, where 7−→ is a function from S × S to R>0 and where ∞7−→∈ S × S and where s0 ∈ S. s0 is the initial state, 7−→ is the stochastic transition relation (or also transition matrix) and ∞7−→ is the (silent) interactive transition relation. Notation (transient, Markovian states). We refer to the stochastic and interactive transition relations with only one relation: we write s α 7−→ s ′ either when α = ∞ and (s, s′ ) ∈ ∞7−→ or when α ∈ R>0 and 7−→ (s, s′ ) = α. A transition is immediate if it has infinite rate. We also call transient a state which has an immediate outgoing transition and Markovian a state which has no immediate outgoing transition. Given a set of states S we note S t and S m the subset of its transient and Markovian states respectively. The derivation of a CTMC semantics by means of basic and collective transition relations can be reused in the presence of infinite rates to derive an IMC semantics. The whole procedure for the derivation of the basic transition relation can be reused as it is. For the collective transition relation the only difficulty is the definition of the sum of the rates: it suffices to define ∞ + λ = ∞ for all finite rate λ. We now carry on with the downgrading of an IMC into a CTMC under the strictly Markovian property.