$\mathrm{var}(u_{i,h})\subseteq\mathrm{rhs}(\mathcal{H}_{i})$;

       * •

$\sigma^{\prime}$ agrees with $\sigma_{i}$ on all variables in
$\mathrm{rhs}(\mathcal{H}_{i})$, for all $i\in I$;

       * •

$\mathrm{rhs}(\mathcal{H})=\bigcup_{i\in I}\mathrm{rhs}(\mathcal{H}_{i})$.

Therefore, we have that $\sigma^{\prime}(u_{i,h})=\sigma_{i}(u_{i,h})=t_{i,h}$
for each $h\in H_{i},i\in I$. Hence, we can conclude that
$\sigma^{\prime}(u)=t_{\mathfrak{f}(u)}$ for each $u\in\\{t_{i,h}\mid h\in
H_{i},i\in I\\}$.

($\Leftarrow$) We aim to show that
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in
M\\}$. To this aim it is enough to show that
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\Theta)\xrightarrow{\,{q_{m}}\,}\sigma^{\prime}(u_{m})\mid
m\in M\\}$ which, since the closed terms $t_{m}$ are pairwise distinct by the
hypothesis, by the choice of $\sigma^{\prime}$ is equivalent to
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in
M\\}$.

Accordingly to Definition 15, let $r_{\textsf{D}}$ and $\sigma_{0}$ be resp.
the $\Sigma$-distribution rule and the substitution from which
$\rho^{\textsf{D}}$ is built, namely let $r_{\textsf{D}}$ be of the form

$\frac{\displaystyle\bigcup_{i\in}\\{\vartheta_{i}\xrightarrow{\,{q_{i,j}}\,}x_{i,j}\mid
j\in J_{i}\\}}{\displaystyle\Big{\\{}\sum_{i\in
I}p_{i}\vartheta_{i}\xrightarrow{\,{q_{x}}\,}x\;\Big{|}\;x\in\\{x_{i,j}\mid
i\in I\wedge j\in J_{i}\\}\text{ and }q_{x}=\sum_{i\in I,j\in J_{i}\text{ s.t.
}x_{i,j}=x}p_{i}\cdot q_{i,j}\Big{\\}}}$

as in Definition 10.3 and $\sigma_{0}$ be such that
$\sigma_{0}(r_{\textsf{D}})$ is of the form

$\frac{\displaystyle\bigcup_{i\in}\\{\Theta_{i}\xrightarrow{\,{q_{i,h}}\,}u_{i,h}\mid
h\in H_{i}\\}}{\displaystyle\Big{\\{}\sum_{i\in
I}p_{i}\Theta_{i}\xrightarrow{\,{q_{m}}\,}u_{m}\;\Big{|}\;u_{m}\in\\{u_{i,h}\mid
i\in I\wedge h\in H_{i}\\}\text{ and }q_{m}=\sum_{i\in I,h\in H_{i}\text{ s.t.
}u_{i,h}=u_{m}}p_{i}\cdot q_{i,h}\Big{\\}}}$

(see Definition 12.3). Then $\rho^{\textsf{D}}$ is of the form

$\rho^{\textsf{D}}=\frac{\displaystyle\bigcup_{i\in
I}\mathcal{H}_{i}}{\displaystyle\\{\sum_{i\in
I}p_{i}\Theta_{i}\xrightarrow{\,{q_{m}}\,}u_{m}\mid m\in M\\}}$

where for each $i\in I$ we have that:

     * •

Either $\sigma_{0}(\vartheta_{i})=\Theta_{i}$ is a variable or a Dirac
distribution and
$\mathcal{H}_{i}=\\{\Theta_{i}\xrightarrow{\,{q_{i},h}\,}u_{i,h}\mid h\in
H_{i}\\}$. Hence from $D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$ we can
immediately infer that
$D_{\Sigma}\vdash\sigma^{\prime}(\\{\Theta_{i}\xrightarrow{\,{q_{i},h}\,}u_{i,h}\mid
h\in H_{i}\\})$.

     * •

Or there is a $\Sigma$-distribution ruloid
$\rho^{\textsf{D}}_{i}=\frac{\displaystyle\mathcal{H}_{i}}{\displaystyle\\{\sigma_{0}(\vartheta)\xrightarrow{\,{q_{i,h}}\,}u_{i,h}\mid
h\in H_{i}\\}}$. Since $D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$ implies
$D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H}_{i})$, by structural induction on
$\Theta_{i}$ we can infer that
$D_{\Sigma}\vdash\sigma^{\prime}(\\{\Theta_{i}\xrightarrow{\,{q_{i,h}}\,}u_{i,h}\mid
h\in H_{i}\\})$.

Hence, we have obtained that the closed substitution instances wrt.
$\sigma^{\prime}\circ\sigma_{0}$ of the premises of $r_{\textsf{D}}$ are
provable from $D_{\Sigma}$ and therefore we can infer that there is a proof
from $D_{\Sigma}$ of
$\\{\sigma^{\prime}(\Theta)\xrightarrow{\,{q_{m}}\,}\sigma^{\prime}(u_{m})\mid
m\in M\\}$. By the choice of $\sigma^{\prime}$, we can conclude that
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in
M\\}$.

∎

###### Example

Consider the distribution term
$\Theta=\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)$ and the closed substitution
$\sigma$ with
$\sigma(\Theta)=\frac{2}{5}(\frac{1}{4}\delta_{t_{1}}+\frac{3}{4}\delta_{t_{2}})+\frac{3}{5}\big{(}(\frac{1}{3}\delta_{t_{3}}+\frac{2}{3}\delta_{t_{4}})\mid\delta_{t_{5}}\big{)}$.
Notice that $\sigma(\Theta)$ is the source term of the distribution over terms
$L$ in Example 3.3. Thus, we know that

$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{1/10}\,}t_{1},\;\sigma(\Theta)\xrightarrow{\,{3/10}\,}t_{2},\;\sigma(\Theta)\xrightarrow{\,{1/5}\,}t_{3}|t_{5},\;\sigma(\Theta)\xrightarrow{\,{2/5}\,}t_{4}|t_{5}\\}.$

Consider the $\Sigma$-distribution ruloid $\rho^{\textsf{D}}$ for $\Theta$
given in Example 4.2

$\frac{\displaystyle\\{\mu\xrightarrow{\,{1/4}\,}x_{1}\quad\mu\xrightarrow{\,{3/4}\,}x_{2}\\}\qquad\\{\nu\xrightarrow{\,{1/3}\,}y_{1},\quad\nu\xrightarrow{\,{2/3}\,}y_{2}\\}\qquad\\{\upsilon\xrightarrow{\,{1}\,}z\\}}{\displaystyle\Big{\\{}\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)\xrightarrow{\,{\frac{1}{10}}\,}x_{1},\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)\xrightarrow{\,{\frac{3}{10}}\,}x_{2},\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)\xrightarrow{\,{\frac{1}{5}}\,}y_{1}|z,\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)\xrightarrow{\,{\frac{2}{5}}\,}y_{2}|z\Big{\\}}}.$

We want to exhibit a proper closed substitution $\sigma^{\prime}$ such that
$\rho^{\textsf{D}}$ and $\sigma^{\prime}$ satisfy Theorem 5 wrt.
$\sigma(\Theta)$. Let

$\begin{array}[]{c}\sigma^{\prime}(x_{1})=t_{1}\qquad\sigma^{\prime}(x_{2})=t_{2}\qquad\sigma^{\prime}(y_{1})=t_{3}\qquad\sigma^{\prime}(y_{2})=t_{4}\qquad\sigma^{\prime}(z)=t_{5}\\\\[3.01385pt]
\sigma^{\prime}(\mu)=\frac{1}{4}\delta_{t_{1}}+\frac{3}{4}\delta_{t_{2}}\qquad\qquad\sigma^{\prime}(\nu)=\frac{1}{3}\delta_{t_{3}}+\frac{2}{3}\delta_{t_{4}}\qquad\qquad\sigma^{\prime}(\upsilon)=\delta_{t_{5}}.\end{array}$

Then we have

$\sigma^{\prime}(\Theta)=\frac{2}{5}\sigma^{\prime}(\mu)+\frac{3}{5}\sigma^{\prime}(\nu|\upsilon)=\frac{2}{5}(\frac{1}{4}\delta_{t_{1}}+\frac{3}{4}\delta_{t_{2}})+\frac{3}{5}\Big{(}(\frac{1}{3}\delta_{t_{3}}+\frac{2}{3}\delta_{t_{4}})\,|\,\delta_{t_{5}}\Big{)}.$

Moreover

$\sigma^{\prime}(y_{1}|z)=t_{3}|t_{5}\qquad\qquad\sigma^{\prime}(y_{2}|z)=t_{4}|t_{5}$

thus giving that
$\sigma^{\prime}(\mathrm{trg}(\rho^{\textsf{D}}))=\mathrm{rhs}(L)$. Finally,
we remark that

  * •

the proof presented for
$\\{\sigma(\mu_{2})\xrightarrow{\,{1/4}\,}t_{1},\,\sigma(\mu_{2})\xrightarrow{\,{3/4}\,}t_{2}\\}$
with $\sigma(\mu_{2})=\frac{1}{4}\delta_{t_{1}}+\frac{3}{4}\delta_{t_{2}}$ in
Example 3.3 gives us
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\mu)\xrightarrow{\,{1/4}\,}t_{1},\,\sigma^{\prime}(\mu)\xrightarrow{\,{3/4}\,}t_{2}\\}$;

  * •

the proof presented for
$\\{\sigma(\mu_{1})\xrightarrow{\,{1/3}\,}t_{3},\,\sigma(\mu_{1})\xrightarrow{\,{2/3}\,}t_{4}\\}$
with $\sigma(\mu_{1})=\frac{1}{3}\delta_{t_{3}}+\frac{2}{3}\delta_{t_{4}}$ in
Example 3.3 gives us
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\nu)\xrightarrow{\,{1/3}\,}t_{3},\,\sigma^{\prime}(\nu)\xrightarrow{\,{2/3}\,}t_{4}\\}$;

  * •

the proof presented for $\\{\sigma(\nu_{1})\xrightarrow{\,{1}\,}t_{5}\\}$ with
$\sigma(\nu_{1})=\delta_{t_{5}}$ in Example 3.3 gives us
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\upsilon)\xrightarrow{\,{1}\,}t_{5}\\}$.

We have therefore obtained that
$D_{\Sigma}\vdash\sigma^{\prime}(\mathrm{prem}(\rho^{\textsf{D}}))$ and thus
that $\rho^{\textsf{D}}$ and $\sigma^{\prime}$ satisfy Theorem 5 wrt.
$\sigma(\Theta)$.

###  4.3. Related work

The only paper dealing with ruloids for specifications of probabilistic
process calculi is [GF12]. As previously outlined, [GF12] deals with reactive
transition systems, which are less expressive than PTSs as they do not admit
internal nondeterminism. Transitions are of the form
$t\xrightarrow{\,{a,p}\,}t^{\prime}$, denoting that $t$ evolves by $a$ to
$t^{\prime}$ with probability $p$. Informally, our $P$-ruloids generalize
those in [GF12] in the same way PTSSs generalize reactive systems. In fact, to
deal with the quadruple $t\xrightarrow{\,{a,p}\,}t^{\prime}$, ruloids in
[GF12] are defined by keeping track of rules and ruloids used in their
construction, in order to assign a proper probability weight to their
conclusion. In detail, to guarantee the property of semi-stochasticity, i.e.
the sum of the probabilities of all transitions for an action from a term is
either $0$ or $1$, a partitioning over ruloids is needed in [GF12]: given a
term $t$ the ruloids in the partition for $t$ related to action $a$ allow one
to derive $a$-labeled transitions from $t$ whose total probability is $1$. To
do so, one also has to constantly keep track of the rules and ruloids used in
the construction of the ruloids in a partition, because the exact probability
weight of a transition depends on this construction. An analogous technicality
was already necessary in the SOS transition rules in [LT09], on which [GF12]
builds.

Here we do not need this technicality, since probabilities are directly
managed by $\Sigma$-distribution ruloids and we can use $P$-ruloids to derive
the transitions leading to probability distributions. More precisely, we
should say that given a term $t$, all ruloids in one partition for $t$ of
[GF12] are captured by one of our $P$-ruloids and one $\Sigma$-distribution
ruloid. The $P$-ruloid captures all the requirements that the subterms of $t$
must satisfy to derive the transition to the desired probability distribution
over terms. The proper probability weights are then automatically assigned to
terms by the $\Sigma$-distribution ruloid, without the need of keeping track
of all the rules and ruloids used in the construction.

##  5\. The decomposition method

In this section we present our method for decomposing formulae in
$\operatorname{\mathcal{L}}$,
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$. To this purpose we exploit
the two classes of ruloids introduced in Section 4. In fact, the idea behind
the decomposition of state (resp. distribution) formulae is to establish which
properties the closed substitution instances of the variables occurring in a
(distribution) term must satisfy to guarantee that the closed substitution
instance of that (distribution) term satisfies the chosen state (resp.
distribution) formula. Thus, since ($\Sigma$-distribution) ruloids derive the
behavior of a (distribution) term directly from the behavior of the variables
occurring in it, the decomposition method is firmly related to them.

Formally, starting from the class $\operatorname{\mathcal{L}}$, the
decomposition of state formulae follows those in [BFvG04, FvG16, FvGL17,
FvGdW06, FvGdW12, GF12] and consists in assigning to each term
$t\in\mathbb{T}(\Sigma)$ and formula
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$, a set of
functions
$\xi\colon\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$,
called _decomposition mappings_ , assigning to each variable $x$ in $t$ a
proper formula in $\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$
such that for any closed substitution $\sigma$ it holds that
$\sigma(t)\models\varphi$ iff $\sigma(x)\models\xi(x)$ for each
$x\in\mathrm{var}(t)$ (Theorem 6). Each mapping $\xi$ will be defined on a
$P$-ruloid having $t$ as source, $P$ being the considered PGSOS-PTSS.
Similarly, the decomposition of distribution formulae consists in assigning to
each distribution term $\Theta\in\mathbb{DT}(\Sigma)$ and distribution formula
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$ a set of
decomposition mappings
$\eta\colon\mathcal{V}\to\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}\cup\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$
such that for any closed substitution $\sigma$ we get that
$\sigma(\Theta)\models\psi$ iff $\sigma(\zeta)\models\eta(\zeta)$ for each
$\zeta\in\mathrm{var}(\Theta)$ (Theorem 6). Each mapping $\eta$ will be
defined on a $\Sigma$-distribution ruloid having $\Theta$ as source.

Then, as $\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$ are subclasses of
$\operatorname{\mathcal{L}}$, we will show how we can easily derive the
decomposition method for them from the one proposed for
$\operatorname{\mathcal{L}}$ (Theorem 7).

###  5.1. Decomposition of formulae in $\operatorname{\mathcal{L}}$

In this section we consider the logic $\operatorname{\mathcal{L}}$. First we
need to introduce the notion of matching for a distribution over terms and a
distribution formula, seen as a probability distribution over state formulae
[CGT16a, DD11].

######  Definition 16 (Matching).

Assume a distribution over terms
$L=\\{\Theta\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in M\\}$ and a distribution
formula $\psi=\bigoplus_{i\in
I}r_{i}\varphi_{i}\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$.
Then a _matching_ for $L$ and $\psi$ is a distribution over the product space
$\mathfrak{w}\in\Delta(\mathbb{T}(\Sigma)\times\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}})$
having $L$ and $\psi$ as left and right marginals respectively, that is
$\sum_{i\in I}\mathfrak{w}(t_{m},\varphi_{i})=q_{m}$ for all $m\in M$ and
$\sum_{m\in M}\mathfrak{w}(t_{m},\varphi_{i})=r_{i}$ for all $i\in I$. We
denote by $\mathfrak{W}(L,\psi)$ the set of all matchings for $L$ and $\psi$.

######  Definition 17 (Decomposition of formulae in
$\operatorname{\mathcal{L}}$).

Let $P=(\Sigma,\mathcal{A},R)$ be a PGSOS-PTSS and let $D_{\Sigma}$ be the
$\Sigma$-DS. We define the mappings

  * •

$\cdot^{-1}\colon\mathbb{T}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}\to{\mathcal{P}}(\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}))$,
and

  * •

$\cdot^{-1}\colon\mathbb{DT}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}\to{\mathcal{P}}(\mathcal{V}\to\operatorname{\mathcal{L}}))$

as follows. For each term $t\in\mathbb{T}(\Sigma)$ and state formula
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$,
$t^{-1}(\varphi)\in{\mathcal{P}}(\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}})$
is the set of _decomposition mappings_
$\xi\colon\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$
such that for any univariate term $t$ we have:

  1. (1)

$\xi\in t^{-1}(\top)$ iff $\xi(x)=\top$ for all $x\in\mathcal{V}\\!_{s}$;

  2. (2)

$\xi\in t^{-1}(\neg\varphi)$ iff there is a function $\mathfrak{f}\colon
t^{-1}(\varphi)\to\mathrm{var}(t)$ such that

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{\xi^{\prime}\in\mathfrak{f}^{-1}(x)}\neg\xi^{\prime}(x)&\text{if
}x\in\mathrm{var}(t)\\\ \top&\text{otherwise;}\end{cases}$

  3. (3)

$\xi\in t^{-1}(\bigwedge_{j\in J}\varphi_{j})$ iff there exist decomposition
mappings $\xi_{j}\in t^{-1}(\varphi_{j})$ for all $j\in J$ such that

$\xi(x)=\bigwedge_{j\in J}\xi_{j}(x)\text{ for all
}x\in\mathcal{V}\\!_{s}\text{;}$

  4. (4)

$\xi\in t^{-1}(\langle a\rangle\psi)$ iff there exist a $P$-ruloid
$\frac{\mathcal{H}}{t\xrightarrow{\,{a}\,}\Theta}$ and a decomposition mapping
$\eta\in\Theta^{-1}(\psi)$ such that:

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}}\langle
b\rangle\eta(\mu)\quad\wedge\quad\bigwedge_{x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
6.02777pt}}{\\!}\in\mathcal{H}}\neg\langle
c\rangle\top\quad\wedge\quad\eta(x)&\text{ if
}x\in\mathrm{var}(t)\\\\[6.45831pt] \top&\text{ otherwise;}\end{cases}$

  5. (5)

$\xi\in(\sigma(t))^{-1}(\varphi)$ for a non injective substitution
$\sigma\colon\mathrm{var}(t)\to\mathcal{V}\\!_{s}$ iff there is a
decomposition mapping $\xi^{\prime}\in t^{-1}(\varphi)$ such that

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{y\in\sigma^{-1}(x)}\xi^{\prime}(y)\quad&\text{
if }x\in\mathrm{var}(t)\\\ \top&\text{ otherwise.}\end{cases}$

Then, for each distribution term $\Theta\in\mathbb{DT}(\Sigma)$ and
distribution formula
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$,
$\Theta^{-1}(\psi)\in{\mathcal{P}}(\mathcal{V}\to\operatorname{\mathcal{L}})$
is the set of _decomposition mappings_
$\eta\colon\mathcal{V}\to\operatorname{\mathcal{L}}$ such that for any
univariate distribution term $\Theta$ we have:

  1. (6)

$\eta\in\Theta^{-1}(\bigoplus_{i\in I}r_{i}\varphi_{i})$ iff there are a
$\Sigma$-distribution ruloid
$\frac{\displaystyle\mathcal{H}}{\displaystyle\\{\Theta\xrightarrow{\,{q_{m}}\,}t_{m}\mid
m\in M\\}}$ and a matching
$\mathfrak{w}\in\mathfrak{W}(\\{\Theta\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in
M\\},\bigoplus_{i\in I}r_{i}\varphi_{i})$ such that for all $m\in M$ and $i\in
I$ there is a decomposition mapping $\xi_{m,i}$ with
$\begin{cases}\xi_{m,i}\in t_{m}^{-1}(\varphi_{i})&\text{if
}\mathfrak{w}(t_{m},\varphi_{i})>0\\\ \xi_{m,i}\in
t_{m}^{-1}(\top)&\text{otherwise}\end{cases}$ and we have

    1. (a)

for all $\mu\in\mathcal{V}\\!_{d}$,
$\eta(\mu)=\begin{cases}\displaystyle\bigoplus_{\mu\xrightarrow{\,{q_{j}}\,}x_{j}\in\mathcal{H}}q_{j}\bigwedge_{i\in
I\atop m\in M}\xi_{m,i}(x_{j})&\text{ if
}\mu\in\mathrm{var}(\Theta)\\\\[4.30554pt] 1\top&\text{
otherwise}\\\\[8.61108pt] \end{cases}$

    2. (b)

for all $x\in\mathcal{V}\\!_{s}$,
$\eta(x)=\begin{cases}\displaystyle\bigwedge_{i\in I\atop m\in
M}\xi_{m,i}(x)&\text{ if }x\in\mathrm{var}(\Theta)\\\\[4.30554pt] \top&\text{
otherwise.}\\\ \end{cases}$

  2. (7)

$\eta\in(\sigma(\Theta))^{-1}(\psi)$ for a non injective substitution
$\sigma\colon\mathrm{var}(\Theta)\to\mathcal{V}$ iff there is a decomposition
mapping $\eta^{\prime}\in\Theta^{-1}(\psi)$ such that for all
$\zeta\in\mathrm{var}(\sigma(\Theta))$ it holds that
$\eta^{\prime}(z)=\eta^{\prime}(z^{\prime})$ for all
$z,z^{\prime}\in\sigma^{-1}(\zeta)$ and

$\eta(\zeta)=\begin{cases}\eta^{\prime}(\tilde{z})&\text{if
}\zeta\in\mathrm{var}(\sigma(\Theta))\text{ and
}\tilde{z}\in\sigma^{-1}(\zeta)\\\ \top&\text{if
}\zeta\not\in\mathrm{var}(\sigma(\Theta)).\end{cases}$

We explain our decomposition method for the diamond modality for state
formulae (Definition 17.4) and for distribution formulae (Definition 17.6).
For the other modalities on state formulae, which do not directly involve the
quantitative properties of processes, we refer to [FvGdW06].

We discuss first the decomposition of a state formula $\varphi=\langle
a\rangle\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$. Given
any term $t\in\mathbb{T}(\Sigma)$ and closed substitution $\sigma$, we need to
identify in $\xi\in t^{-1}(\varphi)$ which properties each $\sigma(x)$ with
$x\in\mathrm{var}(t)$ has to satisfy in order to guarantee
$\sigma(t)\models\varphi$. By Definition 5 we have that
$\sigma(t)\models\varphi$ if and only if
$P\vdash\sigma(t)\xrightarrow{\,{a}\,}\pi$ for some probability distribution
$\pi$ such that $\pi\models\psi$. By Theorem 4 there is such a transition if
and only if there are a $P$-ruloid $\mathcal{H}/t\xrightarrow{\,{a}\,}\Theta$
and a closed substitution $\sigma^{\prime}$ with
$\sigma^{\prime}(t)=\sigma(t)$ and  (i)
$P\vdash\sigma^{\prime}(\mathcal{H})$and  (ii)
$\sigma^{\prime}(\Theta)\models\psi$.  The validity of condition (i) follows
if, for each $x\in\mathrm{var}(t)$, the literals in $\mathcal{H}$ having $x$
as left hand side test only the provable behavior of $\sigma^{\prime}(x)$.
More precisely, we need that $\sigma^{\prime}(x)\models\neg\langle
c\rangle\top$ for each
$x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}\in\mathcal{H}$ and that $\sigma^{\prime}(x)\models\langle
b\rangle\eta(\mu)$ for each $x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}$, for a
chosen decomposition mapping $\eta\in\Theta^{-1}(\psi)$ with
$\sigma^{\prime}(\mu)\models\eta(\mu)$ for each $\mu\in\mathrm{var}(\Theta)$.
The decomposed formula $\xi(x)$ is then defined as the conjunction of such
formulae. Moreover, we also add in $\xi(x)$ a conjunct $\eta(x)$ to capture
the potential behavior of $x$ as a subterm of the target term $\Theta$.
Further, the choice of $\eta$ and its use in $\xi$ also guarantees that
condition (ii) holds.

We discuss now the decomposition of a distribution formula
$\psi=\bigoplus_{i\in
I}r_{i}\varphi_{i}\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$.
Given any distribution term $\Theta\in\mathbb{DT}(\Sigma)$ and a closed
substitution $\sigma$, we need to identify in $\eta\in\Theta^{-1}(\psi)$ which
properties each $\sigma(\zeta)$ with $\zeta\in\mathrm{var}(\Theta)$ has to
satisfy in order to guarantee $\sigma(\Theta)\models\psi$. By Definition 5 we
have that $\sigma(\Theta)\models\psi$ if and only if
$\sigma(\Theta)=\sum_{i\in I}r_{i}\pi_{i}$ with $t\models\varphi_{i}$ for all
$t\in\mathsf{supp}(\pi_{i})$. Assume
$\mathsf{supp}(\sigma(\Theta))=\\{t_{m}\mid m\in M\\}$ and
$\sigma(\Theta)(t_{m})=q_{m}$. By Theorem 3, this is equivalent to have
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid
m\in\mathcal{M}\\}$ which, by Theorem 5, is equivalent to say that there are a
$\Sigma$-distribution ruloid
$\mathcal{H}/\\{\Theta\xrightarrow{\,{q_{m}}\,}u_{m}\mid m\in M\\}$ and a
closed substitution $\sigma^{\prime}$ with
$\sigma^{\prime}(\Theta)=\sigma(\Theta)$ and  (i)
$D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$and  (ii)
$\sigma^{\prime}(u_{m})\models\varphi_{i}$whenever
$\sigma^{\prime}(u_{m})\in\mathsf{supp}(\pi_{i})$.  Since the weights $q_{m}$
are univocally determined by the distributions over terms in $\mathcal{H}$ and
moreover they already represent the exact probability weights of
$\sigma(\Theta)$, we define, for each
$\mu\in\mathrm{var}(\Theta)\cap\mathcal{V}\\!_{d}$, the decomposition mapping
$\eta(\mu)$ using as weights the $q_{j}$ in the distributions over terms
$\\{\mu\xrightarrow{\,{q_{j}}\,}x_{j}\\}\in\mathcal{H}$. Then, to guarantee
condition (ii), we define $\mathfrak{w}(u_{m},\varphi_{i})$ to be positive if
$\sigma^{\prime}(u_{m})\in\mathsf{supp}(\pi_{i})$ so that we can assign the
proper decomposed formula $\xi_{m,i}(x)$ to each $x\in\mathrm{var}(u_{m})$
such that $\sigma^{\prime}(x)\models\xi_{m,i}(x)$. Moreover, since each
$\sigma^{\prime}(u_{m})$ may occur in the support of more than one $\pi_{i}$,
we impose that each $x\in\mathrm{var}(u_{m})$ satisfies the conjunction of all
the decomposed formulae $\xi_{m,i}(x)$. Therefore, also condition (i) follows.

###### Example

We exemplify two decomposition mappings in the set $t^{-1}(\varphi)$ for term
$t=x+_{2/5}(y|z)$, which is the term considered in Example 4.1 with $p=2/5$,
and the formula $\varphi=\langle a\rangle\psi$, with $\psi=\frac{1}{2}\langle
a\rangle\top\oplus\frac{1}{2}\neg\langle a\rangle\top$. As this example is
aimed at providing a deeper insight on the mechanism of our decomposition
method, we will choose arbitrarily the ruloids and the matchings for the
considered terms and formulae in order to minimize the number of mappings
involved in the decomposition and improve readability. Let $\rho$ be the last
ruloid for $t$ in Example 4.1,
$\Theta=\frac{2}{5}\mu+\frac{3}{5}(\nu|\upsilon)$ denote its target, and
$\rho^{\textsf{D}}$ be the $\Sigma$-distribution ruloid for $\Theta$ showed in
Example 4.2. By Definition 17.4, the decomposition mappings $\xi\in
t^{-1}(\varphi)$ built over $\rho$ are such that:

$\xi(x)=\langle a\rangle\eta(\mu)\qquad\qquad\xi(y)=\langle
a\rangle\eta(\nu)\qquad\qquad\xi(z)=\langle a\rangle\eta(\upsilon)$ (11)

where $\eta\in\Theta^{-1}(\psi)$. Consider the matching
$\mathfrak{w}\in\mathfrak{W}(\mathrm{conc}(\rho^{\textsf{D}}),\psi)$ for
$\mathrm{conc}(\rho^{\textsf{D}})$ and $\psi$ defined by

$\mathfrak{w}(x_{1},\langle
a\rangle\top)=\frac{1}{10}\quad\mathfrak{w}(x_{2},\neg\langle
a\rangle\top)=\frac{3}{10}\quad\mathfrak{w}(y_{1}|z,\neg\langle
a\rangle\top)=\frac{1}{5}\quad\mathfrak{w}(y_{2}|z,\langle
a\rangle\top)=\frac{2}{5}\text{.}$

For the terms and the formulae to which $\mathfrak{w}$ gives a positive
weight, we obtain the decomposition mappings in Table 1, where $\xi_{3}$ and
$\xi_{4}$ derive from Definition 17.2.

$x_{1}^{-1}(\langle a\rangle\top)=\\{\xi_{1}\\}$ |  $\xi_{1}(x_{1})=\langle a\rangle\top$, $\xi_{1}(x)=\top$ for all other $x\in\mathcal{V}\\!_{s}$
---|---
$x_{2}^{-1}(\neg\langle a\rangle\top)=\\{\xi_{2}\\}$ |  $\xi_{2}(x_{2})=\neg\langle a\rangle\top$, $\xi_{2}(x)=\top$ for all other $x\in\mathcal{V}\\!_{s}$
$(y_{1}|z)^{-1}(\neg\langle a\rangle\top)=\\{\xi_{3},\xi_{4}\\}$ |  $\xi_{3}(y_{1})=\neg\langle a\rangle\top$, $\xi_{3}(z)=\top$, $\xi_{3}(x)=\top$ for all other $x\in\mathcal{V}\\!_{s}$
$\xi_{4}(y_{1})=\top$, $\xi_{4}(z)=\neg\langle a\rangle\top$,
$\xi_{4}(x)=\top$ for all other $x\in\mathcal{V}\\!_{s}$
$(y_{2}|z)^{-1}(\langle a\rangle\top)=\\{\xi_{5}\\}$ |  $\xi_{5}(y_{2})=\\!\langle a\rangle\top$, $\xi_{5}(z)=\\!\langle a\rangle\top$, $\xi_{5}(x)=\\!\top$ for all other $x\in\mathcal{V}\\!_{s}$
Table 1. Derived decomposition mappings

Next, we construct the decomposition mappings for the variable $\nu$ in
$\Theta$ wrt. $\rho^{\textsf{D}}$ and $\mathfrak{w}$. By Definition 17.6a we
consider the weights of the premises of $\rho^{D}$ having $\nu$ as left-hand
side, namely
$\mathcal{H}_{\nu}=\\{\nu\xrightarrow{\,{1/3}\,}y_{1},\quad\nu\xrightarrow{\,{2/3}\,}y_{2}\\}$,
and use them as weights of the $\bigoplus$ operator. Then for each of the
variables $y_{1},y_{2}$ in the right side of $\mathcal{H}_{\nu}$, we consider
the conjunction of the formulae assigned to it by one decomposition mapping
from each set in the first column of Table 1. In detail, by omitting multiple
occurrences of the $\top$ formulae in conjunctions, for $y_{1}$ we consider
$\xi_{1}(y_{1})\wedge\xi_{2}(y_{1})\wedge\xi_{3}(y_{1})\wedge\xi_{5}(y_{1})=\neg\langle
a\rangle\top$ and
$\xi_{1}(y_{1})\wedge\xi_{2}(y_{1})\wedge\xi_{4}(y_{1})\wedge\xi_{5}(y_{1})=\top$,
and for $y_{2}$ we consider
$\xi_{1}(y_{2})\wedge\xi_{2}(y_{2})\wedge\xi_{3}(y_{2})\wedge\xi_{5}(y_{2})=\langle
a\rangle\top$ and
$\xi_{1}(y_{1})\wedge\xi_{2}(y_{1})\wedge\xi_{4}(y_{1})\wedge\xi_{5}(y_{1})=\langle
a\rangle\top$. Hence the choice between $\xi_{3}$ or $\xi_{4}$ generates two
different decomposition mappings in $\Theta^{-1}(\psi)$: by $\xi_{3}$ we
obtain the decomposition mapping $\eta_{1}\in\Theta^{-1}(\psi)$ with
$\eta_{1}(\nu)=\frac{1}{3}\neg\langle a\rangle\top\oplus\frac{2}{3}\langle
a\rangle\top$ and by $\xi_{4}$ we obtain the decomposition mapping
$\eta_{2}\in\Theta^{-1}(\psi)$ with
$\eta_{2}(\nu)=\frac{1}{3}\top\oplus\frac{2}{3}\langle a\rangle\top$. By
applying the same reasoning to $\mu$ and $\upsilon$ we obtain

$\eta_{1}(\mu)=\frac{1}{4}\langle a\rangle\top\oplus\frac{3}{4}\neg\langle
a\rangle\top\quad\eta_{1}(\nu)=\frac{1}{3}\neg\langle
a\rangle\top\oplus\frac{2}{3}\langle
a\rangle\top\quad\eta_{1}(\upsilon)=1(\top\wedge\langle a\rangle\top)$
$\eta_{2}(\mu)=\frac{1}{4}\langle a\rangle\top\oplus\frac{3}{4}\neg\langle
a\rangle\top\quad\eta_{2}(\nu)=\frac{1}{3}\top\oplus\frac{2}{3}\langle
a\rangle\top\quad\eta_{2}(\upsilon)=1(\neg\langle a\rangle\top\wedge\langle
a\rangle\top)$

where we have omitted multiple occurrences of the $\top$ formulae in
conjunctions. Finally, we obtain two decomposition mappings in
$t^{-1}(\varphi)$ by substituting $\eta$ with either $\eta_{1}$ or $\eta_{2}$
in Equation (11), obtaining respectively

$\xi^{1}(x)=\langle a\rangle\Big{(}\frac{1}{4}\langle
a\rangle\top\oplus\frac{3}{4}\neg\langle
a\rangle\top\Big{)}\quad\xi^{1}(y)=\langle
a\rangle\Big{(}\frac{1}{3}\neg\langle a\rangle\top\oplus\frac{2}{3}\langle
a\rangle\top\Big{)}\quad\xi^{1}(z)=\langle a\rangle\Big{(}1(\langle
a\rangle\top\wedge\top)\Big{)}$ $\xi^{2}(x)=\langle
a\rangle\Big{(}\frac{1}{4}\langle a\rangle\top\oplus\frac{3}{4}\neg\langle
a\rangle\top\Big{)}\quad\xi^{2}(y)=\langle
a\rangle\Big{(}\frac{1}{3}\top\oplus\frac{2}{3}\langle
a\rangle\top\Big{)}\quad\xi^{2}(z)=\langle a\rangle\Big{(}1(\neg\langle
a\rangle\top\wedge\langle a\rangle\top)\Big{)}.$

We show now that by decomposing formulae in $\operatorname{\mathcal{L}}$ we
get formulae in $\operatorname{\mathcal{L}}$. This is essential to derive the
congruence theorem for probabilistic bisimulation (Theorem 8.1): the
congruence theorem exploits the characterization of probabilistic bisimulation
with the logic $\operatorname{\mathcal{L}}$ recalled in Theorem 1, and
requires that the formulae for composed terms and those obtained for their
subterms through the decomposition method are all formulae in the
characterizing logic $\operatorname{\mathcal{L}}$.

###### Lemma 3

Assume the terms $t\in\mathbb{T}(\Sigma)$ and $\Theta\in\mathbb{DT}(\Sigma)$
and the formulae
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ and
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$. Then:

  1. (1)

For all $x\in\mathcal{V}\\!_{s}$ we have
$\xi(x)\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ for each
$\xi\in t^{-1}(\varphi)$.

  2. (2)

For all $\zeta\in\mathcal{V}\\!_{d}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$ for
each $\eta\in\Theta^{-1}(\psi)$.

  3. (3)

For all $\zeta\in\mathcal{V}\\!_{s}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ for
each $\eta\in\Theta^{-1}(\psi)$.

###### Proof.

The proof follows immediately from Definition 17. ∎

The following result confirms that our decomposition method is correct.

######  Theorem 6 (Decomposition theorem)

Let $P=(\Sigma,\mathcal{A},R)$ be a PGSOS-PTSS and let $D_{\Sigma}$ be the
$\Sigma$-DS. For any term $t\in\mathbb{T}(\Sigma)$, closed substitution
$\sigma$ and state formula
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ we have

$\sigma(t)\models\varphi\Leftrightarrow\exists\,\xi\in t^{-1}(\varphi)\text{
such that for all }x\in\mathrm{var}(t)\text{ it holds }\sigma(x)\models\xi(x)$

and for any distribution term $\Theta\in\mathbb{DT}(\Sigma)$, closed
substitution $\sigma$ and distribution formula
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$ we have

$\sigma(\Theta)\models\psi\Leftrightarrow\exists\,\eta\in\Theta^{-1}(\psi)\text{
such that for all }\zeta\in\mathrm{var}(\Theta)\text{ it holds
}\sigma(\zeta)\models\eta(\zeta).$

###### Proof.

We start with univariate terms. We proceed by structural induction over
$\phi\in\operatorname{\mathcal{L}}$ to prove that for any univariate
$t\in\mathbb{T}(\Sigma)$, closed substitution $\sigma$ and
$\phi=\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ we
have

$\sigma(t)\models\varphi\Leftrightarrow\exists\xi\in t^{-1}(\varphi)\text{
such that }\forall x\in\mathrm{var}(t)\text{ it holds }\sigma(x)\models\xi(x)$
(12)

and for any univariate $\Theta\in\mathbb{DT}(\Sigma)$, closed substitution
$\sigma$ and
$\phi=\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$ we have

$\sigma(\Theta)\models\psi\Leftrightarrow\exists\eta\in\Theta^{-1}(\psi)\text{
such that }\forall\zeta\in\mathrm{var}(\Theta)\text{ it holds
}\sigma(\zeta)\models\eta(\zeta).$ (13)

  * •

Base case $\phi=\top$. Then by Definition 17.1 we have that $\xi\in
t^{-1}(\top)$ iff $\xi(x)=\top$ for all $x\in\mathcal{V}\\!_{s}$. Then the
proof obligation Equation (12) directly follows from the definition of
$\models$ (Definition 5).

  * •

Inductive step $\phi=\neg\varphi$ for some
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$. We have

$\displaystyle\sigma(t)\models\neg\varphi$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\sigma(t)\not\models\varphi$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\,\xi\in
t^{-1}(\varphi)\;\exists\,x\in\mathrm{var}(t)\text{ s.t.
}\sigma(x)\not\models\xi(x)$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\,\mathfrak{f}\colon
t^{-1}(\varphi)\to\mathrm{var}(t)\text{ s.t. }\forall\,\xi^{\prime}\in
t^{-1}(\varphi)\text{ it holds
}\sigma(\mathfrak{f}(\xi^{\prime}))\not\models\xi^{\prime}(\mathfrak{f}(\xi^{\prime}))$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists\,\mathfrak{f}\colon
t^{-1}(\varphi)\to\mathrm{var}(t)\text{ s.t.
}\forall\,x\in\mathrm{var}(t)\text{ it holds
}\sigma(x)\models\bigwedge_{\xi^{\prime}\in\mathfrak{f}^{-1}(x)}\neg\xi^{\prime}(x)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists\,\xi\in
t^{-1}(\neg\varphi)\text{ s.t. }\forall\,x\in\mathrm{var}(t)\text{ it holds
}\sigma(x)\models\xi(x)$

where the second relation follows by the inductive hypothesis and the last
relation follows by construction of $t^{-1}(\neg\varphi)$ (Definition 17.2).
Hence, the proof obligation Equation (12) holds also in this case.

  * •

Inductive step $\phi=\bigwedge_{j\in J}\varphi_{j}$ for some $j\in J$ and
$\varphi_{j}\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$. We
have

$\displaystyle\sigma(t)\models\bigwedge_{j\in J}\varphi_{j}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\sigma(t)\models\varphi_{j},\text{ for all }j\in J$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists\,\xi_{j}\in
t^{-1}(\varphi_{j})\text{ s.t. }\forall\,x\in\mathrm{var}(t)\text{ it holds
}\sigma(x)\models\xi_{j}(x),\text{ for all }j\in J$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists\,\xi_{j}\in
t^{-1}(\varphi_{j})\text{ for all }j\in J\text{ s.t.
}\forall\,x\in\mathrm{var}(t)\text{ it holds }\sigma(x)\models\bigwedge_{j\in
J}\xi_{j}(x)$ $\displaystyle\Leftrightarrow\;$ $\displaystyle\exists\,\xi\in
t^{-1}(\bigwedge_{j\in J}\varphi_{j})\text{ s.t.
}\forall\,x\in\mathrm{var}(t)\text{ it holds }\sigma(x)\models\xi(x)$

where the second relation follows by the inductive hypothesis and the last
relation follows by construction of $t^{-1}(\bigwedge_{j\in J}\varphi_{j})$
(Definition 17.3). Hence, the proof obligation Equation (12) holds also in
this case.

  * •

Inductive step $\phi=\bigoplus_{i\in I}r_{i}\varphi_{i}$ for some
$\varphi_{i}\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$, with
$r_{i}\in(0,1]$ for $i\in I$ and $\sum_{i\in I}r_{i}=1$. Notice that in this
case we have $\phi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$
and therefore we need to show Equation (13). To this aim, we prove the two
implications separately.

($\Rightarrow$) Assume first that $\sigma(\Theta)\models\bigoplus_{i\in
I}r_{i}\varphi_{i}$. Then, by definition of $\models$ (Definition 5), this
implies that there exists a family of probability distributions
$\\{\pi_{i}\\}_{i\in I}\subseteq\Delta(\mathcal{T}(\Sigma))$ with
$\sigma(\Theta)=\sum_{i\in I}r_{i}\pi_{i}$ and whenever
$t\in\mathsf{supp}(\pi_{i})$ for some $t\in\mathcal{T}(\Sigma)$, then
$t\models\varphi_{i}$. Notice that
$\mathsf{supp}(\sigma(\Theta))=\bigcup_{i\in I}\mathsf{supp}(\pi_{i})$. Let us
order the elements of the support of the distribution $\sigma(\Theta)$ through
indexes in a suitable set $M$, namely
$\mathsf{supp}(\sigma(\Theta))=\\{t_{m}\mid m\in M\\}$, with
$t_{m},t_{m^{\prime}}$ pairwise distinct for all $m,m^{\prime}\in M$ with
$m\neq m^{\prime}$. We have $\sigma(\Theta)=\sum_{m\in M}q_{m}\delta_{t_{m}}$,
for some $q_{m}\in(0,1]$ such that $\sum_{m\in M}q_{m}=1$. In particular, this
gives $q_{m}=\sigma(\Theta)(t_{m})$, which, by Theorem 3, implies that
$D\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in M\\}$. By
Theorem 5,
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in
M\\}$ implies that there are a $\Sigma$-distribution ruloid
$\rho^{\textsf{D}}=\frac{\displaystyle\mathcal{H}}{\displaystyle\\{\Theta\xrightarrow{\,{q_{m}}\,}u_{m}\mid
m\in M\\}}$ and a closed substitution $\sigma^{\prime}$ with
$D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$,
$\sigma^{\prime}(\Theta)=\sigma(\Theta)$ and $\sigma^{\prime}(u_{m})=t_{m}$
for each $m\in M$. Let us show that the rewriting of $\sigma^{\prime}(\Theta)$
as convex combination of the $\\{\pi_{i}\\}_{i\in I}$ gives rise to a matching
for $\mathrm{conc}(\rho^{\textsf{D}})$ and $\bigoplus_{i\in
I}r_{i}\varphi_{i}$. Define
$\mathfrak{w}\in\mathfrak{W}(\mathrm{conc}(\rho^{\textsf{D}}),\bigoplus_{i\in
I}r_{i}\varphi_{i})$ as
$\mathfrak{w}(u_{m},\varphi_{i})=r_{i}\pi_{i}(\sigma^{\prime}(u_{m}))$, then
$\mathfrak{w}$ is a matching with left marginal
$\mathrm{conc}(\rho^{\textsf{D}})$, and right marginal the distribution
formula $\bigoplus_{i\in I}r_{i}\varphi_{i}$. More precisely, we have

$\displaystyle q_{m}$ $\displaystyle={}$ $\displaystyle\sigma(\Theta)(t_{m})$
(by construction of $\sigma(\Theta)$) $\displaystyle={}$
$\displaystyle\sum_{i\in I}r_{i}\pi_{i}(t_{m})$ (by def. of convex combination
of distributions) $\displaystyle={}$ $\displaystyle\sum_{i\in
I}r_{i}\pi_{i}(\sigma^{\prime}(u_{m}))$ (by construction of $\sigma^{\prime}$)
$\displaystyle={}$ $\displaystyle\sum_{i\in I}\mathfrak{w}(u_{m},\varphi_{i})$
(by definition of $\mathfrak{w}$)

and

$\displaystyle\sum_{m\in M}\mathfrak{w}(u_{m},\varphi_{i})$ $\displaystyle={}$
$\displaystyle\sum_{m\in M}r_{i}\pi_{i}(\sigma^{\prime}(u_{m}))$ (by
definition of $\mathfrak{w}$) $\displaystyle={}$ $\displaystyle\sum_{m\in
M}r_{i}\pi_{i}(t_{m})$ (by construction of $\sigma^{\prime}$)
$\displaystyle={}$ $\displaystyle
r_{i}\,\sum_{t\in\mathsf{supp}(\sigma(\Theta))}\pi_{i}(t)$ (by the choice of
$M$) $\displaystyle={}$ $\displaystyle
r_{i}\,\sum_{t\in\mathsf{supp}(\pi_{i})}\pi_{i}(t)$ $\displaystyle={}$
$\displaystyle r_{i}\text{.}$

We derive that:

    1. (1)

from $\sigma^{\prime}(\Theta)=\sigma(\Theta)$ we obtain that
$\sigma^{\prime}(\zeta)=\sigma(\zeta)$ for all variables
$\zeta\in\mathrm{var}(\Theta)$;

    2. (2)

whenever $\mathfrak{w}(u_{m},\varphi_{i})>0$ it holds that
$\sigma^{\prime}(u_{m})\in\mathsf{supp}(\pi_{i})$ and, therefore, we infer
$\sigma^{\prime}(u_{m})\models\varphi_{i}$. By the inductive hypothesis we
derive that there is a decomposition mapping $\xi_{m,i}\in
u_{m}^{-1}(\varphi_{i})$ such that $\sigma^{\prime}(x)\models\xi_{m,i}(x)$ for
all $x\in\mathrm{var}(u_{m})$;

    3. (3)

from $D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$ we obtain that for all
premises $\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid j\in J\\}\in\mathcal{H}$
we have
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\zeta)\xrightarrow{\,{q_{h}}\,}t^{\prime}_{h}\mid
h\in H\\}$, where
$\\{\sigma^{\prime}(\zeta)\xrightarrow{\,{q_{h}}\,}t^{\prime}_{h}\mid h\in
H\\}$ is $\sigma^{\prime}(\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid j\in
J\\})$, for a suitable set of indexes $H$ and proper terms $t_{h}^{\prime}$.
By Theorem 3,
$D_{\Sigma}\vdash\\{\sigma^{\prime}(\zeta)\xrightarrow{\,{q_{h}}\,}t^{\prime}_{h}\mid
h\in H\\}$ iff $\sigma^{\prime}(\zeta)(t^{\prime}_{h})=q_{h}$ and $\sum_{h\in
H}q_{h}=1$. Hence we have that

$\displaystyle\sigma^{\prime}(\zeta)$ $\displaystyle={}$
$\displaystyle\sum_{h\in H}q_{h}\delta_{t^{\prime}_{h}}$ $\displaystyle={}$
$\displaystyle\sum_{h\in H}\big{(}\sum_{j\in
J,\sigma^{\prime}(x_{j})=t^{\prime}_{h}}q_{j}\big{)}\delta_{t^{\prime}_{h}}$
(by Definition 11) $\displaystyle={}$ $\displaystyle\sum_{h\in
H}\big{(}\sum_{j\in
J,\sigma^{\prime}(x_{j})=t^{\prime}_{h}}q_{j}\delta_{\sigma^{\prime}(x_{j})}\big{)}$
$\displaystyle={}$ $\displaystyle\sum_{j\in
J}q_{j}\delta_{\sigma^{\prime}(x_{j})}$ (the $t^{\prime}_{h}$ are pairwise
distinct).

We remark that this reasoning holds since we assumed that $\Theta$ is
univariate, and therefore there is only one set of distribution premises in
$\mathcal{H}$ with left-hand side $\zeta$, for each
$\zeta\in\mathrm{var}(\Theta)$.

Let $\eta\in\Theta^{-1}(\bigoplus_{i\in I}r_{i}\varphi_{i})$ be the
decomposition mapping defined as in Definition 17.6 by means of the
$\Sigma$-distribution ruloid
$\frac{\displaystyle\mathcal{H}}{\displaystyle\\{\Theta\xrightarrow{\,{q_{m}}\,}u_{m}\mid
m\in M\\}}$ and the decomposition mappings $\xi_{m,i}$ as in item (2) above
for each $m\in M$ and $i\in I$ such that $\mathfrak{w}(u_{m},\varphi_{i})>0$,
and $\xi_{m,i}$ defined by $\xi_{m,i}(x)=\top$ for all
$x\in\mathcal{V}\\!_{s}$ for those $m,i$ such that
$\mathfrak{w}(u_{m},\varphi_{i})=0$. We aim to show that for this $\eta$ it
holds that $\sigma^{\prime}(\zeta)\models\eta(\zeta)$ for each
$\zeta\in\mathrm{var}(\Theta)$. By construction,

$\eta(\zeta)=\begin{cases}\displaystyle\bigoplus_{\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid
j\in J\\}\in\mathcal{H}}q_{j}\bigwedge_{m\in M\atop i\in
I}\xi_{m,i}(x_{j})&\text{ if }\zeta\in\mathcal{V}\\!_{d}\\\
\displaystyle\bigwedge_{m\in M\atop i\in I}\xi_{m,i}(x)&\text{ if
}\zeta=x\in\mathcal{V}\\!_{s}.\end{cases}$

For each variable $y\in\\{x_{j}\mid j\in J\\}\cup\\{x\\}$ and for each $m\in
M$ and $i\in I$, we can distinguish three cases:

    1. (4)

$y\in\mathrm{var}(u_{m})$ and $\mathfrak{w}(u_{m},\varphi_{i})>0$. Then, by
item (2) above, we have $\sigma^{\prime}(y)\models\xi_{m,i}(y)$.

    2. (5)

$y\in\mathrm{var}(u_{m})$ and $\mathfrak{w}(u_{m},\varphi_{i})=0$. Then by
construction $\xi_{m,i}(y)=\top$, thus giving that
$\sigma^{\prime}(y)\models\xi_{m,i}(y)$ holds trivially also in this case.

    3. (6)

$y\not\in\mathrm{var}(u_{m})$. Then, whichever is the value of
$\mathfrak{w}(u_{m},\varphi_{i})$, we have $\xi_{m,i}(y)=\top$ (see Definition
17) and consequently $\sigma^{\prime}(y)\models\xi_{m,i}(y)$ holds trivially
also in this case.

Since these considerations apply to each $m\in M$ and $i\in I$ we can conclude
that if $\zeta\in\mathcal{V}\\!_{d}$ then for all
$\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid j\in J\\}\in\mathcal{H}$ it holds
that for each $x_{j}$ with $j\in J$ we have
$\sigma^{\prime}(x_{j})\models\bigwedge_{m\in M,i\in I}\xi_{m,i}(x_{j})$.
Furthermore, by item (3) above, if $\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid
j\in J\\}\in\mathcal{H}$ then $D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$
gives $\sigma^{\prime}(\zeta)=\sum_{j\in
J}q_{j}\delta_{\sigma^{\prime}(x_{j})}$, from which we can conclude that

$\sigma^{\prime}(\zeta)\models\bigoplus_{j\in J}q_{j}\bigwedge_{i\in I,m\in
M}\xi_{m,i}(x_{j})\text{, namely }\sigma^{\prime}(\zeta)\models\eta(\zeta).$

Similarly, if $\zeta=x\in\mathcal{V}\\!_{s}$ then

$\sigma^{\prime}(x)\models\bigwedge_{m\in M,i\in I}\xi_{m,i}(x)\text{, namely
}\sigma^{\prime}(x)\models\eta(x).$

Thus, we can conclude that for each $\zeta\in\mathrm{var}(\Theta)$ it holds
that $\sigma^{\prime}(\zeta)\models\eta(\zeta)$. Since moreover
$\sigma(\zeta)=\sigma^{\prime}(\zeta)$ (item (1) above), we can conclude that
$\sigma(\zeta)\models\eta(\zeta)$ as required.

($\Leftarrow$) Assume now that there is a decomposition mapping
$\eta\in\Theta^{-1}(\bigoplus_{i\in I}r_{i}\varphi_{i})$ such that
$\sigma(\zeta)\models\eta(\zeta)$ for all $\zeta\in\mathrm{var}(\Theta)$.
Following Definition 17.6, the existence of such a decomposition mapping
$\eta$ entails the existence of a $\Sigma$-distribution ruloid
$\rho^{\textsf{D}}=\frac{\displaystyle\mathcal{H}}{\displaystyle\\{\Theta\xrightarrow{\,{q_{m}}\,}t_{m}\mid
m\in M\\}}$ with $\sum_{m\in M}q_{m}=1$ (Proposition 5) and of a matching
$\mathfrak{w}\in\mathfrak{W}(\mathrm{conc}(\rho^{\textsf{D}}),\bigoplus_{i\in
I}r_{i}\varphi_{i})$ from which we can build the following decomposition
mappings:

$\begin{cases}\xi_{m,i}\in t_{m}^{-1}(\varphi_{i})&\text{ if
}\mathfrak{w}(t_{m},\varphi_{i})>0\\\ \xi_{m,i}\in t_{m}^{-1}(\top)&\text{
otherwise.}\end{cases}$

In particular, we have that for each $\mu\in\mathrm{var}(\Theta)$

$\eta(\mu)=\bigoplus_{\\{\mu\xrightarrow{\,{q_{j}}\,}x_{j}\mid\sum_{j\in
J}q_{j}=1\\}\in\mathcal{H}}q_{j}\bigwedge_{i\in I,m\in M}\xi_{m,i}(x_{j})$

and for each $x\in\mathrm{var}(\Theta)$

$\eta(x)=\displaystyle\bigwedge_{i\in I,m\in M}\xi_{m,i}(x).$

We define a closed substitution $\sigma^{\prime}$ such that
$\sigma^{\prime}(\zeta)=\sigma(\zeta)$ for each $\zeta\in\mathrm{var}(\Theta)$
and $\sigma^{\prime}(x)=\sigma(x)$ for each $x\in\mathrm{rhs}(\mathcal{H})$.
Then, the following properties hold:

    1. (a)

From $\sigma^{\prime}(\zeta)=\sigma(\zeta)$ and
$\sigma(\zeta)\models\eta(\zeta)$ we derive
$\sigma^{\prime}(\zeta)\models\eta(\zeta)$. In particular we obtain that
$\sigma^{\prime}(x)\models\bigwedge_{i\in I,m\in M}\xi_{m,i}(x)$ for each
$x\in\mathrm{var}(\Theta)$.

    2. (b)

As $\sigma^{\prime}(\mu)\models\eta(\mu)$ for each
$\mu\in\mathrm{var}(\Theta)$, by previous item (a), we derive that there are
probability distributions $\pi_{j}$ such that $\sigma^{\prime}(\mu)=\sum_{j\in
J}q_{j}\pi_{j}$ and whenever $t\in\mathsf{supp}(\pi_{j})$, for some
$t\in\mathcal{T}(\Sigma)$, then $t\models\bigwedge_{i\in I,m\in
M}\xi_{m,i}(x_{j})$. By Definition 17.6a, the weights of the distribution
formula $\eta(\mu)$ coincide with the weights of the distribution literals in
$\\{\mu\xrightarrow{\,{q_{j}}\,}x_{j}\mid\sum_{j\in
J}q_{j}=1\\}\in\mathcal{H}$. Therefore, we have that
$\sigma^{\prime}(\mu)=\sum_{j\in J}q_{j}\delta_{\sigma^{\prime}(x_{j})}$ from
which we gather $\sigma^{\prime}(x_{j})\models\bigwedge_{i\in I,m\in
M}\xi_{m,i}(x_{j})$, for each $j\in J$.

    3. (c)

From $\sigma(\zeta)=\sigma^{\prime}(\zeta)$ for each
$\zeta\in\mathrm{var}(\Theta)$ we infer that
$\sigma^{\prime}(\Theta)=\sigma(\Theta)$. Moreover, by Lemma 2.3 we have that
$\mathrm{rhs}(\mathcal{H})=\bigcup_{m\in M}\mathrm{var}(t_{m})$, so that
$\sigma^{\prime}(x)=\sigma(x)$ for each $x\in\mathrm{rhs}(\mathcal{H})$
implies $\sigma^{\prime}(t_{m})=\sigma(t_{m})$ for each $m\in M$.

From items (a), (b) above and by structural induction we gather
$\sigma^{\prime}(t_{m})\models\varphi_{i}$ for each $m\in M,i\in I$ with
$\mathfrak{w}(t_{m},\varphi_{i})>0$. Moreover, from
$\sigma^{\prime}(\zeta)\models\eta(\zeta)$ for each
$\zeta\in\mathrm{var}(\Theta)$, item (a) above, we obtain that
$D_{\Sigma}\vdash\sigma^{\prime}(\mathcal{H})$, namely $D_{\Sigma}$ proves the
reduced instance w.r.t, $\sigma^{\prime}$ of each set of distribution premises
$\\{\zeta\xrightarrow{\,{q_{j}}\,}x_{j}\mid\sum_{j\in
J}q_{j}=1\\}\in\mathcal{H}$. This fact taken together with item (c) above and
Theorem 5 gives that $D_{\Sigma}$ proves the reduced instance of
$\\{\Theta\xrightarrow{\,{q_{m}}\,}t_{m}\mid m\in M\\}$ wrt. $\sigma$, that is
$D_{\Sigma}\vdash\\{\sigma(\Theta)\xrightarrow{\,{q_{h}}\,}t^{\prime}_{h}\mid
h\in H\\}$ for a suitable set of indexes $H$ and a proper set of closed terms
$t^{\prime}_{h}$ such that for each $h\in H$ there is at least one $m\in M$
such that $t^{\prime}_{h}=\sigma^{\prime}(t_{m})$ and moreover
$q_{h}=\sum_{\\{m\in M\mid\sigma^{\prime}(t_{m})=t^{\prime}_{h}\\}}q_{m}$
(Definition 11). In addition, by Theorem 3 it follows that
$q_{h}=\sigma(\Theta)(t^{\prime}_{h})$ for each $h\in H$ and $\sum_{h\in
H}q_{h}=1$. Since moreover $q_{h}\in(0,1]$ for each $h\in H$, this is
equivalent to say that $\sigma(\Theta)=\sum_{h\in
H}q_{h}\delta_{\sigma^{\prime}(t_{h})}$. Finally, we notice that

$\displaystyle\sigma(\Theta)={}$ $\displaystyle\sum_{h\in
H}q_{h}\delta_{t^{\prime}_{h}}$ $\displaystyle={}$ $\displaystyle\sum_{h\in
H}\Big{(}\sum_{\\{m\in
M\mid\sigma^{\prime}(t_{m})=t^{\prime}_{h}\\}}q_{m}\Big{)}\delta_{t^{\prime}_{h}}$
$\displaystyle={}$ $\displaystyle\sum_{m\in
M}q_{m}\delta_{\sigma^{\prime}(t_{m})}$ ($t^{\prime}_{h}$ pairwise distinct)
$\displaystyle={}$ $\displaystyle\sum_{m\in M}\Big{(}\sum_{i\in
I}\mathfrak{w}(t_{m},\varphi_{i})\Big{)}\delta_{\sigma^{\prime}(t_{m})}$
$\displaystyle\text{(}\sum_{i\in
I}\mathfrak{w}(t_{m},\varphi_{i})=q_{m}\text{)}$ $\displaystyle={}$
$\displaystyle\sum_{i\in I}\Big{(}\sum_{m\in
M}\mathfrak{w}(t_{m},\varphi_{i})\delta_{\sigma^{\prime}(t_{m})}\Big{)}$
$\displaystyle={}$ $\displaystyle\sum_{i\in I}\Big{(}\sum_{m\in
M}r_{i}\frac{\mathfrak{w}(t_{m},\varphi_{i})}{r_{i}}\delta_{\sigma^{\prime}(t_{m})}\Big{)}$
$\displaystyle={}$ $\displaystyle\sum_{i\in I}r_{i}\Big{(}\sum_{m\in
M}\frac{\mathfrak{w}(t_{m},\varphi_{i})}{r_{i}}\delta_{\sigma^{\prime}(t_{m})}\Big{)}$
$\displaystyle={}$ $\displaystyle\sum_{i\in I}r_{i}\pi_{i}$

where for each $i\in I$, $\pi_{i}=\sum_{m\in
M}\displaystyle\frac{\mathfrak{w}(t_{m},\varphi_{i})}{r_{i}}\delta_{\sigma^{\prime}(t_{m})}$
is a probability distribution as it is obtained as a convex combination of
probability distributions ($\sum_{m\in
M}\displaystyle\frac{\mathfrak{w}(t_{m},\varphi_{i})}{r_{i}}=1$). Moreover,
the $\pi_{i}$ are such that whenever
$\sigma^{\prime}(t)\in\mathsf{supp}(\pi_{i})$ it holds that
$\sigma^{\prime}(t)\models\varphi_{i}$. In fact, we have that whenever
$\mathfrak{w}(t_{m},\varphi_{i})>0$, then the only closed term in the support
of $\delta_{\sigma^{\prime}(t_{m})}$ is indeed $\sigma^{\prime}(t_{m})$.
Furthermore, whenever $\sigma^{\prime}(t_{m})\not\models\varphi_{i}$ we are
granted that $\mathfrak{w}(t_{m},\varphi_{i})=0$, thus giving that
$\sigma^{\prime}(t_{m})$ is not in the support of $\pi_{i}$. Therefore, we can
conclude that $\sigma(\Theta)\models\bigoplus_{i\in I}r_{i}\varphi_{i}$ as
requested.

Hence, the proof obligation Equation (13) follows from the two implications.

  * •

Inductive step $\phi=\langle a\rangle\psi$ for some
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{d}}}$ and
$a\in\mathcal{A}$. Notice that in this case we have
$\phi\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ and therefore
we need to show Equation (12). To this aim, we prove the two implications
separately.

($\Rightarrow$) Assume first that $\sigma(t)\models\langle a\rangle\psi$.
Then, by definition of relation $\models$ (Definition 5), there exists a
probability distribution $\pi\in\Delta(\mathcal{T}(\Sigma))$ with
$P\vdash\sigma(t)\xrightarrow{\,{a}\,}\pi$ and $\pi\models\psi$. By Theorem 4,
$P\vdash\sigma(t)\xrightarrow{\,{a}\,}\pi$ implies that there are a $P$-ruloid
$\frac{\displaystyle\mathcal{H}}{\displaystyle t\xrightarrow{\,{a}\,}\Theta}$
and a closed substitution $\sigma^{\prime}$ with
$P\vdash\sigma^{\prime}(\mathcal{H})$, $\sigma^{\prime}(t)=\sigma(t)$ and
$\sigma^{\prime}(\Theta)=\pi$. We infer the following facts:

    1. (1)

from $\sigma^{\prime}(t)=\sigma(t)$ we obtain that
$\sigma^{\prime}(x)=\sigma(x)$ for all $x\in\mathrm{var}(t)$;

    2. (2)

from $\sigma^{\prime}(\Theta)=\pi$ and $\pi\models\psi$, we gather
$\sigma^{\prime}(\Theta)\models\psi$ and by the inductive hypothesis we obtain
that there exists a $\eta\in\Theta^{-1}(\psi)$ such that
$\sigma^{\prime}(\zeta)\models\eta(\zeta)$ for all
$\zeta\in\mathrm{var}(\Theta)$;

    3. (3)

from $P\vdash\sigma^{\prime}(\mathcal{H})$ we obtain that whenever
$x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}$ we have
$P\vdash\sigma^{\prime}(x)\xrightarrow{\,{b}\,}\sigma^{\prime}(\mu)$. Then, if
$\mu\in\mathrm{var}(\Theta)$, by previous item (2), we get
$\sigma^{\prime}(\mu)\models\eta(\mu)$. Otherwise, if
$\mu\not\in\mathrm{var}(\Theta)$, we have $\eta(\mu)=\top$ thus giving
$\sigma^{\prime}(\mu)\models\eta(\mu)$ also in this case. Hence,
$\sigma^{\prime}(\mu)\models\eta(\mu)$ and $\sigma^{\prime}(x)\models\langle
b\rangle\eta(\mu)$ in all cases.

    4. (4)

from $P\vdash\sigma^{\prime}(\mathcal{H})$ we obtain that whenever
$x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}\in\mathcal{H}$ we have
$P\vdash\sigma^{\prime}(x)\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$, namely
$P\not\vdash\sigma^{\prime}(x)\xrightarrow{\,{c}\,}\upsilon$ for any
$\upsilon\in{\mathcal{D}T}(\Sigma)$, giving
$\sigma^{\prime}(x)\models\neg\langle c\rangle\top$.

Let $\xi\in t^{-1}(\langle a\rangle\psi)$ be defined as in Definition 17.4 by
means of the $P$-ruloid $\frac{\displaystyle\mathcal{H}}{\displaystyle
t\xrightarrow{\,{a}\,}\Theta}$ and the decomposition mapping $\eta$ introduced
in item (2) above. We aim to show that for this $\xi$ it holds that
$\sigma^{\prime}(x)\models\xi(x)$ for each $x\in\mathrm{var}(t)$. By
construction,

$\xi(x)=\bigwedge_{x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}}\langle
b\rangle\eta(\mu)\wedge\bigwedge_{x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
6.02777pt}}{\\!}\in\mathcal{H}}\neg\langle c\rangle\top\wedge\eta(x).$

By item (3) above we have $\sigma^{\prime}(x)\models\langle b\rangle\eta(\mu)$
for each $x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}$. By item (4) above we have
$\sigma^{\prime}(x)\models\neg\langle c\rangle\top$ for each
$x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}\in\mathcal{H}$. Finally, if $x\in\mathrm{var}(\Theta)$ by
item (2) above we get $\sigma^{\prime}(x)\models\eta(x)$. If
$x\not\in\mathrm{var}(\Theta)$ then we have $\eta(x)=\top$ (Definition 17.6b)
thus giving $\sigma^{\prime}(x)\models\eta(x)$ also in this case. Hence,
$\sigma^{\prime}(x)\models\eta(x)$ in all cases. Thus, we can conclude that
$\sigma^{\prime}(x)\models\xi(x)$. Since, by item (1) above,
$\sigma(x)=\sigma^{\prime}(x)$ we can conclude that $\sigma(x)\models\xi(x)$
as required.

($\Leftarrow$) Assume now that there is a $\xi\in t^{-1}(\langle
a\rangle\psi)$ such that $\sigma(x)\models\xi(x)$ for all
$x\in\mathrm{var}(t)$. Following Definition 17.4, we construct $\xi$ in terms
of some $P$-ruloid $\frac{\displaystyle\mathcal{H}}{\displaystyle
t\xrightarrow{\,{a}\,}\Theta}$ and decomposition mapping
$\eta\in\Theta^{-1}(\psi)$. In particular, we have that for each
$x\in\mathrm{var}(t)$

$\xi(x)=\bigwedge_{x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}}\langle
b\rangle\eta(\mu)\wedge\bigwedge_{x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
6.02777pt}}{\\!}\in\mathcal{H}}\neg\langle c\rangle\top\wedge\eta(x).$

We define a closed substitution $\sigma^{\prime}$ such that the following
properties hold:

    1. (a)

$\sigma^{\prime}(x)=\sigma(x)$ for all $x\in\mathrm{var}(t)$. As a
consequence, from $\sigma(x)\models\xi(x)$ we derive
$\sigma^{\prime}(x)\models\xi(x)$.

    2. (b)

As $\sigma^{\prime}(x)\models\xi(x)$, by previous item (a), we derive that
$\sigma^{\prime}(x)\models\langle b\rangle\eta(\mu)$ for each
$x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}$. This implies that for each positive
premise in $\mathcal{H}$ there exists a probability distribution $\pi_{b,\mu}$
such that $P\vdash\sigma^{\prime}(x)\xrightarrow{\,{b}\,}\pi_{b,\mu}$ and
$\pi_{b,\mu}\models\eta(\mu)$. We define $\sigma^{\prime}(\mu)=\pi_{b,\mu}$
thus obtaining that for each $x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}$ we have
$P\vdash\sigma^{\prime}(x)\xrightarrow{\,{b}\,}\sigma^{\prime}(\mu)$ and
$\sigma^{\prime}(\mu)\models\eta(\mu)$.

    3. (c)

As $\sigma^{\prime}(x)\models\xi(x)$, by previous item (a), we derive that
$\sigma^{\prime}(x)\models\neg\langle c\rangle\top$ for each
$x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}\in\mathcal{H}$. Therefore, we obtain that
$P\vdash\sigma^{\prime}(x)\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ for each
$x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}\in\mathcal{H}$.

    4. (d)

Since
$\mathrm{var}(\Theta)\subseteq\mathrm{var}(t)\cup\mathrm{rhs}(\mathcal{H})$,
previous items (b) and (c) we obtain that
$\sigma^{\prime}(\mu)\models\eta(\mu)$ for each $\mu\in\mathcal{V}\\!_{d}$.

    5. (e)

$\sigma^{\prime}(x)\models\eta(x)$ for each $x\in\mathrm{var}(\Theta)$.

From items (d), (e) and structural induction, we gather
$\sigma^{\prime}(\Theta)\models\psi$. Moreover, items (b) and (c) give
$P\vdash\sigma^{\prime}(\mathcal{H})$. Hence, by Theorem 4 we obtain
$P\vdash\sigma^{\prime}(t)\xrightarrow{\,{a}\,}\sigma^{\prime}(\Theta)$. From
item (a) we have that $\sigma^{\prime}(t)=\sigma(t)$ and, therefore, we can
conclude that $\sigma(t)\models\langle a\rangle\psi$.

Hence, the proof obligation Equation (12) follows from the two implications.

Finally, let us deal with terms that are not univariate.

Assume first that $t$ is not univariate, namely $t=\varsigma(s)$ for some
univariate $s$ and non-injective substitution
$\varsigma\colon\mathrm{var}(s)\to\mathcal{V}\\!_{s}$. Then,
$\sigma(\varsigma(s))\models\varphi$ iff there exists a decomposition mapping
$\xi^{\prime}\in s^{-1}(\varphi)$ such that
$\sigma(\varsigma(y))\models\xi^{\prime}(y)$, which by Definition 17.5 is
equivalent to require that there exists a decomposition mapping
$\xi^{\prime}\in s^{-1}(\varphi)$ such that for each $x\in\mathrm{var}(t)$ we
have $\sigma(x)\models\bigwedge_{y\in\varsigma^{-1}(x)}\xi^{\prime}(y)$. By
defining the decomposition mapping $\xi\in t^{-1}(\varphi)$ as
$\xi(x)=\bigwedge_{y\in\varsigma^{-1}(x)}\xi^{\prime}(y)$, we obtain the
thesis.

Assume now that $\Theta$ is not univariate, namely
$\Theta=\varsigma(\Theta_{1})$ for some univariate $\Theta_{1}$ and non-
injective substitution
$\varsigma\colon\mathrm{var}(\Theta_{1})\to\mathcal{V}\\!_{d}\cup\delta_{\mathcal{V}\\!_{s}}$.
Then, $\sigma(\varsigma(\Theta_{1}))\models\psi$ iff there exists a
decomposition function $\eta_{1}\in\Theta_{1}^{-1}(\psi)$ such that
$\sigma(\varsigma(z))\models\eta_{1}(z)$, which by Definition 17.7 is
equivalent to require that there exists a decomposition mapping
$\eta^{\prime}\in\Theta_{1}^{-1}(\psi)$ such that for each
$\zeta\in\mathrm{var}(\Theta)$ we have
$\eta^{\prime}(z)=\eta^{\prime}(z^{\prime})$ for all
$z,z^{\prime}\in\varsigma^{-1}(\zeta)$ and, for a chosen
$\tilde{z}\in\varsigma^{-1}(\zeta)$,
$\sigma(\zeta)\models\eta^{\prime}(\tilde{z})$. By defining the decomposition
mapping $\eta\in\Theta^{-1}(\psi)$ as $\eta(\zeta)=\eta^{\prime}(\tilde{z})$,
for $\tilde{z}\in\varsigma^{-1}(\zeta)$, we obtain the thesis. ∎

###  5.2. Decomposition of formulae in
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$

In this section we consider the logics
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$, whose decomposition can be
derived from the one for $\operatorname{\mathcal{L}}$.

######  Definition 18 (Decomposition of formulae in
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$).

Let $P=(\Sigma,\mathcal{A},R)$ be a PGSOS-PTSS and let $D_{\Sigma}$ be the
$\Sigma$-DS. The mappings
$\cdot^{-1}\colon\mathbb{T}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}\to{\mathcal{P}}(\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}))$
and
$\cdot^{-1}\colon\mathbb{DT}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{d}}}\to{\mathcal{P}}(\mathcal{V}\to\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}))$
are obtained as in Definition 17 by rewriting Definition 17.2 and Definition
17.4, respectively, by

  1. (2)

$\xi\in t^{-1}(\bar{a})$ iff there is a function $\mathfrak{f}\colon
t^{-1}(\langle a\rangle\top)\to\mathrm{var}(t)$ such that

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{\xi^{\prime}\in\mathfrak{f}^{-1}(x)}\neg\xi^{\prime}(x)&\text{if
}x\in\mathrm{var}(t)\\\ \top&\text{otherwise;}\end{cases}$

  2. (4)

$\xi\in t^{-1}(\langle a\rangle\psi)$ iff there are a ruloid
$\frac{\mathcal{H}}{t\xrightarrow{\,{a}\,}\Theta}$ and a decomposition mapping
$\eta\in\Theta^{-1}(\psi)$ such that

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}}\langle
b\rangle\eta(\mu)\;\wedge\;\bigwedge_{x\mathrel{{\xrightarrow{\,{c}\,}}\makebox[0.0pt][r]{$\not$\hskip
6.02777pt}}{\\!}\in\mathcal{H}}\bar{c}\;\wedge\;\eta(x)&\text{if
}x\in\mathrm{var}(t)\\\ \top&\text{otherwise.}\end{cases}$

Moreover, if $P$ is positive, then the mappings
$\cdot^{-1}\colon\mathbb{T}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}\to{\mathcal{P}}(\mathcal{V}\\!_{s}\to\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}))$
and
$\cdot^{-1}\colon\mathbb{DT}(\Sigma)\to(\operatorname{\operatorname{\mathcal{L}}_{\mathrm{+}}^{\mathrm{d}}}\to{\mathcal{P}}(\mathcal{V}\to\operatorname{\operatorname{\mathcal{L}}_{+}}))$
are obtained as in Definition 17 by removing Definition 17.2 and by rewriting
Definition 17.4 by

  1. (4)

$\xi\in t^{-1}(\langle a\rangle\psi)$ iff there are a positive $P$-ruloid
$\frac{\mathcal{H}}{t\xrightarrow{\,{a}\,}\Theta}$ and a decomposition mapping
$\eta\in\Theta^{-1}(\psi)$ such that

$\xi(x)=\begin{cases}\displaystyle\bigwedge_{x\xrightarrow{\,{b}\,}\mu\in\mathcal{H}}\langle
b\rangle\eta(\mu)\;\wedge\;\eta(x)&\text{if }x\in\mathrm{var}(t)\\\
\top&\text{otherwise.}\end{cases}$

We show now that by decomposing formulae in
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ (resp.
$\operatorname{\operatorname{\mathcal{L}}_{+}}$) we get formulae in
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ (resp.
$\operatorname{\operatorname{\mathcal{L}}_{+}}$). Again, this is necessary for
the precongruence theorem Theorem 8.2 (resp. Theorem 8.3), which exploits the
characterization of probabilistic ready simulation with the logic
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ (resp. the
characterization of probabilistic simulation with the logic
$\operatorname{\operatorname{\mathcal{L}}_{+}}$) given in Theorem 2 and
requires that the formulae for composed terms and those obtained for their
subterms through the decomposition method are all formulae in the
characterizing logic $\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$
(resp. $\operatorname{\operatorname{\mathcal{L}}_{+}}$).

###### Lemma 4

Let $P$ be a PGSOS-PTSS and consider the term $t\in\mathbb{T}(\Sigma)$ and the
formulae
$\varphi\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}$,
$\psi\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{d}}}$,
$\varphi^{\prime}\in\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}$
and
$\psi^{\prime}\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{+}}^{\mathrm{d}}}$.

  1. (1)

     * •

For all $x\in\mathcal{V}\\!_{s}$ we have
$\xi(x)\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}$
for each $\xi\in t^{-1}(\varphi)$.

     * •

For all $\zeta\in\mathcal{V}\\!_{d}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{d}}}$
for each $\eta\in\Theta^{-1}(\psi)$.

     * •

For all $\zeta\in\mathcal{V}\\!_{s}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}$
for each $\eta\in\Theta^{-1}(\psi)$.

  2. (2)

If $P$ is positive, then

     * •

For all $x\in\mathcal{V}\\!_{s}$ we have
$\xi(x)\in\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}$ for each
$\xi\in t^{-1}(\varphi^{\prime})$.

     * •

For all $\zeta\in\mathcal{V}\\!_{d}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{+}}^{\mathrm{d}}}$
for each $\eta\in\Theta^{-1}(\psi^{\prime})$.

     * •

For all $\zeta\in\mathcal{V}\\!_{s}$ we have
$\eta(\zeta)\in\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}$ for
each $\eta\in\Theta^{-1}(\psi^{\prime})$.

###### Proof.

The proofs of items (1) and (2) follow immediately from Definition 18. ∎

Then, we can show that also the decomposition methods for
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$ are correct.

######  Theorem 7 (Decomposition theorem II)

Let $P=(\Sigma,\mathcal{A},R)$ be a PGSOS-PTSS and $D_{\Sigma}$ be the
$\Sigma$-DS. Assume the decomposition mappings as in Definition 18. Then:

  * •

The results in Theorem 6 hold for
$\varphi\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{s}}}$
and
$\psi\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}^{\mathrm{d}}}$.

  * •

Moreover, if $P$ is positive, then the results in Theorem 6 hold for
$\varphi\in\operatorname{\operatorname{\mathcal{L}}_{+}^{\mathrm{s}}}$ and
$\psi\in\operatorname{\operatorname{\mathcal{L}}_{\mathrm{+}}^{\mathrm{d}}}$.

###### Proof.

The proof of both items can be obtained by following the one of Theorem 6 wrt.
the decompositions of the two logics (Definition 18). In particular, we remark
that in the proof for the diamond modality in
$\operatorname{\operatorname{\mathcal{L}}_{+}}$, we use Corollary 1 in place
of Theorem 4. ∎

###  5.3. (Pre)congruence theorems

To support the compositional reasoning, the congruence (resp. precongruence)
property is required for any behavioral equivalence (resp. preorder)
$\,{\mathcal{R}}\,$. It consists in verifying whether
$f(t_{1},\ldots,t_{\mathfrak{n}})\;\,{\mathcal{R}}\,\;f(t_{1}^{\prime},\ldots,t_{\mathfrak{n}}^{\prime})$
whenever $t_{i}\,{\mathcal{R}}\,t_{i}^{\prime}$ for $i=1,\ldots,\mathfrak{n}$.
In [DGL14] it is proved that probabilistic bisimilarity is a congruence for
all operators defined by a PGSOS-PTSS. We can restate this result as a direct
consequence of the characterization result of [DD11] (Theorem 1) combined with
our first decomposition result in Theorem 6. Then, by our characterization
results in Theorem 2 and our decomposition results in Theorem 7 we can derive
precongruence formats for both ready similarity and similarity.

######  Theorem 8 ((Pre)congruence theorem)

Let $P=(\Sigma,\mathcal{A},R)$ be a PGSOS-PTSS. Then:

  1. (1)

Probabilistic bisimilarity is a congruence for all operators defined by $P$;

  2. (2)

Probabilistic ready similarity is a precongruence for all operators defined by
$P$;

  3. (3)

If $P$ is positive, then probabilistic similarity is a precongruence for all
operators defined by $P$.

###### Proof.

  1. (1)

Let $t\in\mathbb{T}(\Sigma)$ and let $\sigma,\sigma^{\prime}$ be two closed
substitutions. We aim to show that

$\text{whenever }\sigma(x)\sim\sigma^{\prime}(x)\text{ for each
}x\in\mathrm{var}(t)\text{ then it holds that
}\sigma(t)\sim\sigma^{\prime}(t).$ (14)

Considering the characterization result of $\operatorname{\mathcal{L}}$ for
probabilistic bisimilarity (Theorem 1), to prove the proof obligation Equation
(14) we simply have to show that $\sigma(t)$ and $\sigma^{\prime}(t)$ satisfy
the same formulae in $\operatorname{\mathcal{L}}$. Assume that
$\sigma(t)\models\varphi$, for some state formula
$\varphi\in\operatorname{\mathcal{L}}$. By Theorem 6, there is a decomposition
mapping $\xi\in t^{-1}(\varphi)$ such that $\sigma(x)\models\xi(x)$ for each
$x\in\mathrm{var}(t)$. From Lemma 3 we gather that
$\xi(x)\in\operatorname{\operatorname{\mathcal{L}}^{\mathrm{s}}}$ and moreover
by Theorem 1 from $\sigma(x)\sim\sigma^{\prime}(x)$ we obtain that
$\sigma^{\prime}(x)\models\xi(x)$ for each $x\in\mathrm{var}(t)$. By applying
Theorem 6 once again, we obtain that $\sigma^{\prime}(t)\models\varphi$, thus
proving Equation (14).

  2. (2)

The proof for probabilistic ready simulation is analogous to the one for item
$1$ by exploiting Theorem 2.$1$ in place of Theorem 1, Theorem 7.$1$ in place
of Theorem 6 and Lemma 4.$1$ in place of Lemma 3.

  3. (3)

Under the assumption of $P$ positive, the proof for probabilistic simulation
is analogous to the one for item $1$ by exploiting Theorem 2.$2$ in place of
Theorem 1, Theorem 7.$2$ in place of Theorem 6 and Lemma 4.$2$ in place of
Lemma 3.

∎

##  6\. Conclusions

We developed a modal decomposition of formulae in $\operatorname{\mathcal{L}}$
and its subclasses
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}},\operatorname{\operatorname{\mathcal{L}}_{+}}$,
on nondeterministic probabilistic processes. The modal logic
$\operatorname{\mathcal{L}}$ was introduced in [DD11] for the characterization
of probabilistic bisimilarity and we have proved here that
$\operatorname{\operatorname{\mathcal{L}}_{\mathrm{r}}}$ and
$\operatorname{\operatorname{\mathcal{L}}_{+}}$ are powerful enough to
characterize ready similarity and similarity, respectively. Our decomposition
method is novel with respect to the ones existing in the literature (see for
instance [BFvG04, FvG16, FvGL17, FvGdW06, FvGdW12, GF12]) as it is based on
the structural operational semantics of nondeterministic probabilistic
processes in the PTS model.

The dual nature of these processes, and of the classes of formulae
characterizing them, enforced the introduction of a SOS framework tailored for
the specification of distribution terms, namely the $\Sigma$-_distribution
specification_ in which we have syntactically represented open distribution
terms as probability distributions over open terms. Moreover, the
$\Sigma$-_distribution ruloids_ , built from this new specification, provide a
general tool that can be used to support the decomposition of any modal logic
with modalities specifying quantitative properties for the PTS model.
Moreover, they can be easily adapted to models admitting subdistributions (see
among others [LdV15, LdV16]).

To prove the robustness of our decomposition method we have showed how the
congruence theorems for probabilistic bisimilarity, ready similarity and
similarity with respect to the PGSOS format can be restated as an application
of our decomposition theorems.

As future work, we will investigate the application of our decomposition
method to modal formulae characterizing different behavioral semantics for
nondeterministic probabilistic processes, as trace [BDL14, CT17, Seg95a],
testing [BDL14, DvGHM08] and weak semantics [AW06, LdV15, LdV16], and we will
derive robust (pre)congruence formats for them from their modal
characterizations, as done in [BFvG04, FvG16, FvGL17, FvGdW12] in the non
probabilistic setting.

Moreover, in [CGT16a] it is proved that by the modal logic
$\operatorname{\mathcal{L}}$ we can provide a logical characterization of the
bisimulation metric [DCPP06, DGJP04, vBW01]. Inspired by this result, we aim
to start a new research line, that is deriving the compositional properties of
a behavioral pseudometric from the modal decomposition of formulae
characterizing them. As the metric semantics provide notions of _distance_
over processes, the formats for them guarantee that a small variance in the
behavior of the subprocesses leads to a bounded small variance in the behavior
of the composed processes (_uniform continuity_ [GLT15, GLT16]). Then, we aim
to use the decomposition method to re-obtain the formats for the bisimilarity
metric proposed in [GT14, GT15, GT18] and to automatically derive original
formats for weak metric semantics [DJGP02] and metric variants of branching
bisimulation equivalence [AW06].

## References

  * [AW06] Suzana Andova and Tim A.C. Willemse.  Branching bisimulation for probabilistic systems: characteristics and decidability.  Theoret. Comput. Sci., 356(3):325–355, 2006.
  * [BDL14] Marco Bernardo, Rocco De Nicola, and Michele Loreti.  Revisiting trace and testing equivalences for nondeterministic and probabilistic processes.  Logical Methods in Computer Science, 10(1), 2014.
  * [BFvG04] Bard Bloom, Wan J. Fokkink, and Rob J. van Glabbeek.  Precongruence formats for decorated trace semantics.  ACM Trans. Comput. Log., 5(1):26–78, 2004.
  * [BIM95] Bard Bloom, Sorin Istrail, and Albert R. Meyer.  Bisimulation can’t be traced.  J. ACM, 42(1):232–268, 1995.
  * [CGT16a] Valentina Castiglioni, Daniel Gebler, and Simone Tini.  Logical characterization of bisimulation metrics.  In Proc. QAPL 2016, Electronic Proceedings in Theoretical Computer Science, 2016.
  * [CGT16b] Valentina Castiglioni, Daniel Gebler, and Simone Tini.  Modal decomposition on nondeterministic probabilistic processes.  In Proc. CONCUR 2016, pages 36:1–36:15, 2016.
  * [Cla77] Keith L. Clark.  Negation as failure.  In Logic and Data Bases, pages 293–322, 1977.
  * [CT17] Valentina Castiglioni and Simone Tini.  Logical characterization of trace metrics.  In Proceedings of QAPL@ETAPS 2017, volume 250 of EPTCS, pages 39–74, 2017.
  * [DCPP06] Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang.  Metrics for action-labelled quantitative transition systems.  Electr. Notes Theor. Comput. Sci., 153(2):79–96, 2006.
  * [DD11] Yuxin Deng and Wenjie Du.  Logical, metric, and algorithmic characterisations of probabilistic bisimulation.  CoRR, abs/1103.4577, 2011.
  * [DGJP04] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled Markov processes.  Theoret. Comput. Sci., 318(3):323–354, 2004.
  * [DGL14] Pedro R. D’Argenio, Daniel Gebler, and Matias D. Lee.  Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules.  In Proc. FoSSaCS 2014, volume 8412 of Lecture Notes in Computer Science, pages 289–303. Springer, 2014.
  * [DJGP02] Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden.  The metric analogue of weak bisimulation for probabilistic processes.  In Proc. LICS 2002, pages 413–422. IEEE Computer Society, 2002\.
  * [DL12] Pedro R. D’Argenio and Matias D. Lee.  Probabilistic transition system specification: Congruence and full abstraction of bisimulation.  In Proc. FoSSaCS 2012, volume 7213 of Lecture Notes in Computer Science, pages 452–466. Springer, 2012.
  * [DvG10] Yuxin Deng and Rob J. van Glabbeek.  Characterising probabilistic processes logically - (extended abstract).  In Proc. LPAR-17, volume 6397 of Lecture Notes in Computer Science, pages 278–293. Springer, 2010.
  * [DvGHM08] Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, and Carroll Morgan.  Characterising testing preorders for finite probabilistic processes.  Logical Methods in Computer Science, 4(4), 2008.
  * [FvG16] Wan J. Fokkink and Rob J. van Glabbeek.  Divide and congruence II: delay and weak bisimilarity.  In Logic in Computer Science, pages 778–787. ACM, 2016.
  * [FvGdW06] Wan J. Fokkink, Rob J. van Glabbeek, and Paulien de Wind.  Compositionality of Hennessy-Milner logic by structural operational semantics.  Theoret. Comput. Sci., 354(3):421–440, 2006.
  * [FvGdW12] Wan J. Fokkink, Rob J. van Glabbeek, and Paulien de Wind.  Divide and congruence: From decomposition of modal formulas to preservation of branching and $\eta$-bisimilarity.  Inf. Comput., 214:59–85, 2012.
  * [FvGL17] Wan J. Fokkink, Rob J. van Glabbeek, and Bas Luttik.  Divide and congruence III: stability & divergence.  In CONCUR, volume 85, pages 15:1–15:16. Leibniz International Proceedings in Informatics, 2017.
  * [GF12] Daniel Gebler and Wan J. Fokkink.  Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics.  In Proc. CONCUR 2012, volume 7454 of Lecture Notes in Computer Science, pages 395–409. Springer, 2012.
  * [GLT15] Daniel Gebler, Kim G. Larsen, and Simone Tini.  Compositional metric reasoning with Probabilistic Process Calculi.  In Proc. FoSSaCS’15, volume 9034 of Lecture Notes in Computer Science, pages 230–245. Springer, 2015.
  * [GLT16] Daniel Gebler, Kim G. Larsen, and Simone Tini.  Compositional metric reasoning with Probabilistic Process Calculi.  Logical Methods in Computer Science, 2016.
  * [GT14] Daniel Gebler and Simone Tini.  Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators.  In Proc. EXPRESS/SOS’14, volume 160 of EPTCS, pages 63–78, 2014.
  * [GT15] Daniel Gebler and Simone Tini.  SOS specifications of probabilistic systems by uniformly continuous operators.  In Proc. CONCUR 2015, volume 42 of LIPIcs, pages 155–168. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [GT18] Daniel Gebler and Simone Tini.  Sos specifications for uniformly continuous operators.  Journal of Computer and System Sciences, 92:113–151, 2018.
  * [HM85] Matthew Hennessy and Robin Milner.  Algebraic laws for nondeterminism and concurrency.  J. ACM, 32:137–161, 1985.
  * [LdV15] Matias D. Lee and Erik P. de Vink.  Rooted branching bisimulation as a congruence for probabilistic transition systems.  In Proc. QAPL 2015, pages 79–94, 2015.
  * [LdV16] Matias D. Lee and Erik P. de Vink.  Logical characterization of bisimulation for transition relations over probability distributions with internal actions.  In Proc. MFCS 2016, pages 29:1–29:14, 2016.
  * [LS91] Kim G. Larsen and Arne Skou.  Bisimulation through probabilistic testing.  Inf. Comput., 94(1):1–28, 1991.
  * [LT09] Ruggero Lanotte and Simone Tini.  Probabilistic bisimulation as a congruence.  ACM Trans. Comput. Log., 10:1–48, 2009.
  * [LX91] Kim G. Larsen and Liu Xinxin.  Compositionality through an operational semantics of contexts.  J. Log. Comput., 1(6):761–795, 1991.
  * [Plo81] Gordon Plotkin.  A structural approach to operational semantics.  Report DAIMI FN-19, Aarhus University, 1981.
  * [PS07] Augusto Parma and Roberto Segala.  Logical characterizations of bisimulations for discrete probabilistic systems.  In Proc. FoSSaCS 2007, pages 287–301, 2007.
  * [Seg95a] Roberto Segala.  A compositional trace-based semantics for probabilistic automata.  In Proceedings of CONCUR ’95, pages 234–248, 1995.
  * [Seg95b] Roberto Segala.  Modeling and Verification of Randomized Distributed Real-Time Systems.  PhD thesis, MIT, 1995.
  * [vBW01] Frank van Breugel and James Worrell.  An algorithm for quantitative verification of probabilistic transition systems.  In Proc. CONCUR 2001, volume 2154 of Lecture Notes in Computer Science, pages 336–350. Springer, 2001.
  * [vG96] Rob J. van Glabbeek.  The meaning of negative premises in transition system specifications II.  In Proc. ICALP’96, pages 502–513, 1996.
  * [vGSS95] Rob J. van Glabbeek, Scott A. Smolka, and Bernhard Steffen.  Reactive, generative and stratified models of probabilistic processes.  Inf. Comput., 121(1):59–80, 1995.

##  Appendix A Proofs of auxiliary results

Proof of Proposition 2. We proceed by a case analysis over the form of
$\Sigma$-distribution rules.

  * •

For $\Sigma$-distribution rules
$r_{\textsf{D}}=\\{\delta_{x}\xrightarrow{\,{1}\,}x\\}$, for some
$x\in\mathcal{V}\\!_{s}$, and $r_{\textsf{D}}=\\{c\xrightarrow{\,{1}\,}c\\}$,
for some constant function $c\in\Sigma$, the thesis is immediate.

  * •

Consider a $\Sigma$-distribution rule $r_{\textsf{D}}$ as in Definition 10.2.
Then, to prove the thesis we need to show that
$\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}}J_{i}}q_{k}=1$. We have

$\displaystyle\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}}J_{i}}q_{k}={}$
$\displaystyle\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}}J_{i}}\Big{(}\prod_{i=1}^{\mathfrak{n}}q_{i,k(i)}\Big{)}$
$\displaystyle={}$ $\displaystyle\prod_{i=1}^{\mathfrak{n}}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}$ $\displaystyle={}$
$\displaystyle\prod_{i=1}^{\mathfrak{n}}(1)$ $\displaystyle={}$ $\displaystyle
1$

where
$\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}}J_{i}}\Big{(}\prod_{i=1}^{\mathfrak{n}}q_{i,k(i)}\Big{)}=\prod_{i=1}^{\mathfrak{n}}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}$ follows by the distributive property of the summation
wrt. the product and can be formally proved by induction over $\mathfrak{n}$,
with inductive step
$\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}-1}J_{i}}\Big{(}\prod_{i=1}^{\mathfrak{n}-1}q_{i,(i)}\Big{)}=\prod_{i=1}^{\mathfrak{n}-1}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}$, as follows:

$\displaystyle\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}}J_{i}}\Big{(}\prod_{i=1}^{\mathfrak{n}}q_{i,k(i)}\Big{)}$
$\displaystyle={}$ $\displaystyle\sum_{j\in
J_{\mathfrak{n}}}q_{\mathfrak{n},j}\Bigg{(}\sum_{k\in\bigtimes_{i=1}^{\mathfrak{n}-1}J_{i}}\Big{(}\prod_{i=1}^{\mathfrak{n}-1}q_{i,k(i)}\Big{)}\Bigg{)}$
$\displaystyle={}$ $\displaystyle\sum_{j\in
J_{\mathfrak{n}}}q_{\mathfrak{n},j}\Bigg{(}\prod_{i=1}^{\mathfrak{n}-1}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}\Bigg{)}$ (inductive step) $\displaystyle={}$
$\displaystyle\Big{(}\sum_{j\in
J_{\mathfrak{n}}}q_{\mathfrak{n},j}\Big{)}\cdot\Bigg{(}\prod_{i=1}^{\mathfrak{n}-1}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}\Bigg{)}$ $\displaystyle={}$
$\displaystyle\prod_{i=1}^{\mathfrak{n}}\Big{(}\sum_{j\in
J_{i}}q_{i,j}\Big{)}.$

  * •

Finally, consider a $\Sigma$-distribution rule $r_{\textsf{D}}$ as in
Definition 10.3. Then, to prove the thesis we need to show that
$\sum_{x\in\\{x_{i,j}\mid j\in J_{i},i\in I\\}}q_{x}=1$. We have

$\displaystyle\sum_{x\in\\{x_{i,j}\mid j\in J_{i},i\in I\\}}q_{x}$
$\displaystyle={}$ $\displaystyle\sum_{x\in\\{x_{i,j}\mid j\in J_{i},i\in
I\\}}\Big{(}\sum_{i\in I,j\in J_{i}\atop\text{ s.t.
}x_{i,j}=x}p_{i}q_{i,j}\Big{)}$ $\displaystyle={}$ $\displaystyle\sum_{i\in
I}p_{i}\Big{(}\sum_{x\in\\{x_{i,j}\mid j\in J_{i},i\in I\\}\atop j\in
J_{i}\text{ s.t. }x_{i,j}=x}q_{i,j}\Big{)}$ $\displaystyle={}$
$\displaystyle\sum_{i\in I}p_{i}\Big{(}\sum_{j\in J_{i}}q_{i,j}\Big{)}$ (for
each $i\in I$ the $x_{i,j}$ are distinct) $\displaystyle={}$
$\displaystyle\sum_{i\in I}p_{i}$ $\displaystyle={}$ $\displaystyle 1.$

∎

Proof of Proposition 3. The thesis follows directly by the definition of
$\sigma(L)$. In fact, if we let
$\sigma(L)=\\{\sigma(\Theta)\xrightarrow{\,{q_{j}}\,}t_{j}\mid j\in J\\}$,
then the targets $t_{j}$ are pairwise distinct by construction and moreover we
have

$\displaystyle\sum_{j\in J}q_{j}$ $\displaystyle={}$ $\displaystyle\sum_{j\in
J}\Big{(}\sum_{\\{i\in I\mid\sigma(t_{i})=t_{j}\\}}q_{i}\Big{)}$
$\displaystyle={}$ $\displaystyle\sum_{i\in I}q_{i}$ $\displaystyle={}$
$\displaystyle 1$ $\displaystyle\text{($L$ is a distribution over terms)}.$

∎

Proof of Proposition 5. As the conclusion of a $\Sigma$-distribution ruloid
coincides with the conclusion of a reduced instance of the
$\Sigma$-distribution rule on which the $\Sigma$-distribution ruloid is built,
the thesis follows immediately from Proposition 4. ∎