Mario Bravetti

# Reduction Semantics in Markovian Process Algebra

Mario Bravetti  Università di Bologna, Italy
INRIA, France
<EMAIL_ADDRESS>
###### Abstract

Stochastic (Markovian) process algebra extend classical process algebra with
probabilistic exponentially distributed time durations denoted by rates (the
parameter of the exponential distribution). Defining a semantics for such an
algebra, so to derive Continuous Time Markov Chains from system
specifications, requires dealing with transitions labeled by rates. With
respect to standard process algebra semantics this poses a problem: we have to
take into account the multiplicity of several identical transitions (with the
same rate). Several techniques addressing this problem have been introduced in
the literature, but they can only be used for semantic definitions that do not
exploit a structural congruence relation on terms while inferring transitions.
On the other hand, using a structural congruence relation is a useful
mechanism that is commonly adopted, for instance, in order to define semantics
in reduction style for non-basic process algebras such as the $\pi-$calculus
or richer ones. In this paper we show how to define semantics for Markovian
process algebra when structural congruence is used while inferring transitions
and, as an application example, we define the reduction semantics for a
stochastic version of the $\pi-$calculus. Moreover we show such semantics to
be correct with respect to the standard one (defined in labeled operational
semantics style).

###### keywords:

Markovian Process Algebra, Pi-calculus, Markov Chains

##  1 Introduction

The advantages of using process algebras for the performance modeling and
evaluation of concurrent systems due to their feature of compositionality have
been widely recognized (see [14, 1, 18, 13, 4, 3] and the references therein).
Particularly simple and successful has been the extension of standard process
algebras with time delays whose duration follows an exponential probability
distribution, called Markovian process algebras (see e.g. [14, 1, 18, 13, 5]).
The “timed” behavior of systems specified with a Markovian process algebra can
be represented by a continuous time Markov chain (CTMC), that is a simple
continuous time stochastic process where, in each time point, the future
behavior of the process is completely independent of its past behavior. Due to
their simplicity CTMCs can be analyzed with standard mathematical techniques
and software tools (see e.g. [21]) for deriving performance measures of
systems.

The semantics of all Markovian process algebras previously introduced in the
literature is defined in labeled operational semantics style, that is where
transitions are labeled with actions (representing potential of communication)
and transitions representing actual communications are produced by matching
action transitions of parallel processes. In this paper we present a technique
that allows us, for the first time, to develop semantics for Markovian process
algebra in reduction style (see for instance the reduction semantics of
$\pi$-calculus [19, 16]), that is where transitions are not labeled with
actions and are directly produced by readjusting the structure of terms via a
structural congruence relation: such a relation is endowed with commutative
and associative laws that allow communicating processes to get syntactically
adjacent to each other so to directly produce reduction transitions. Reduction
semantics is also commonly used, in that convenient for defining semantics of
complex languages, see for example [15].

Markovian process algebras extend usual process algebras with probabilistic
exponentially distributed time durations denoted by rates $\lambda$ (positive
real numbers), where $\lambda$ is the parameter of the exponential
distribution. Defining a semantics for such algebras, so to derive CTMCs from
system specifications, requires dealing with transitions labeled by rates
$\lambda$. With respect to standard process algebra semantics this poses a
problem: we have to take into account the multiplicity of several identical
transitions, that is transitions with the same rate and source and target
terms. The simplest way to deal with this problem (see [14]) is counting the
number of different possible inferences of the same transition so to determine
its multiplicity. However this can be done only for semantic definitions that
do not infer transitions by means of a structural congruence relation $\equiv$
on terms, that is via the classical operational rule of closure w.r.t.
$\equiv$ that makes it possible to infer a transition
$P\,\mathop{\longrightarrow}\limits^{\alpha}\,Q^{\prime}$ from
$Q\,\mathop{\longrightarrow}\limits^{\alpha}\,Q^{\prime}$ whenever $P\equiv
Q$. This because, supposing that common laws like $P\equiv P|\underline{0}$
are considered, the presence of such a rule causes the same transition to be
inferred in an infinite number of ways even in the case of just one occurrence
of a Markovian delay (e.g. consider $P$ just being a single Markovian delay
and the congruence law above). On the other hand using a structural congruence
relation is a useful mechanism that is commonly used, for instance, when
defining reduction semantics of non-basic process algebras such as the
$\pi-$calculus (to compute reductions due to communication while inferring
transitions, as we already mentioned).

Another similar way used in the literature to deal with Markovian transition
multiplicity is to explicitly introduce a mechanism to differently identify
multiple execution of identical Markovian delays by introducing some kind of
identifier that typically expresses syntactical position of the delay in the
term (for example it is called a “location” in the case of the position with
respect to the parallel operator) and whose syntax is dependent on the
operators used in the language (see, for instance, [11, 18]). Again, since
Markovian transitions are, roughly, identified by indicating the path
(left/right at every node) in the syntax tree of the term, this solution is
not compatible with inferring transition by means of a structural congruence
relation with the commutative and associative laws (which are fundamental,
e.g., to define a reduction semantics for the $\pi-$calculus). This because
term structure is readjusted at need during transition inference.

Finally, techniques exploiting the representation of Markovian transitions
collectively as a distribution over a target state space (a traditional
approach in the context of probabilistic transition systems, see Giry functor
[10] and its generalizations, for instance [20, 8, 22]) have been used in [7]
and in [9] for any Markovian process algebra whose operational rules are in a
Markovian extension of the GSOS rule format. These techniques are crucially
based on collectively inferring Markovian transitions performable at a certain
syntactical level (e.g. in $P\,|\,Q$) from transitions performable at lower
levels (e.g. from all Markovian transitions performable by $P$ and by $Q$).
Therefore, they are, again, not compatible with using structural congruence
$\equiv$ (with commutative and associative laws) during the inference of
transitions, as caused by the operational rule of closure w.r.t. $\equiv$
mentioned above, which is not in the GSOS format of [9] (the approach in [9]
cannot be used in the presence of such a rule, which is fundamental in
reduction semantics). Since there is not a fixed stratification of transition
inference, different transitions can be inferred by readjusting the structure
of terms via the commutative and associative laws of structural congruence in
different ways. For instance, given a term $P|(Q|R)$ it can be that the term
needs to be readjusted into $(P|Q)|R$ to infer a reduction due to a
communication between $P$ and $Q$ and to $(P|R)|Q$ to infer a reduction due to
a communication between $P$ and $R$. So we cannot fix a stratification of
transition inference, that is first collectively inferring all transitions of
$(Q|R)$ and then use them to infer all transitions of $P|(Q|R)$.

###  1.1 The Main Idea

In this paper we show how to define semantics for Markovian process algebras
in the presence of transitions inferred by means of structural congruence,
which also easily allows us to deal with a recursion operator: the possibility
of expressive cycling behavior is fundamental for steady state based
performance analysis. This will make it possible to define, for the first
time, the semantics of a Markovian process algebra (we will use a simple
Markovian version of $\pi-$calculus) via reduction semantics instead of
labeled operational semantics, as done in all above mentioned approaches.

Moreover our technique is such that the presence of Markovian delays in the
process algebra does not cause a significant modification of the process
algebra semantics, in that most of the burden is concentrated in a couple of
additional rules which are independent of the particular operators used by the
algebra. More precisely, we do not have to introduce an explicit (operator
dependent) mechanism to distinguish multiple occurrences of actions as in [11,
18], or to intervene in the semantics of every operator as in [7] or to
separately define, by induction on term syntax, how rate distribution is
calculated using (total) rate information attached to rules as in [9] (which
also does not cope with recursion). But more importantly, this opens the new
possibility to introduce Markovian delays in complex languages like that of
[15] without the need to completely change the semantics from reduction style
to labeled style.

The idea is to introduce stochastic names (that can be seen as names for
stochastic variables) and stochastic binders (binders for such names).
Stochastic names are used in process algebra prefixes and numerical rates
$\lambda$ are assigned by the corresponding stochastic binder. In essence (a
set of) stochastic binders act as a (probabilistic/stochastic) scheduler: they
use names attached to prefixes to collectively quantify them. In this way,
assuming that all prefixes are associated with a different stochastic name,
rate values replace stochastic names upon binding and multiplicity is
correctly taken into account because prefixes with the same rates are anyhow
distinguished by having different stochastic names.

But how to guarantee that prefixes are given different stochastic names? The
idea is to consider a specification language where prefixes are, as usual,
associated with numerical rates $\lambda$ and then to turn them (by a law of
structural congruence) into stochastic names that are immediately bound with a
stochastic binder assigning the rate $\lambda$. Then, with the usual rules of
binder extrusion, we impose that, before binders can be evaluated, they must
be all lifted to the outermost syntactical level by structural congruence. As
a consequence we have the guarantee (due to the requirement of
$\alpha$-conversion related to binder extrusion) that every prefix is assigned
a distinguished stochastic name. Note that recursion is dealt with in the
correct way as well, because, as we will see, recursions need to be unfolded
in order to perform the lift of the binders.

###  1.2 Plan of the Paper

In this paper we consider a simple extension of the $\pi-$calculus with
Markovian delays, where for the sake of simplicity, Markovian delays are
expressed separately from standard actions as in the Interactive Markov Chains
approach of [13]. We first define the semantics of this calculus in labeled
operational semantics style (we use the early semantics of the $\pi-$calculus)
according to the classical approach of [11, 18], that is using an explicit
(operator dependent) mechanism to distinguish multiple occurrences of
Markovian delays. We then apply our technique based on stochastic names and
binders to provide a reduction semantics for the very same process algebra. We
finally assess the correctness of our approach by showing that a theorem
similar to the Harmony Lemma in [19] (or the one in [16]) holds true, that is:
stochastic and standard reductions of reduction semantics are in
correspondence with $\tau$ and Markovian delay transitions of the labeled
operational semantics and, thus, the underlaying Interactive Markov Chains.

In particular, in Sect. 2 we present the Markovian $\pi-$calculus and its
labeled operational semantics defined according to the “classical” technique.
In Sect. 3 we present the reduction semantics for the Markovian
$\pi-$calculus. In Sect. 4 we conclude the paper by further discussing related
work and future extensions of the technique. Finally, Appendix A includes a
long proof for a proposition (whose proof structure is described in the paper
body). The work in this paper is based on the technical report [2].

##  2 Classical Approach

We consider $\pi-$calculus with constant definitions (as in [17]) extended
with Markovian delay prefixes (following the approach in [13]). Markovian
delays are thus simply represented by $(\lambda)$ prefixes, where $\lambda$ is
the rate of a Markovian distribution. As usual in the context of Markovian
process algebra (see e.g. [18]) we consider recursion by constant definitions
(as done for the standard $\pi-$calculus e.g. in [17]) and not by a bang
operator. Moreover, as usual, we assume recursion to be (weakly) guarded. In
this way we avoid terms like $A\buildrel\Delta\over{=}A|(\lambda).P$ for which
we would not get a finite cumulative rate for the outgoing Markovian
transitions of A.

Let $x,y,\dots$ range over the set ${\cal X}$ of channel names and $\lambda$
range over the set + of rate values (representing rates of Markovian
distributions).

######  Definition 2.1.

The syntax of terms $P,Q,\dots$ is:

$\begin{array}[]{lll}P&::=&M\mid P|P^{\prime}\mid(\nu x)P\mid
A(x_{1},\dots,x_{n})\\\ M&::=&\underline{0}\mid\alpha.P\mid M+M^{\prime}\\\
\alpha&::=&\overline{x}\mbox{$<$}y\mbox{$>$}\mid
x(y)\mid\tau\mid({\lambda})\end{array}$

We take ${\cal P}$ to be the set of terms $P,Q,\dots$ generated by this
syntax.

We abbreviate $x_{1},\dots,x_{n}$ with $\tilde{x}$ and we assume a given set
of constant definitions $A(\tilde{x})\buildrel\Delta\over{=}P$. Technically we
assume that for every constant $A(\tilde{x})\buildrel\Delta\over{=}P$ the
following holds true. We can, starting from $P$ and by performing a finite
number of successive substitutions of constants $B(\tilde{y})$ for their
defining term $Q\\{\tilde{y}/\tilde{x}\\}$ (assuming
$B(\tilde{x})\buildrel\Delta\over{=}Q$) reach a term $P^{\prime}$ where every
constant occurs in $P^{\prime}$ in the scope of a prefix operator ($A$ is
weakly guarded defined, see [17]).

###  2.1 Labeled Operational Semantics

Concerning the labeled operational semantics we consider the early semantics
of the $\pi-$calculus (see e.g. [19]) and, concerning Markovian delays, the
classical approach of [18], i.e. using an explicit (operator dependent)
mechanism to distinguish multiple occurrences.

The operational semantics is thus defined by a transition system with two kind
of transitions:

  * •

The classical $\pi-$calculus early semantics labeled transitions, defined in
Table 1 (we assume, as usual, symmetric rules to be also included, the meaning
of labels and the definition of functions $n$ (names), $bn$ (bound names) and
$fn$ (free names) to be the standard one, see, e.g., [19] and $\mu,\eta$ to
range over sets including all standard labels), and

  * •

Markovian transitions, defined in Table 2, that are labeled with pairs
$\lambda,id$ where: $\lambda$ is the rate of the Markovian delay being
executed and $id$ is a unique identifier. An identifier $id$ is a string over
the alphabet $\\{+_{0},+_{1},|_{0},|_{1}\\}$ and represents the syntactical
position of the delay in the syntax tree of the term (the path in the tree).
Notice that $\eta$ (differently from $\mu$) also ranges over labels
$\lambda,id$ of Markovian transitions, whose definition, thus, includes also
the involved rules of Table 1.

$\begin{array}[]{ccc}\lx@intercol\hfil\tau.P\,\mathop{\longrightarrow}\limits^{\tau}\,P\hskip
28.45274pt\overline{x}\mbox{$<$}y\mbox{$>$}.P\,\mathop{\longrightarrow}\limits^{\overline{x}y}\,P\hskip
<EMAIL_ADDRESS>&\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\mu}\,P^{\prime}\\\
\hline\cr
P+Q\,\mathop{\longrightarrow}\limits^{\mu}\,P^{\prime}\end{array}&\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\mu}\,P^{\prime}\\\
\hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\mu}\,P^{\prime}|Q\end{array}\hskip
8.5359ptbn(\mu)\cap fn(Q)=\emptyset\\\
&\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\overline{x}y}\,P^{\prime}\hskip
14.22636ptQ\,\mathop{\longrightarrow}\limits^{xy}\,Q^{\prime}\\\ \hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\tau}\,P^{\prime}|Q^{\prime}\end{array}&\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\overline{x}(y)}\,P^{\prime}\hskip
14.22636ptQ\,\mathop{\longrightarrow}\limits^{xy}\,Q^{\prime}\\\ \hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\tau}\,(\nu
x)P^{\prime}|Q^{\prime}\end{array}\hskip 8.5359pty\notin fn(Q)\\\
\lx@intercol\hfil\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\eta}\,P^{\prime}\\\
\hline\cr(\nu x)P\,\mathop{\longrightarrow}\limits^{\eta}\,(\nu
x)P^{\prime}\end{array}\hskip 5.69046ptx\notin n(\eta)\hskip
14.22636pt\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\overline{x}y}\,P^{\prime}\\\
\hline\cr(\nu
y)P\,\mathop{\longrightarrow}\limits^{\overline{x}(y)}\,P^{\prime}\end{array}\hskip
5.69046pty\neq x\hskip
14.22636pt\begin{array}[]{c}P\\{\tilde{y}/\tilde{x}\\}\,\mathop{\longrightarrow}\limits^{\eta}\,P^{\prime}\\\
\hline\cr
A(\tilde{y})\,\mathop{\longrightarrow}\limits^{\eta}\,P^{\prime}\end{array}\hskip
5.69046ptA(\tilde{x})\buildrel\Delta\over{=}P\hfil\lx@intercol\end{array}$

Table 1: Standard Rules

$\begin{array}[]{c}(\lambda).P\,\mathop{\longrightarrow}\limits^{\lambda,\varepsilon}\,P\\\\[5.69046pt]
\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}\\\
\hline\cr
P+Q\,\mathop{\longrightarrow}\limits^{\lambda,+_{0}\,id}\,P^{\prime}\end{array}\hskip
22.76228pt\begin{array}[]{c}Q\,\mathop{\longrightarrow}\limits^{\lambda,id}\,Q^{\prime}\\\
\hline\cr
P+Q\,\mathop{\longrightarrow}\limits^{\lambda,+_{1}\,id}\,Q^{\prime}\end{array}\hskip
22.76228pt\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}\\\
\hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\lambda,|_{0}\,id}\,P^{\prime}|Q\end{array}\hskip
22.76228pt\begin{array}[]{c}Q\,\mathop{\longrightarrow}\limits^{\lambda,id}\,Q^{\prime}\\\
\hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\lambda,|_{1}\,id}\,P|Q^{\prime}\end{array}\\\
\end{array}$

Table 2: Identified Markovian Transitions

The labeled transition system arising from the semantics of a term $P$ has
states with both outgoing Markovian and standard transitions (Interactive
Markov Chain) and has to be interpreted as in [13]. In particular the
Markovian transitions performable in states that also have outgoing $\tau$
transitions are considered to be pre-empted (maximal progress assumption where
“$\tau$” are instantaneous) and a system is considered to be complete if it
cannot undergo further communication with the environment, i.e. it can perform
only $\tau$ and Markovian transitions.

This is expressed by the notion of Markovian Bisimulation considered in [13].
We first define the total rate $\gamma(P,P^{\prime})$ of transiting from state
$P$ to $P^{\prime}$ with Markovian transitions as
$\gamma(P,P^{\prime})=\sum_{P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}}\lambda$.
This is extended to sets of states in the usual way:
$\gamma(P,Set)=\sum_{P^{\prime}\in Set}\gamma(P,P^{\prime})$.

We can now consider the Markovian bisimulation as in [13] (see [13] for weak
bisimulation definition abstracting, when possible, from $\tau$ transitions).

######  Definition 2.2.

An equivalence relation ${\cal B}$ on ${\cal P}$ is a strong bisimulation iff
$P{\cal B}Q$ implies for all $\mu$ and all equivalence classes $C$ of ${\cal
B}$

  * •

$P\,\mathop{\longrightarrow}\limits^{\mu}\,P^{\prime}$ implies
$Q\,\mathop{\longrightarrow}\limits^{\mu}\,Q^{\prime}$ for some $Q^{\prime}$
with $Q^{\prime}{\cal B}P^{\prime}$

  * •

$P\not\\!\\!\,\mathop{\longrightarrow}\limits^{\tau}\,$ implies
$\gamma(P,C)=\gamma(Q,C)$

Two processes $P$ and $Q$ are strongly bisimilar, written $P\sim Q$,if they
are contained in some strong bisimulation.

##  3 Reduction Semantics for Markovian Delays

In this section we use our technique based on symbolic representation of rates
via stochastic names and stochastic binders to give a semantics in reduction
style for the Markovian $\pi-$calculus of Section 2.

###  3.1 Stochastic Names and Stochastic Binders

We now extend the syntax of terms $P,Q,\dots$ by adding stochastic names and
stochastic binders. We use $q,q^{\prime},\dots\in{\cal Q}{\cal N}$ to range
over names used to express symbolically stochastic information for delays.
$\theta,\theta^{\prime},\dots$ ranges over ${\cal X}\cup{\cal Q}{\cal N}$.

######  Definition 3.1.

We take ${\cal P}_{ext}$ to be the set of terms $P,Q,\dots$ generated by the
syntax in Definition 2.1, where we add:“$(\nu q\rightarrow\\!\lambda)P$” to
the possible instantiations of $P$, and “$(q)$” to the possible instantiations
of $\alpha$ prefixes.

$(\nu q\rightarrow\\!\lambda)$ is a stochastic binder for name $q$ used by a
delay, that associates value $\lambda$ to it. In the following we use $(\nu
x\rightarrow\\!\varepsilon)$ to stand for $(\nu x)$, i.e. the standard
$\pi$-calculus binder, which does not associate any value to $x$, This will
allow us to write $(\nu\theta\rightarrow\\!\widehat{\,\lambda})$ to stand for
any binder (stochastic or classical) by assuming
$\widehat{\,\lambda},\widehat{\,\lambda^{\prime}\\!}$ to range over
${}^{+}\cup\\{\epsilon\\}$.

Notice that we will used ${\cal P}_{ext}$ terms over the extended syntax to
define the semantics of ${\cal P}$ terms in reduction style. As we will see,
for every state of the semantics we will always have a congruent term which
belongs to ${\cal P}$. The definition of structural congruence follows.

###  3.2 Structural Congruence Relation

$\begin{array}[]{llll}(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})P\;|\;Q&\equiv&(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})(P|Q)&\mbox{if}\;\theta\notin
fn(Q)\\\
(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})(\nu\theta^{\prime}\rightarrow\\!\\!\widehat{\,\lambda^{\prime}\\!})P&\equiv&(\nu\theta^{\prime}\rightarrow\\!\\!\widehat{\,\lambda^{\prime}\\!})(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})P&\mbox{if}\;\theta\neq\theta^{\prime}\\\
(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})\underline{0}&\equiv&\underline{0}\\\
(M_{1}+M_{2})+M_{3}&\equiv&M_{1}+(M_{2}+M_{3})&\\\ M+N&\equiv&N+M\\\
M+\underline{0}&\equiv&M\\\ (P_{1}|P_{2})|P_{3}&\equiv&P_{1}|(P_{2}|P_{3})&\\\
P|Q&\equiv&Q|P\\\ P|\underline{0}&\equiv&P\\\
A(\tilde{y})&\equiv&P\\{\tilde{y}/\tilde{x}\\}&\mbox{if}\;A(\tilde{x})\buildrel\Delta\over{=}P\\\
\end{array}\\\ $

Table 3: Standard Structural Congruence Laws (with quantified binders)

We consider a structural congruence relation over processes in ${\cal
P}_{ext}$ defined as usual by a set of laws. We consider the standard laws in
Table 3 (where we just add the possible presence of quantification in binders)
and, in addition, the following law:

$\begin{array}[]{llll}(\lambda).P+M&\equiv&(\nu
q\rightarrow\\!\lambda)(\,(q).P+M)&\mbox{if}\;q\notin fn(M,P)\\\ \end{array}$

As usual, alpha renaming inside processes, concerning any name $\theta$ and
its binder $(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})$ is assumed.
Concerning use of parentheses when writing terms in the laws above, we assume
binding to take precedence over parallel and prefix to take precedence over
sum.

###  3.3 Operational Semantics

We now define the semantics of the process algebra of Definition 3 in
reduction style. As we will see besides standard reduction transitions
(defined with standard rules), we have two other kinds of transitions
representing stochastic execution. Transitions labeled with a stochastic delay
name which are treated similarly as standard reduction transitions and
stochastic transitions (that are generated when a stochastic binder is applied
at the top level). The latter lead from a term to a rate distribution over
terms.

We consider rate distributions $\sigma$ describing how a state can be reached
from another one by performing a Markovian transition.

######  Definition 3.2.

A rate distribution $\sigma$ over a set $S$ is a non-empty finite multiset
over ${}^{+}\times S$, i.e. a multiset of pairs $(\lambda,e)$, with
$\lambda\in{}^{+}$ and $e\in S$. We use $RDist(S)$ to denote the set of rate
distributions over $S$.

Due to usage of the structural congruence relation, it will be convenient to
use rate distributions $\sigma$ over congruence classes of terms, i.e.
$RDist({\cal P}_{ext}/\\!\equiv)$.

The operational semantics is defined in terms of three transition relations:

  * •

Standard reductions [16] that represent action execution, leading from a term
to another term and denoted by
$P\,\mathop{\longrightarrow}\limits\,P^{\prime}$.

  * •

Transitions similar to standard reductions [16] that represent delay
executions and just differ from reductions in that they are additionally
labeled with the name $q$ associated to the delay: their quantification is
symbolical in that the name of the delay is included and not the actual rate.
They are denoted by $P\,\mathop{\longrightarrow}\limits^{q}\,P^{\prime}$.

  * •

Stochastic transitions leading from a term to a rate distribution on
congruence classes of terms. They are denoted denoted by
$P\,\mathop{\longrightarrow}\limits\,\sigma$, where $\sigma\in RDist({\cal
P}_{ext}/\\!\equiv)$.

$\begin{array}[]{c}(q).P+M\,\mathop{\longrightarrow}\limits^{q}\,P\hskip
28.45274pt\mbox{}\tau.P+M\,\mathop{\longrightarrow}\limits\,P\hskip
28.45274pt\mbox{}x(z).P+M\;|\;\overline{x}\mbox{$<$}y\mbox{$>$}.Q+N\,\mathop{\longrightarrow}\limits\,P\\{y/z\\}\;|\;Q\\\\[11.38092pt]
\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,P^{\prime}\\\
\hline\cr
P|Q\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,P^{\prime}|Q\end{array}\hskip
14.22636pt\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,P^{\prime}\\\
\hline\cr(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})P\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,(\nu\theta\rightarrow\\!\\!\widehat{\,\lambda})P^{\prime}\end{array}\hskip
5.69046pt\theta\neq q\hskip 14.22636pt\begin{array}[]{c}P\equiv Q\hskip
8.5359ptQ\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,Q^{\prime}\hskip
8.5359ptQ^{\prime}\equiv P^{\prime}\\\ \hline\cr
P\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,P^{\prime}\end{array}\end{array}$

Table 4: Standard Rules for Reductions and Symbolically Quantified Transitions

The first two relations are collectively defined as the smallest subset of
${\cal P}_{ext}\times({\cal Q}{\cal N}\cup{\varepsilon})\times{\cal P}_{ext}$
(where $\varepsilon$ labeled reductions represent the standard ones of [16])
satisfying the operational rules in Table 4, where $\\!\widehat{q}\in{\cal
Q}{\cal N}\cup\\{\varepsilon\\}$. With respect to the usual ones of [16], the
rules in Table 4 only differ for including a rule for delay prefix and for
considering names $q\in{\cal Q}{\cal N}$ as possible reduction labels (and
rates $\lambda$ possibly associated to binders).

Stochastic $P\,\mathop{\longrightarrow}\limits\,\sigma$ transitions are
defined as the smallest subset of ${\cal P}_{ext}\times RDist({\cal
P}_{ext}/\\!\equiv)$ satisfying the operational rules in Table 5, where we
assume $(\nu q\rightarrow\\!\lambda)\sigma=\\{\\!|\,(\lambda,[(\nu
q\rightarrow\\!\lambda)P]_{\equiv})\mid(\lambda,[P]_{\equiv})\in\sigma\,|\\!\\}$.111We
use $\\{\\!|\,$ and $\,|\\!\\}$ to denote multiset parentheses, $\cup$ to
denote multiset union. Notice that even if the (Sto2) rule includes a negative
premise the operational semantics is well-defined in that the inference of
transitions can be stratified (see, e.g., [12]).

The idea behind the semantics is that
$\,\mathop{\longrightarrow}\limits\,\sigma$ transitions can be generated only
for terms that are (re)organized by the structural congruence in such a way
that stochastic binders (actually binding a delay) are the outermost
operators, thus they can correctly evaluate the multiset of Markovian
transitions leaving a state from symbolic delay transitions (each of which is
guaranteed to have a different name).

$\begin{array}[]{cc}\lx@intercol\hfil(Sto1)\hskip
5.69046pt\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits\,\sigma\hskip
14.22636ptP\,\mathop{\longrightarrow}\limits^{q}\,P^{\prime}\\\ \hline\cr(\nu
q\rightarrow\\!\lambda)P\,\mathop{\longrightarrow}\limits\,(\nu
q\rightarrow\\!\lambda)\sigma\cup\\{\\!|\,(\lambda,[(\nu
q\rightarrow\\!\lambda)P^{\prime}]_{\equiv})\,|\\!\\}\end{array}\hfil\lx@intercol\\\
(Sto2)\hskip
5.69046pt\begin{array}[]{c}P\,\mathop{\longrightarrow}\limits\,\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!/\,\,\,\,\,\,\,\,\,\,\sigma\hskip
14.22636ptP\,\mathop{\longrightarrow}\limits^{q}\,P^{\prime}\\\ \hline\cr(\nu
q\rightarrow\\!\lambda)P\,\mathop{\longrightarrow}\limits\,\\{\\!|\,(\lambda,[(\nu
q\rightarrow\\!\lambda)P^{\prime}]_{\equiv})\,|\\!\\}\end{array}&\hskip
14.22636pt(StoCong)\hskip 5.69046pt\begin{array}[]{c}P\equiv Q\hskip
14.22636ptQ\,\mathop{\longrightarrow}\limits\,\sigma\\\ \hline\cr
P\,\mathop{\longrightarrow}\limits\,\sigma\end{array}\end{array}$

Table 5: Rules for Stochastic Transitions

######  Example 3.3.

Consider $P=(5).A|(5).A$ and $A\buildrel\Delta\over{=}(5).A$ we have that
$P\equiv(\nu q\rightarrow\\!5)(q).A|(\nu q\rightarrow\\!5)(q).A\equiv(\nu
q\rightarrow\\!5)(\nu q^{\prime}\rightarrow\\!5)((q).A|(q^{\prime}).A)$ hence
$P$ performs a $\sigma$ transition with
$\sigma=\\{\\!|\,(5,[(5).A|(5).A]_{\equiv}),(5,[(5).A|(5).A]_{\equiv})\,|\\!\\}$,
i.e. it is a multiset including two occurrences of the same pair.

The transition system of terms can be represented in a finitary way by
resorting to equivalence classes $[P]_{\equiv}\in{\cal P}_{ext}/\\!\equiv$.
This will be important when deriving, as done in Section 2 for the labeled
operational semantics, the underlying Interactive Markov Chain.

######  Definition 3.4.

Let $P,P^{\prime}\in{\cal P}_{ext}$.
$[P]_{\equiv}\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,[P^{\prime}]_{\equiv}$
whenever $P\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,P^{\prime}$.
Let $P\in{\cal P}_{ext}$ and $\sigma\in RDist({\cal P}_{ext}/\\!\equiv)$.
$[P]_{\equiv}\,\mathop{\longrightarrow}\limits\,\sigma$ whenever
$P\,\mathop{\longrightarrow}\limits\,\sigma$.

The above is well-defined because congruent terms $P$ have the same
transitions (rule of closure w.r.t. congruence in each of Tables 4 and 5).
Notice that it is also possible to define directly transitions of equivalence
classes, instead of resorting to a definition like Definition 3.4, by putting
equivalence classes directly into rules, e.g. for parallel

${\begin{array}[]{c}[P]_{\equiv}\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,[P^{\prime}]_{\equiv}\\\
\hline\cr[P|Q]_{\equiv}\,\mathop{\longrightarrow}\limits^{\\!\widehat{q}}\,[P^{\prime}|Q]_{\equiv}\end{array}}$

This would also make the two rules of closure w.r.t. congruence in each of
Tables 4 and 5 no longer needed (working directly with classes yields the same
effect).

Let us now analyze properties of transitions of terms $P\in{\cal P}$ (that is
terms belonging to the restricted syntax of Definition 2.1).

First of all we have that they cannot perform
$\,\mathop{\longrightarrow}\limits^{q}\,$ transitions.

######  Proposition 3.5.

Let $P\in{\cal P}$. There is no $P^{\prime}\in{\cal P}_{ext}$, $q\in{\cal
Q}{\cal N}$ such that $P\,\mathop{\longrightarrow}\limits^{q}\,P^{\prime}$.

######  Proof 3.6.

A direct consequence of the fact that for any $Q\equiv P$, with $P\in{\cal
P}$, we have that, due to the laws of $\equiv$, all delay prefixes $(q)$
occurring in $Q$ are bound (rules for binders do not allow transition labeled
with the bound name to be inferred).

The following proposition shows that Markovian transitions are well-defined,
i.e. roughly that, no matter the order in which we choose to solve the
stochastic binders, the $\sigma$ transition performed is the same.

######  Proposition 3.7.

Let $P\in{\cal P}$ and $P\,\mathop{\longrightarrow}\limits\,\sigma$. We have
$P\,\mathop{\longrightarrow}\limits\,\sigma^{\prime}$ implies
$\sigma=\sigma^{\prime}$.

######  Proof 3.8.

The complete formal proof is quite involved and is presented in Appendix A. In
the following we just present the structure of the proof in some detail and
the main ideas.

Let $n$ be the number of unguarded syntactical occurrences of Markovian delay
prefixes inside $P$. Formally $n$ is evaluated as follows: $P^{\prime}$ is
obtained from $P$ by performing a finite number of successive substitutions of
constants so that all constants occur weakly guarded in $P^{\prime}$ (always
possible because recursion is guarded, see Section 3); $n$ is the number of
Markovian delay prefixes that occur in $P^{\prime}$ not in the scope of a
prefix operator. Since $P\,\mathop{\longrightarrow}\limits\,\sigma$ we must
have $n\geq 1$.

We first show, by induction on $k$, with $0\leq k\leq n$ ($k=0$ being the base
case), that the following statement holds true (see Appendix A for details on
the induction proof). Let $q_{1}$, …, $q_{k}$ be any set of distinguished
names. There exists $Q$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu q_{k}\rightarrow\\!\lambda_{k})Q$
(consider $P\equiv Q$ in the case $k=0$) and $\forall i,1\leq h\leq k\ldotp
Q\,\mathop{\longrightarrow}\limits^{q_{h}}\,$. Moreover for any such $Q$, we
have, supposing $\forall h,1\leq h\leq k\ldotp
Q\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$, that:

  * •

$Q$ includes a unique free unguarded syntactical occurrence of $(q_{h})$
$\forall h,1\leq h\leq k$ (this reduces to true for the base case $k=0$).

  * •

If $k<n$, for any $q$ distinguished from $q_{h}$ $\forall h,1\leq h\leq k$,
there exist $Q^{\prime},\lambda$ such that $Q\equiv(\nu
q\rightarrow\\!\lambda)Q^{\prime}$ and
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q}\,$, i.e.
$Q\,\mathop{\longrightarrow}\limits\,\sigma$ for some $\sigma$. Moreover, any
such $Q^{\prime}$ includes unique free unguarded syntactical occurrences of
$(q_{h})$ $\forall h,1\leq h\leq k$ and, supposing $\forall h,1\leq h\leq
k\ldotp
Q^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime\prime}_{h}$, we
have that $(\nu q\rightarrow\\!\lambda)P^{\prime\prime}_{h}\equiv
P^{\prime}_{h}$.

  * •

If, instead, $k=n$ there is no $Q^{\prime},q,\lambda$ such that $Q\equiv(\nu
q\rightarrow\\!\lambda)Q^{\prime}$ and
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q}\,$, i.e.
$Q\not\,\mathop{\longrightarrow}\limits\,\sigma$.

Considering case $k=n$ of the above, we have that, given distinguished names
$q_{1}$, …, $q_{n}$, there exists $P^{\prime}$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}$ and $\forall i,1\leq h\leq n\ldotp
P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,$. Moreover for any such
$P^{\prime}$ we have that $P^{\prime}$ includes a unique free unguarded
syntactical occurrence of $(q_{i})$ $\forall i,1\leq i\leq n$.

We then show, by induction on the length of inference chains (see Appendix A),
that inferring a $\sigma$ transition from $P$ (where $q_{1}$ is the name of
the binder used to infer $\sigma$ in the last rule used in the inference chain
and so on and so forth in depth until $q_{n}$ where the chain of binder
applications begins with the (Sto2) rule) entails singling out one of such
terms $P^{\prime}$ and that, supposing $\forall h,1\leq h\leq n\ldotp
P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$, the
inferred $\sigma$ is such that

$\sigma=\\{\\!|\,(\lambda_{1},[(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{1}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{n},[(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{n}]_{\equiv})\,|\\!\\}$

Notice that this value does not depend on the choice of the $P^{\prime}_{h}$
such that
$P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$ in that,
since $P^{\prime}$ includes a unique free unguarded syntactical occurrence of
$(q_{h})$, possible terms $P^{\prime}_{h}$ are all related by $\equiv$ (and,
in general, $P\equiv Q$ implies $(\nu q\rightarrow\\!\lambda)P\equiv(\nu
q\rightarrow\\!\lambda)Q$ for any $P,Q,q$ and $\lambda$).

From this fact we can derive that the $\sigma$ inferred is the same for any
possible inference chain of a $\sigma$ transition from $P$, i.e. that no
matter the order in which delay prefixes are bound, the same rate distribution
is obtained. This because, considered $\sigma^{\prime}$ derived with another
inference chain, such an inference would determine a $P^{\prime\prime}$ such
that $P\equiv(\nu q^{\prime}_{1}\rightarrow\\!\lambda^{\prime}_{1})\dots(\nu
q^{\prime}_{n}\rightarrow\\!\lambda^{\prime}_{n})P^{\prime\prime}$ and
$\forall i,1\leq i\leq n\ldotp
P^{\prime\prime}\,\mathop{\longrightarrow}\limits^{q^{\prime}_{i}}\,$. It is
immediate to verify that there exists a permutation $k_{i}$, with $1\leq i\leq
n$, such that, by alpha-conversion we can write $(\nu
q^{\prime}_{1}\rightarrow\\!\lambda^{\prime}_{1})\dots(\nu
q^{\prime}_{n}\rightarrow\\!\lambda^{\prime}_{n})P^{\prime\prime}$ as $(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime\prime}$ where for
$P^{\prime\prime\prime}$ it holds $P^{\prime\prime\prime}\equiv P^{\prime}$.
Thus $\sigma^{\prime}=\\{\\!|\,(\lambda_{k_{1}},(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime}_{k_{1}}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{k_{n}},[(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime}_{k_{n}}]_{\equiv})\,|\\!\\}$,
where $\forall i,1\leq i\leq n$ we have $P^{\prime\prime}_{k_{i}}\equiv
P^{\prime}_{k_{i}}$ because $P^{\prime}$ includes a unique free unguarded
syntactical occurrence of $(q_{i})$ $\forall i,1\leq i\leq n$.
$\sigma^{\prime}=\sigma$ by reordering of the binders, of the members of the
multiset union and from the fact that $P\equiv Q$ implies $(\nu
q\rightarrow\\!\lambda)P\equiv(\nu q\rightarrow\\!\lambda)Q$ for any $P,Q,q$
and $\lambda$.

Moreover, from terms in ${\cal P}$ we always reach terms in ${\cal P}$ modulo
congruence.

######  Proposition 3.9.

Let $P\in{\cal P}$ and $P^{\prime}\in{\cal P}_{ext}$ such that
$P\,\mathop{\longrightarrow}\limits\,P^{\prime}$ or
$P\,\mathop{\longrightarrow}\limits\,\sigma$ and $\exists\lambda$ such that
$(\lambda,[P^{\prime}]_{\equiv})\in\sigma$. There exists
$P^{\prime\prime}\in{\cal P}$ such that $P^{\prime\prime}\equiv P^{\prime}$.

######  Proof 3.10.

For any $Q\equiv P$ with $P\in{\cal P}$ we have: all delay prefixes $(q)$
occurring in $Q$ are bound and every stochastic binder can bind at most a
single delay prefix $(q)$. It is easy to verify that this property is
preserved by reductions $Q\,\mathop{\longrightarrow}\limits\,Q^{\prime}$ or
transitions $Q\,\mathop{\longrightarrow}\limits\,\sigma$ for which
$\exists\lambda$ such that $(\lambda,[Q^{\prime}]_{\equiv})\in\sigma$, i.e.
for any such $Q^{\prime}$ the same property holds true. For instance
performing the $\sigma$ transition causes the corresponding stochastic binder
to not bind any delay prefix in the target state. Any $Q^{\prime}$ satisfying
the property above can be shown to be $\equiv$ to a term of $P$ by just
removing stochastic binders not binding any delay prefix and by turning
stochastic binder binding a single delay prefix $(q)$ into a Markovian delay
prefix.

A consequence of the above propositions is that, given $P\in{\cal P}$, we can
represent the semantics of $P$ as a labeled transition system whose initial
state is $[P]_{\equiv}$ and, in general, states (congruence classes reachable
from $[P]_{\equiv}$) are $[P^{\prime}]_{\equiv}$ such that $P^{\prime}\in{\cal
P}$ (such classes always have a representative in ${\cal P}$). In particular,
concerning the underlying Interactive Markov Chain, see Section 2, we have
that

  * •

the rate $\gamma([P]_{\equiv},[P^{\prime}]_{\equiv})$ of transiting from state
$[P]_{\equiv}$ to state $[P^{\prime}]_{\equiv}$ is:
$\sum_{(\lambda,[P^{\prime}]_{\equiv})\in\sigma}\lambda\cdot\mu_{\sigma}(\lambda,[P^{\prime}]_{\equiv})$
if $[P]_{\equiv}\,\mathop{\longrightarrow}\limits\,\sigma$ for some $\sigma$;
$0$ otherwise222We assume an empty sum to yield $0$. Given a multiset $m$,
$\mu_{m}(e)$ denotes the number of occurrences of element $e$ in $m$.

  * •

$\tau$ transitions of the Interactive Markov Chain are standard reductions.

The above also provides a definition of bisimulation over states of $P\in{\cal
P}$ by applying it to Definition 2.2 (and to other equivalences in [13]).
Obviously the reduction semantics yields a closed system interpretation (i.e.
corresponding to labeled operational semantics where all actions are assumed
to be bound at the top level), thus the obtained Interactive Markov Chain is
just labeled with $\tau$ actions as for all Interactive Markov Chains
corresponding to complete (and not partial) systems, which are commonly the
ones to be analyzed for performance.

In the following we formalize this correspondence. In the classical setting
this has been done for the $\pi-$calculus, see, e.g., Harmony Lemma in [19] or
[16]. Here we extend this result to Markovian delays.

######  Theorem 3.11 (Harmony).

Let $P\in{\cal P}$. We have:

  * •

$P\,\mathop{\longrightarrow}\limits\,P^{\prime}$ iff
$P\,\mathop{\longrightarrow}\limits^{\tau}\,\\!\equiv P^{\prime}$

  * •

$P\,\mathop{\longrightarrow}\limits\,\sigma$ for some $\sigma$ iff
$P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}$ for some
$\lambda$, $id$ and $P^{\prime}$. Moreover in the case both hold true, we have
that $\forall P^{\prime}\in{\cal P}$

$\sum_{(\lambda,[P^{\prime}]_{\equiv})\in\sigma}\lambda\cdot\mu_{\sigma}(\lambda,[P^{\prime}]_{\equiv})=\sum_{P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,\equiv
P^{\prime}}\lambda$

######  Proof 3.12.

Here we will present in detail the proof of the second item (the first item is
standard in that reduction and $\tau$ transitions are derived via standard
rules, see, e.g. the Harmony Lemma in [19]). Let $n$ be the number of
unguarded syntactical occurrences of Markovian delay prefixes inside $P$ (see
proof of Proposition 3.7 for a formal definition of $n$). We have that
$P\,\mathop{\longrightarrow}\limits\,\sigma$ for some $\sigma$ iff $n>0$ (the
“if” part is obvious, see proof of Proposition 3.7 for the “only if”).
Moreover we also obviously have that
$P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}$ for some
$\lambda$, $id$ and $P^{\prime}$ iff $n>0$.

Assumed $n>0$, we consider term $Q$ obtained from $P$ by performing a finite
number of successive substitutions of constants so that all constants occur
weakly guarded in $Q$ (always possible because recursion is guarded, see
Section 3). Notice that since $P\equiv Q$ we have
$Q\,\mathop{\longrightarrow}\limits\,\sigma$. Moreover it is immediate to
verify that for each $Q^{\prime}$ such that
$Q\,\mathop{\longrightarrow}\limits^{\lambda,id}\,Q^{\prime}$ there exists
$P^{\prime}$, with $P^{\prime}\equiv Q^{\prime}$, such that
$P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,P^{\prime}$; and viceversa.

Given distinguished names $q_{1}$, …, $q_{n}$, let $Q^{\prime}$ and rates
$\lambda_{i}$, $1\leq i\leq n$, with $Q^{\prime}$ including a unique free
unguarded syntactical occurrence of each $(q_{i})$ $\forall i,1\leq i\leq n$,
be such that $Q^{\prime}\\{\lambda_{i}/q_{i}\mid 1\leq i\leq n\\}=Q$. We have
that $Q\equiv(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime}$ (by extruding stochastic binders up
to the top level). Moreover $\forall h,1\leq h\leq n$, let $Q_{h}$ be
$Q^{\prime}\\{\lambda_{i}/q_{i}\mid 1\leq i\leq n\wedge i\neq h\\}$. We have
that $Q\equiv(\nu q_{h}\rightarrow\\!\lambda_{h})Q_{h}$ (by extruding the
stochastic binder $q_{h}$ up to the top level).

We now resort to classical correspondence of transitions between reduction and
labeled semantics. We have:
$Q_{h}\,\mathop{\longrightarrow}\limits^{q_{h}}\,Q^{\prime}_{h}$ iff
$Q\,\mathop{\longrightarrow}\limits^{\lambda_{h},id_{h}}\,Q^{\prime\prime}_{h}$
with $Q^{\prime\prime}_{h}\\!\equiv Q^{\prime}_{h}$. This is proved in a
completely analogous way as for the Harmony Lemma in [19], since, both unbound
$(q_{h})$ prefixes for the reduction semantics in this paper and $(\lambda)$
for the labeled semantics in this paper have the same behavior as $\tau$
prefixes for standard reduction and labeled semantics (they are just
“consumed” in the target state with no other effects).

Considered $Q^{\prime}$ we have that
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,Q^{\prime\prime\prime}_{h}$
with $Q^{\prime}_{h}\equiv(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime\prime\prime}_{h}$ (see proof of
Proposition 3.7 ), hence $\sigma=\\{\\!|\,(\lambda_{1},[(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime\prime\prime}_{1}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{n},[(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime\prime\prime}_{n}]_{\equiv})\,|\\!\\}$.
Thus, considered the set $I$ of the indexes $h$, with $1\leq h\leq n$, such
that $[(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime\prime\prime}_{h}]_{\equiv}=[P^{\prime}]_{\equiv}$
we have
$\sum_{(\lambda,[P^{\prime}]_{\equiv})\in\sigma}\lambda\cdot\mu_{\sigma}(\lambda,[P^{\prime}]_{\equiv})=\sum_{h\in
I}\lambda_{h}$. Moreover $I$ is also the set of indexes $h$ such that
$Q^{\prime\prime}_{h}\equiv P^{\prime}$, because
$Q^{\prime\prime}_{h}\equiv(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime\prime\prime}_{h}$. Therefore, since
$h\neq h^{\prime}$ implies $id_{h}\neq id_{h^{\prime}}$, we also have
$\sum_{P\,\mathop{\longrightarrow}\limits^{\lambda,id}\,\equiv
P^{\prime}}\lambda=\sum_{Q\,\mathop{\longrightarrow}\limits^{\lambda,id}\,\equiv
P^{\prime}}\lambda=\sum_{h\in I}\lambda_{h}$.

##  4 Conclusion

We start by considering (other) related work. As already mentioned this paper
is based on a (quite dated) technical report [2] where the idea of stochastic
names and stochastic binders has been introduced, but applied to a slightly
more complicate Markovian Process Algebra with respect to the one presented
here. In particular, while here we consider a process algebra where Markovian
delays and standard actions are separated prefixes (by following the simple
approach of [13]), in [2] we apply our technique to a process algebra where
Markovian rates are assigned to standard actions, which become “durational”
actions (as in [14, 18, 1]). Such Markovian process algebras are slightly more
complex in that the problem of calculating the rate of a synchronized action
(out of the rate of the synchronizing actions and the so-called apparent
rates, that is the total rate of the actions of the same type as the
synchronizing ones that are collectively performable by one of the processes
involved in the synchronization) come into play. The particular way in which
such rates are calculated strictly depends on a fixed structure for the syntax
tree for the parallel operators in the term (calculating the rates of the
synchronizations performable at a certain syntactical level, for instance in
$P\,|\,Q$, from the rates of the transitions performable at lower levels in
$P$ and $Q$) and therefore is not compatible with a semantics in reduction
style. This does not mean that there are no meaningful ways for defining rates
of synchronized actions in reduction semantics (see [2] and future work
below), but different calculations of apparent rates must be adopted that make
parallel composition associative [2, 9], thus yielding different values for
the rates. The more simplified setting adopted in this paper, instead, allowed
us to provide a theorem of consistency with the labeled operational semantics
and to show our approach based on stochastic names and stochastic binders, in
its essence, to be correct. We also would like to mention the approach in the
recently appeared paper [6]. Even if the version of Stochastic $\pi-$calculus
presented in [6] considers a congruence relation on terms, it defines
semantics via a labeled operational semantics (and not semantics in reduction
style), thus not exploiting congruence while inferring transitions (which, for
instance, would allow terms to be synchronized to get next to each other and
then produce a reduction). In particular [6] deals with multiplicity following
an approach like that of [7]. It is also worth noting that in [6] binders that
are very similar to the stochastic binders in this paper (and in [2]) are
used, but for a different aim. Here rate values inside binders are used to
associate a numerical value to a name representing symbolically a duration for
the aim of distinguishing multiple transitions (with the same rate). In [6],
where multiplicity is dealt with as in [7], they are used instead to associate
rates directly to action names in order to be able to express a novel feature:
the ability to pass around actions with a bound name but with an explicit
associated rate value. The similarity in the binder representation would maybe
make it possible to apply the technique in this paper to produce a reduction
semantics for the expressive algebra in [6] in an overall harmonic approach.

As a final remark, we would like to observe that the approach introduced in
this paper, that allows us to independently identify each Markovian delay
without introducing an explicit identification mechanism (but by exploiting
extrusion and stochastic binders) is applicable also in the case of generally
distributed durations where the identification mechanism is necessary to
generate clock names (to uniquely relate start of delays with termination of
delays), see, for instance, [4, 3]. In this case the generally distributed
delays would be considered as stochastic binders assigning a general
distribution $f$ and immediately binding a delay start prefix followed by a
delay termination prefix, both decorated with the same stochastic name that is
bound by the binder.

As future work we consider the application of the technique in this paper to
produce semantics in reduction style in Markovian process algebra with rates
associated to actions (using, for instance, the mass action law as in [2] so
to have associativity of parallel, see [9], or the generative/reactive
approach of [1], that can be adopted in the context of an associative parallel
and whose rate calculation is compatible with inferring transitions via a
congruence relation) and in process algebra with probabilistic choices and
generally distributed durations [4, 3].

#### Acknowledgements

We would like to thank Luca Cardelli and Davide Sangiorgi for the fruitful
comments and suggestions.

## References

  * [1] M. Bernardo, M. Bravetti “Performance measure sensitive congruences for Mar-kovian process algebras”, in Theoretical Computer Science, 290(1):117-160, 2003
  * [2] M. Bravetti “Stochastic Semantics in the Presence of Structural Congruence: Reduction Semantics for Stochastic Pi-Calculus”, Technical Report UBLCS-2008-16 of University of Bologna, Department of Computer Science. Available at `http://www.informatica.unibo.it/it/ricerca/technical-report/2008`
  * [3] M. Bravetti, P. R. D’Argenio “Tutte le Algebre Insieme: Concepts, Discussions and Relations of Stochastic Process Algebras with General Distributions.”, in Validation of Stochastic Systems, LNCS 2925: 44-88, 2004
  * [4] M. Bravetti, R. Gorrieri, “The Theory of Interactive Generalized Semi-Markov Processes”, in Theoretical Computer Science, 282:5-32, 2002
  * [5] M. Bravetti, H. Hermanns, J.-P. Katoen, “YMCA: - Why Markov Chain Algebra?”, Electr. Notes Theor. Comput. Sci. 162: 107-112, 2006
  * [6] L. Cardelli, R. Mardare “Stochastic Pi-calculus Revisited”, proc. of 10th Int. Coll. on Theoretical Aspects of Computing (ICTAC 2013), LNCS 8049: 1-21, 2013
  * [7] R. De Nicola, D. Latella, M. Loreti, M. Massink “A Uniform Definition of Stochastic Process Calculi”, ACM Computing Surveys 46(1): 5, 2013
  * [8] Josee Desharnais, Abbas Edalat, Prakash Panangaden: “Bisimulation for Labelled Markov Processes”, Information and Computation 179(2): 163-193, 2002
  * [9] B. Klin, V. Sassone, “Structural operational semantics for stochastic and weighted transition systems”, in Information and Computation, 227:58-83, 2013
  * [10] M. Giry, “A categorical approach to probability theory”, in Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, 915:68-85, 1982
  * [11] N. Götz, U. Herzog, M. Rettelbach, “TIPP - A Stochastic Process Algebra”, proc. of 1st workshop on Process Algebras and Perf. Modeling (PAPM ’93): 31-36, 1994
  * [12] J.F. Groote, “Transition system specifications with negative premises”, in Theoretical Computer Science, 118(2):263-299, 1993
  * [13] H. Hermanns, “Interactive Markov Chains: The quest for quantified quality”, Springer-Verlag Berlin, 2002
  * [14] J. Hillston, “A Compositional Approach to Performance Modelling”, Cambridge University Press, 1996
  * [15] E. B. Johnsen and O. Owe, “An asynchronous communication model for distributed concurrent objects”, in Software and System Modeling, 6(1):35-58, 2007
  * [16] R. Milner, “Communicating and mobile systems - the Pi-calculus”, Cambridge University Press, 1999
  * [17] R. Milner, J. Parrow, D. Walker “A Calculus of Mobile Processes I and II”, Information and Computation 100(1): 1-77, 1992
  * [18] C. Priami, “Stochastic $\pi$-Calculus”, in Computer Journal 38(6):578-589, 1995
  * [19] D. Sangiorgi, D. Walker, “The pi-calculus: a Theory of Mobile Processes”, Cambridge University Press , 2001
  * [20] R. Segala, N. A. Lynch: “Probabilistic Simulations for Probabilistic Processes”, Nordic Journal of Computing 2(2): 250-273, 1995
  * [21] W.J. Stewart, “Introduction to the Numerical Solution of Markov Chains”, Princeton University Press, 1994
  * [22] Erik P. de Vink, Jan J. M. M. Rutten, “Bisimulation for Probabilistic Transition Systems, A Coalgebraic Approach”, Theoretical Computer Science 221(1-2): 271-293, 1999

##  Appendix A Proof of Proposition 8

Let $P\in{\cal P}$ and $P\,\mathop{\longrightarrow}\limits\,\sigma$. We have
$P\,\mathop{\longrightarrow}\limits\,\sigma^{\prime}$ implies
$\sigma=\sigma^{\prime}$.

######  Proof A.1.

Let $n$ be the number of unguarded syntactical occurrences of Markovian delay
prefixes inside $P$. Formally $n$ is evaluated as follows: $P^{\prime}$ is
obtained from $P$ by performing a finite number of successive substitutions of
constants so that all constants occur weakly guarded in $P^{\prime}$ (always
possible because recursion is guarded, see Section 3); $n$ is the number of
Markovian delay prefixes that occur in $P^{\prime}$ not in the scope of a
prefix operator. Since $P\,\mathop{\longrightarrow}\limits\,\sigma$ we must
have $n\geq 1$.

We first show, by induction on $k$, with $0\leq k\leq n$ ($k=0$ being the base
case), that the following statement holds true. Let $q_{1}$, …, $q_{k}$ be any
set of distinguished names. There exists $Q$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu q_{k}\rightarrow\\!\lambda_{k})Q$
(consider $P\equiv Q$ in the case $k=0$) and $\forall i,1\leq h\leq k\ldotp
Q\,\mathop{\longrightarrow}\limits^{q_{h}}\,$. Moreover for any such $Q$, we
have, supposing $\forall h,1\leq h\leq k\ldotp
Q\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$, that:

  * •

$Q$ includes a unique free unguarded syntactical occurrence of $(q_{h})$
$\forall h,1\leq h\leq k$ (this reduces to true for the base case $k=0$). This
assert (and all other properties of $Q$ stated above) derives directly from
the induction hypothesis (case $k-1$): it is shown by extruding $(\nu
q_{k}\rightarrow\\!\lambda_{k})$ via congruence laws up to the top-level of a
term $Q^{\prime}$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{k-1}\rightarrow\\!\lambda_{k-1})Q^{\prime}$ . Moreover, since congruence
laws preserve uniqueness of free $(q)$ prefixes, we have that $Q$ includes a
unique free unguarded syntactical occurrence of $(q_{k})$ and unique free
unguarded syntactical occurrences of $(q_{h})$ $\forall h,1\leq h\leq k-1$.

  * •

If $k<n$, for any $q$ distinguished from $q_{h}$ $\forall h,1\leq h\leq k$,
there exist $Q^{\prime},\lambda$ such that $Q\equiv(\nu
q\rightarrow\\!\lambda)Q^{\prime}$ and
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q}\,$, i.e.
$Q\,\mathop{\longrightarrow}\limits\,\sigma$. This is shown by extruding $(\nu
q\rightarrow\\!\lambda)$ via congruence laws up to the top-level of $Q$.
Moreover, for any such $Q^{\prime},\lambda$ we have that $Q^{\prime}$ includes
a unique free unguarded syntactical occurrence of $(q)$ and unique free
unguarded syntactical occurrences of $(q_{h})$ $\forall h,1\leq h\leq k$ and,
supposing $\forall h,1\leq h\leq k\ldotp
Q^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime\prime}_{h}$, we
have that $(\nu q\rightarrow\\!\lambda)P^{\prime\prime}_{h}\equiv
P^{\prime}_{h}$. This is shown as follows. Since, as already observed, $Q$
includes a unique free unguarded syntactical occurrence of $(q_{h})$ $\forall
h,1\leq h\leq k$ and $Q\equiv(\nu q\rightarrow\\!\lambda)Q^{\prime}$, we have
the uniqueness results (due to the fact, similarly as in the previous item,
that congruence laws preserve uniqueness) and, consequently, that $(\nu
q\rightarrow\\!\lambda)Q^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,(\nu
q\rightarrow\\!\lambda)P^{\prime\prime}_{h}$ with $(\nu
q\rightarrow\\!\lambda)P^{\prime\prime}_{h}\equiv P^{\prime}_{h}$.

  * •

If, instead, $k=n$ there is no $Q^{\prime},q,\lambda$ such that $Q\equiv(\nu
q\rightarrow\\!\lambda)Q^{\prime}$ and
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q}\,$, i.e.
$Q\not\,\mathop{\longrightarrow}\limits\,\sigma$. This because, due again to
the fact that congruence laws preserve uniqueness, the only occurrences of
$(q)$ prefixes in $Q$ are the unique free unguarded syntactical occurrences of
$(q_{h})$ $\forall h,1\leq h\leq n$ and in $Q$ there is no $\lambda$ such that
$Q$ includes an unguarded syntactical occurrence of $(\lambda)$.

Considering case $k=n$ of the above, we have that, given distinguished names
$q_{1}$, …, $q_{n}$, there exists $P^{\prime}$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}$ and $\forall i,1\leq h\leq n\ldotp
P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,$. Moreover for any such
$P^{\prime}$ we have that $P^{\prime}$ includes a unique free unguarded
syntactical occurrence of $(q_{i})$ $\forall i,1\leq i\leq n$.

In the following we will show, by induction on the length of inference chains,
that inferring a $\sigma$ transition from $P$ (where $q_{1}$ is the name of
the binder used to infer $\sigma$ in the last rule used in the inference chain
and so on and so forth in depth until $q_{n}$ where the chain of binder
applications begins with the (Sto2) rule) entails singling out one of such
terms $P^{\prime}$ and that, supposing $\forall h,1\leq h\leq n\ldotp
P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$, the
inferred $\sigma$ is such that

$\sigma=\\{\\!|\,(\lambda_{1},[(\nu q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{1}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{n},[(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{n}]_{\equiv})\,|\\!\\}$

Notice that this value does not depend on the choice of the $P^{\prime}_{h}$
such that
$P^{\prime}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$ in that,
since $P^{\prime}$ includes a unique free unguarded syntactical occurrence of
$(q_{h})$, possible terms $P^{\prime}_{h}$ are all related by $\equiv$ (and,
in general, $P\equiv Q$ implies $(\nu q\rightarrow\\!\lambda)P\equiv(\nu
q\rightarrow\\!\lambda)Q$ for any $P,Q,q$ and $\lambda$).

From this fact we can derive that the $\sigma$ inferred is the same for any
possible inference chain of a $\sigma$ transition from $P$, i.e. that no
matter the order in which delay prefixes are bound, the same rate distribution
is obtained. This because, considered $\sigma^{\prime}$ derived with another
inference chain, such an inference would determine a $P^{\prime\prime}$ such
that $P\equiv(\nu q^{\prime}_{1}\rightarrow\\!\lambda^{\prime}_{1})\dots(\nu
q^{\prime}_{n}\rightarrow\\!\lambda^{\prime}_{n})P^{\prime\prime}$ and
$\forall i,1\leq i\leq n\ldotp
P^{\prime\prime}\,\mathop{\longrightarrow}\limits^{q^{\prime}_{i}}\,$. It is
immediate to verify that there exists a permutation $k_{i}$, with $1\leq i\leq
n$, such that, by alpha-conversion we can write $(\nu
q^{\prime}_{1}\rightarrow\\!\lambda^{\prime}_{1})\dots(\nu
q^{\prime}_{n}\rightarrow\\!\lambda^{\prime}_{n})P^{\prime\prime}$ as $(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime\prime}$ where for
$P^{\prime\prime\prime}$ it holds $P^{\prime\prime\prime}\equiv P^{\prime}$.
Thus $\sigma^{\prime}=\\{\\!|\,(\lambda_{k_{1}},(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime}_{k_{1}}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{k_{n}},[(\nu
q_{k_{1}}\rightarrow\\!\lambda_{k_{1}})\dots(\nu
q_{k_{n}}\rightarrow\\!\lambda_{k_{n}})P^{\prime\prime}_{k_{n}}]_{\equiv})\,|\\!\\}$,
where $\forall i,1\leq i\leq n$ we have $P^{\prime\prime}_{k_{i}}\equiv
P^{\prime}_{k_{i}}$ because $P^{\prime}$ includes a unique free unguarded
syntactical occurrence of $(q_{i})$ $\forall i,1\leq i\leq n$.
$\sigma^{\prime}=\sigma$ by reordering of the binders, of the members of the
multiset union and from the fact that $P\equiv Q$ implies $(\nu
q\rightarrow\\!\lambda)P\equiv(\nu q\rightarrow\\!\lambda)Q$ for any $P,Q,q$
and $\lambda$.

Let us now analyze the structure of the inference chain of a $\sigma$
transition from $P$ by considering an inductive argument (starting from
$k=0$). Given $k$ such that $0\leq k\leq n-1$, the structure of any inference
sequence of any $\sigma$ transition of $Q$ such that $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu q_{k}\rightarrow\\!\lambda_{k})Q$
(consider $P\equiv Q$ in the case $k=0$) and $\forall h,1\leq h\leq k\ldotp
Q\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$ must be as
follows. Apart from applications of the rule (StoCong), that can be used to
get, from $Q\,\mathop{\longrightarrow}\limits\,\sigma$, $(\nu
q_{k+1}\rightarrow\\!\lambda_{k+1})Q^{\prime}\,\mathop{\longrightarrow}\limits\,\sigma$,
with $Q^{\prime}$ such that $Q\equiv(\nu
q_{k+1}\rightarrow\\!\lambda_{k+1})Q^{\prime}$ and
$Q^{\prime}\,\mathop{\longrightarrow}\limits^{q_{k+1}}\,P^{\prime}_{k+1}$ (we
have already shown such $Q^{\prime}$ to always exist for $k\leq n-1$) the last
rule used must be:

  * •

(Sto2) if $k=n-1$, yielding directly $(\nu
q_{n}\rightarrow\\!\lambda_{n})Q^{\prime}\,\mathop{\longrightarrow}\limits\,\sigma$.
This because, as we have shown already,
$Q^{\prime}\not\,\mathop{\longrightarrow}\limits\,\sigma$. The inference
sequence is therefore terminated (as far as stochastic binder application is
concerned).

  * •

(Sto1) if $k<n-1$, yielding $(\nu
q_{k+1}\rightarrow\\!\lambda_{k+1})Q^{\prime}\,\mathop{\longrightarrow}\limits^{\sigma}\,$.
This because, as we have shown already,
$Q^{\prime}\,\mathop{\longrightarrow}\limits\,\sigma$. The inference sequence
is therefore continued by the inference of a $\sigma^{\prime}$ transition of
term $Q^{\prime}$.

Hence, by repeatedly applying the statement above ($n$ times starting from
$k=0$) we have that, for any $\sigma$ transition of $P$ there exist
$Q_{1},\dots,Q_{n}$, with $P\equiv(\nu
q_{1}\rightarrow\\!\lambda_{1})\dots(\nu q_{k}\rightarrow\\!\lambda_{k})Q_{k}$
for $1\leq k\leq n$, such that the inference sequence of the $\sigma$
transition must include $n-1$ usages of the (Sto1) rule yielding $(\nu
q_{1}\rightarrow\\!\lambda_{1})Q_{1}\,\mathop{\longrightarrow}\limits\,\sigma_{1}$,
…, $(\nu
q_{n-1}\rightarrow\\!\lambda_{n-1})Q_{n-1}\,\mathop{\longrightarrow}\limits\,\sigma_{n-1}$
transitions, with $\sigma_{1}=\sigma$, followed by one usage of the (Sto2)
rule yielding $(\nu
q_{n}\rightarrow\\!\lambda_{n})Q_{n}\,\mathop{\longrightarrow}\limits\,\sigma_{n}$
transition. We have, supposing $\forall h,1\leq h\leq n\ldotp
Q_{n}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime}_{h}$,
$\sigma_{k}=\\{\\!|\,(\lambda_{k},[(\nu
q_{k}\rightarrow\\!\lambda_{k})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{k}]_{\equiv})\,|\\!\\}\cup\dots\cup\\{\\!|\,(\lambda_{n},[(\nu
q_{k}\rightarrow\\!\lambda_{k})\dots(\nu
q_{n}\rightarrow\\!\lambda_{n})P^{\prime}_{n}]_{\equiv})\,|\\!\\}$. This is
shown by induction on the length of the inference sequence (in terms of number
of applications of (Sto1)/(Sto2) rules). The base case is for $k=n$
(application of the (Sto2) rule). Then we show it holds for $k$ supposing that
it holds for $k+1$ (application of the (Sto1) rule). In the inductive case we
exploit the fact, we showed before, that, given $P^{\prime\prime\prime}_{h}$
such that
$Q_{k+1}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime\prime\prime}_{h}$,
we have, for $P^{\prime\prime}_{h}$ with
$Q_{k}\,\mathop{\longrightarrow}\limits^{q_{h}}\,P^{\prime\prime}_{h}$, that
$(\nu q_{k+1}\rightarrow\\!\lambda_{k+1})P^{\prime\prime\prime}_{h}\equiv
P^{\prime\prime}_{h}$.