PBES Generation

Wieger Wesselink, Tim Willemse

This document describes the generation of PBESs. These algorithms are implemented in the tools lps2pbes and lpsbisim2pbes.

Transforming an LPS and a property to a PBES

In this section we define the algorithm $\operatorname{lps2pbes}$ that generates a PBES from a modal mu-calculus property $\varphi$ and an LPS. Let $\langle D_p, d_0, P \rangle$ be the LPS given by

$\begin{array}{lrl} \mathbf{proc}~P(x{:}D_p) &=& \sum_{i\in I}\sum_{y_i:E_i} c_i(x,y_i) \rightarrow a_i(f_i(x,y_i)) @ t_i(x,y_i) \cdot P(g_i(x,y_i)) \\ &+& \sum_{j\in J}\sum_{y_j:E_j} c_j(x,y_j) \rightarrow \delta @ t_j(x,y_j); \end{array}$

where $a_i(f_i(x,y))$ is a multiset of actions. Then we define

$\operatorname{lps2pbes}(\sigma X(x_f{:}D_f{:=}d).\,\varphi,\, \langle D_p, d_0, P \rangle) = \mathbf{E}(\varphi),$

where the function $\mathbf{E}$ is inductively defined using the tables below. The function $\varphi$ has to be in positive normal form, i.e. it may not contain any $\lnot$ or $\Rightarrow$ symbols. There is also an untimed variant of the algorithm, which can be obtained by removing all time references. A formula $\varphi$ not of the form $\sigma X(x_f{:}D_f{:=}d).\,\varphi$ is first translated into $\nu X().\,\varphi$ . We assume that $T{:}\mathbb{R}$ is a unique fresh time variable that is generated by the algorithm. We denote the formula $\varphi$ that is passed to the algorithm $\operatorname{lps2pbes}$ as $\varphi_0$ . It is used as a global variable in the translation.

Let $a = \{a_1,\ldots,a_n\}$ and $b = \{b_1,\ldots,b_n\}$ be two multiactions. Let $A$ be the set of all permutations $[i_1,\ldots,i_n]$ of $[1,\ldots,n]$ such that $\mathit{name}(a_k) = \mathit{name}(b_{i_k})$ for $k = 1\ldots n$ . Then we define the function $\mathbf{Sat}$ as follows:

$\begin{array}{lll} \mathbf{Sat}(a@t,\, b) &=_{\mathit{def}}& \left\{\begin{array}{ll} \bigvee_{[i_1,\ldots,i_n]\in A}\bigwedge_{k=1\ldots n}(a_k = b_{i_k}) & \text{if } A \neq \emptyset \\ \mathit{false} & \text{otherwise} \end{array}\right. \\[4pt] \mathbf{Sat}(a@t,\, c) &=_{\mathit{def}}& c \\ \mathbf{Sat}(a@t,\, \alpha@u) &=_{\mathit{def}}& \mathbf{Sat}(a@t,\alpha) \wedge t \approx u \\ \mathbf{Sat}(a@t,\, \lnot\alpha) &=_{\mathit{def}}& \lnot\,\mathbf{Sat}(a@t,\alpha) \\ \mathbf{Sat}(a@t,\, \alpha\wedge\beta) &=_{\mathit{def}}& \mathbf{Sat}(a@t,\alpha) \wedge \mathbf{Sat}(a@t,\beta) \\ \mathbf{Sat}(a@t,\, \alpha\vee\beta) &=_{\mathit{def}}& \mathbf{Sat}(a@t,\alpha) \vee \mathbf{Sat}(a@t,\beta) \\ \mathbf{Sat}(a@t,\, \alpha\Rightarrow\beta) &=_{\mathit{def}}& \mathbf{Sat}(a@t,\alpha) \Rightarrow \mathbf{Sat}(a@t,\beta) \\ \mathbf{Sat}(a@t,\, \forall x{:}D.\,\alpha) &=_{\mathit{def}}& \forall y{:}D.\,\mathbf{Sat}(a@t,\alpha[x:=y]) \\ \mathbf{Sat}(a@t,\, \exists x{:}D.\,\alpha) &=_{\mathit{def}}& \exists y{:}D.\,\mathbf{Sat}(a@t,\alpha[x:=y]) \end{array}$

$\begin{array}{lll} \mathbf{Par}_{X,l}(c) &=_{\mathit{def}}& [] \\ \mathbf{Par}_{X,l}(\lnot\varphi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi) \\ \mathbf{Par}_{X,l}(\varphi\wedge\psi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi)\,{+\!\!+}\,\mathbf{Par}_{X,l}(\psi) \\ \mathbf{Par}_{X,l}(\varphi\vee\psi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi)\,{+\!\!+}\,\mathbf{Par}_{X,l}(\psi) \\ \mathbf{Par}_{X,l}(\varphi\Rightarrow\psi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi)\,{+\!\!+}\,\mathbf{Par}_{X,l}(\psi) \\ \mathbf{Par}_{X,l}([\alpha]\varphi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi) \\ \mathbf{Par}_{X,l}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \mathbf{Par}_{X,l}(\varphi) \\ \mathbf{Par}_{X,l}(\forall x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{Par}_{X,l\,{+\!\!+}\,[x{:}D]}(\varphi) \\ \mathbf{Par}_{X,l}(\exists x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{Par}_{X,l\,{+\!\!+}\,[x{:}D]}(\varphi) \\ \mathbf{Par}_{X,l}(Y(d_f)) &=_{\mathit{def}}& [] \\ \mathbf{Par}_{X,l}(\sigma Y(x_f{:}D_f{:=}d).\,\varphi) &=_{\mathit{def}}& \left\{\begin{array}{ll} l & \text{if } Y = X \\ \mathbf{Par}_{X,l\,{+\!\!+}\,[x_f{:}D_f]}(\varphi) & \text{if } Y \neq X \end{array}\right. \\[4pt] \mathbf{Par}_{X,l}(\nabla(t)) &=_{\mathit{def}}& [] \\ \mathbf{Par}_{X,l}(\Delta(t)) &=_{\mathit{def}}& [] \end{array}$

$\begin{array}{lll} \mathbf{RHS}(c) &=_{\mathit{def}}& c \\ \mathbf{RHS}(\varphi\wedge\psi) &=_{\mathit{def}}& \mathbf{RHS}(\varphi) \wedge \mathbf{RHS}(\psi) \\ \mathbf{RHS}(\varphi\vee\psi) &=_{\mathit{def}}& \mathbf{RHS}(\varphi) \vee \mathbf{RHS}(\psi) \\ \mathbf{RHS}(\forall x{:}D.\,\varphi) &=_{\mathit{def}}& \forall x{:}D.\,\mathbf{RHS}(\varphi) \\ \mathbf{RHS}(\exists x{:}D.\,\varphi) &=_{\mathit{def}}& \exists x{:}D.\,\mathbf{RHS}(\varphi) \\ \mathbf{RHS}([\alpha]\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigwedge_{i\in I}\forall_{y:E_i}\bigl( \bigl(\mathbf{Sat}(a_i(f_i(x,y))@t_i(x,y),\alpha) \wedge c_i(x,y) \wedge t_i(x,y) > T\bigr) \\ \quad\Rightarrow \mathbf{RHS}(\varphi)[T,x:=t_i(x,y),g_i(x,y)]\bigr) \end{array} \\[4pt] \mathbf{RHS}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigvee_{i\in I}\exists_{y:E_i}\bigl( \mathbf{Sat}(a_i(f_i(x,y))@t_i(x,y),\alpha) \wedge c_i(x,y) \wedge t_i(x,y) > T \\ \quad\wedge\,\mathbf{RHS}(\varphi)[T,x:=t_i(x,y),g_i(x,y)]\bigr) \end{array} \\[4pt] \mathbf{RHS}(X(e)) &=_{\mathit{def}}& X(T,\, e,\, x,\, \mathbf{Par}_{X,[]}(\varphi_0)) \\ \mathbf{RHS}(\sigma X(x_f{:}D_f{:=}e).\,\varphi) &=_{\mathit{def}}& X(T,\, e,\, x,\, \mathbf{Par}_{X,[]}(\varphi_0)) \\ \mathbf{RHS}(\nabla(t)) &=_{\mathit{def}}& \left(\bigwedge_{i\in I\cup J}\forall_{y:E_i} (\lnot c_i(x,y) \vee t > t_i(x,y))\right) \wedge t > T \\ \mathbf{RHS}(\Delta(t)) &=_{\mathit{def}}& \left(\bigvee_{i\in I\cup J}\exists_{y:E_i} (c_i(x,y) \wedge t \leq t_i(x,y))\right) \vee t \leq T \end{array}$

$\begin{array}{lll} \mathbf{E}(c) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\varphi\wedge\psi) &=_{\mathit{def}}& \mathbf{E}(\varphi)\,\mathbf{E}(\psi) \\ \mathbf{E}(\varphi\vee\psi) &=_{\mathit{def}}& \mathbf{E}(\varphi)\,\mathbf{E}(\psi) \\ \mathbf{E}(\forall x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(\exists x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}([\alpha]\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(\nabla) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\nabla(t)) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\Delta) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\Delta(t)) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(X(e)) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\sigma X(x_f{:}D_f{:=}e).\,\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigl(\sigma X(T{:}\mathbb{R},\; x_f{:}D_f,\; x{:}D_p,\; \mathbf{Par}_{X,[]}(\varphi_0)) = \mathbf{RHS}(\varphi)\bigr)\, \mathbf{E}(\varphi) \end{array} \end{array}$

Counter example generation

There is a modified translation that adds information to the PBES from which a counter example can be generated. Note that counter example generation is only available for the untimed case. The function $\mathbf{RHS}$ is adapted from

$\begin{array}{lll} \mathbf{RHS}([\alpha]\varphi) &=_{\mathit{def}}& \bigwedge_{i\in I}\forall_{y:E_i}\bigl( (\mathbf{Sat}(a_i(f_i(x,y)),\alpha) \wedge c_i(x,y)) \Rightarrow \mathbf{RHS}(\varphi)[x:=g_i(x,y)]\bigr) \\[4pt] \mathbf{RHS}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \bigvee_{i\in I}\exists_{y:E_i}\bigl( (\mathbf{Sat}(a_i(f_i(x,y)),\alpha) \wedge c_i(x,y)) \wedge \mathbf{RHS}(\varphi)[x:=g_i(x,y)]\bigr) \end{array}$

into

$\begin{array}{lll} \mathbf{RHS}([\alpha]\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigwedge_{i\in I}\forall_{y:E_i} \bigl(\mathbf{Sat}(a_i(f_i(x,y)),\alpha) \wedge c_i(x,y)\bigr) \Rightarrow \\ \quad\bigl(\bigl(\mathbf{RHS}(\varphi)[x:=g_i(x,y)] \wedge Z_{a_i}^{+}(x,f_i(x,y),g_i(x,y))\bigr) \vee Z_{a_i}^{-}(x,f_i(x,y),g_i(x,y))\bigr) \end{array} \\[4pt] \mathbf{RHS}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigvee_{i\in I}\exists_{y:E_i} \bigl(\mathbf{Sat}(a_i(f_i(x,y)),\alpha) \wedge c_i(x,y)\bigr) \wedge \\ \quad\bigl(\bigl(\mathbf{RHS}(\varphi)[x:=g_i(x,y)] \vee Z_{a_i}^{-}(x,f_i(x,y),g_i(x,y))\bigr) \wedge Z_{a_i}^{+}(x,f_i(x,y),g_i(x,y))\bigr) \end{array} \end{array}$

where $\nu Z_{a_i}^+(x,f_i(x,y),d') = \mathit{true}$ and $\nu Z_{a_i}^-(x,f_i(x,y),d') = \mathit{false}$ are additional equations for every $a_i$ that appears in the LPS.

Transforming an LTS and a property to a PBES

In this section we define the algorithm $\operatorname{lts2pbes}$ that generates a PBES from a modal mu-calculus formula $\varphi$ and an LTS $\langle S, \mathit{Act}, \rightarrow, s_0 \rangle$ :

$\operatorname{lts2pbes}(\sigma X(d{:}D{:=}e).\,\varphi,\, \langle S, \mathit{Act}, {\rightarrow}, s_0 \rangle) = \langle \mathbf{E}_{\sigma X(d:D:=e).\,\varphi}(\varphi),\; X_{s_0}(e) \rangle$

where the function $\mathbf{E}$ is inductively defined using the tables below. The function $\varphi$ has to be in positive normal form, i.e. it may not contain any $\lnot$ or $\Rightarrow$ symbols. A formula $\psi$ not of the form $\sigma X(d{:}D{:=}e).\,\varphi$ is translated into $\nu X().\,\psi$ . We denote the formula $\varphi$ that is passed to the algorithm $\operatorname{lts2pbes}$ as $\varphi_0$ . It is used as a global variable in the translation.

The functions $\mathbf{Sat}$ and $\mathbf{Par}$ are defined in the section about $\operatorname{lps2pbes}$ .

$\begin{array}{lll} \mathbf{E}(c) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\varphi\wedge\psi) &=_{\mathit{def}}& \mathbf{E}(\varphi)\,\mathbf{E}(\psi) \\ \mathbf{E}(\varphi\vee\psi) &=_{\mathit{def}}& \mathbf{E}(\varphi)\,\mathbf{E}(\psi) \\ \mathbf{E}(\forall x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(\exists x{:}D.\,\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}([\alpha]\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(\langle\alpha\rangle\varphi) &=_{\mathit{def}}& \mathbf{E}(\varphi) \\ \mathbf{E}(X(d)) &=_{\mathit{def}}& \epsilon \\ \mathbf{E}(\sigma X(d{:}D{:=}e).\,\varphi) &=_{\mathit{def}}& \begin{array}[t]{l} \bigl(\sigma \{X_s(d{:}D,\, \mathbf{Par}_{X,[]}(\varphi_0)) = \mathbf{RHS}_\varphi(\varphi,s) \mid s \in S\}\bigr)\,\mathbf{E}(\varphi) \end{array} \end{array}$

$\begin{array}{lll} \mathbf{RHS}(c,\, s) &=_{\mathit{def}}& c \\ \mathbf{RHS}(\varphi\wedge\psi,\, s) &=_{\mathit{def}}& \mathbf{RHS}(\varphi,s) \wedge \mathbf{RHS}(\psi,s) \\ \mathbf{RHS}(\varphi\vee\psi,\, s) &=_{\mathit{def}}& \mathbf{RHS}(\varphi,s) \vee \mathbf{RHS}(\psi,s) \\ \mathbf{RHS}(\forall d{:}D.\,\varphi,\, s) &=_{\mathit{def}}& \forall d{:}D.\,\mathbf{RHS}(\varphi,s) \\ \mathbf{RHS}(\exists d{:}D.\,\varphi,\, s) &=_{\mathit{def}}& \exists d{:}D.\,\mathbf{RHS}(\varphi,s) \\ \mathbf{RHS}([\alpha]\varphi,\, s) &=_{\mathit{def}}& \bigwedge\bigl\{\mathbf{Sat}(a(x),\alpha) \Rightarrow \mathbf{RHS}_{\varphi_0}(\varphi,t) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \\ \mathbf{RHS}(\langle\alpha\rangle\varphi,\, s) &=_{\mathit{def}}& \bigvee\bigl\{\mathbf{Sat}(a(x),\alpha) \wedge \mathbf{RHS}_{\varphi_0}(\varphi,t) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \\ \mathbf{RHS}(X(e),\, s) &=_{\mathit{def}}& X_s(e,\, \mathbf{Par}_{X,[]}(\varphi_0)) \\ \mathbf{RHS}(\sigma X(d{:}D{:=}e).\,\varphi,\, s) &=_{\mathit{def}}& X_s(e,\, \mathbf{Par}_{X,[]}(\varphi_0)) \end{array}$

Counter example generation

There is a modified translation that adds information to the PBES from which a counter example can be generated. The function $\mathbf{RHS}$ is adapted from

$\begin{array}{lll} \mathbf{RHS}([\alpha]\varphi,\, s) &=_{\mathit{def}}& \bigwedge\bigl\{\mathbf{Sat}(a(x),\alpha) \Rightarrow \mathbf{RHS}_{\varphi_0}(\varphi,t) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \\[4pt] \mathbf{RHS}(\langle\alpha\rangle\varphi,\, s) &=_{\mathit{def}}& \bigvee\bigl\{\mathbf{Sat}(a(x),\alpha) \wedge \mathbf{RHS}_{\varphi_0}(\varphi,t) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \end{array}$

into

$\begin{array}{lll} \mathbf{RHS}([\alpha]\varphi,\, s) &=_{\mathit{def}}& \bigwedge\bigl\{\mathbf{Sat}(a(x),\alpha) \Rightarrow \bigl((\mathbf{RHS}(\varphi,t) \wedge Z_a^+(s,x,t)) \vee Z_a^-(s,x,t)\bigr) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \\[4pt] \mathbf{RHS}(\langle\alpha\rangle\varphi,\, s) &=_{\mathit{def}}& \bigvee\bigl\{\mathbf{Sat}(a(x),\alpha) \wedge \bigl((\mathbf{RHS}(\varphi,t) \vee Z_a^-(s,x,t)) \wedge Z_a^+(s,x,t)\bigr) \mid s \overset{a(x)}{\rightarrow} t\bigr\} \end{array}$

where $\nu Z_a^+(s,d_x,t) = \mathit{true}$ and $\nu Z_a^-(s,d_x,t) = \mathit{false}$ are additional equations for every $a(x)$ that appears in the LTS.

Bisimulation

Let

$\begin{array}{lcl} M(d) &=& \sum_{i\in I_M}\sum_{e:E_i} c_i(d,e) \rightarrow a_i(d,e) \cdot M(g_i(d,e)) \\ S(d) &=& \sum_{i\in I_S}\sum_{e:E_i} c_i(d,e) \rightarrow a_i(d,e) \cdot S(g_i(d,e)) \end{array}$

be two linear processes, such that $I_M \cap I_S = \emptyset$ . $M$ is called the model and $S$ the specification. The expression $a_i(d,e)$ can be a multiaction, or have the special value $\tau$ . We assume that there are no $\delta$ summands. We define four PBES equation systems that express some kind of bisimulation equivalence between $M$ and $S$ .

Branching bisimulation

$\mathit{brbsim}(M,S) = \nu E_2\,\mu E_1$ , where

$\begin{array}{ccl} E_2 &:=& \{X^{M,S}(d,d') = \mathit{match}^{M,S}(d,d') \wedge \mathit{match}^{S,M}(d',d), \\ & & \phantom{\{} X^{S,M}(d',d) = X^{M,S}(d,d')\} \\[4pt] E_1 &:=& \{Y_i^{M,S}(d,d',e) = \mathit{close}_i^{M,S}(d,d',e) \mid i\in I_M, \\ & & \phantom{\{} Y_i^{S,M}(d',d,e) = \mathit{close}_i^{S,M}(d',d,e) \mid i\in I_S\} \end{array}$

with for all $i\in I_p$ and $(p,q)\in\{(M,S),(S,M)\}$ :

$\begin{array}{lcl} \mathit{match}^{p,q}(d,d') &=& \bigwedge_{i\in I_p}\forall_{e:E_i}.\bigl(c_i(d,e) \Rightarrow Y_i^{p,q}(d,d',e)\bigr) \\[4pt] \mathit{close}_i^{p,q}(d,d',e) &=& \begin{array}[t]{l} \bigvee_{\{j\in I_q \mid a_j=\tau\}}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge Y_i^{p,q}(d,g_j(d',e'),e)\bigr) \\ \vee\,\bigl(X^{p,q}(d,d') \wedge \mathit{step}_i^{p,q}(d,d',e)\bigr) \end{array} \\[8pt] \mathit{step}_i^{p,q}(d,d',e) &=& \left\{\begin{array}{cl} a_i = \tau{:} & \begin{array}[t]{l} X^{p,q}(g_i(d,e),d') \vee{} \\ \bigvee_{\{j\in I_q \mid a_j=\tau\}}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge X^{p,q}(g_i(d,e),g_j(d',e'))\bigr) \end{array} \\[8pt] a_i \neq \tau{:} & \bigvee_{\{j\in I_q \mid a_j=a_i\}}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge (a_i(d,e) = a_j(d',e')) \wedge X^{p,q}(g_i(d,e),g_j(d',e'))\bigr) \end{array}\right. \end{array}$

Strong bisimulation

$\mathit{sbisim}(M,S) = \nu E$ , where

$\begin{array}{ccl} E &:=& \{X^{M,S}(d,d') = \mathit{match}^{M,S}(d,d') \wedge \mathit{match}^{S,M}(d',d), \\ & & \phantom{\{} X^{S,M}(d',d) = X^{M,S}(d,d')\} \end{array}$

with for all $i\in I_p$ and $(p,q)\in\{(M,S),(S,M)\}$ :

$\begin{array}{lcl} \mathit{match}^{p,q}(d,d') &=& \bigwedge_{i\in I_p}\forall_{e:E_i}.\bigl(c_i(d,e) \Rightarrow \mathit{step}_i^{p,q}(d,d',e)\bigr) \\[4pt] \mathit{step}_i^{p,q}(d,d',e) &=& \bigvee_{j\in I_q}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge (a_i(d,e) = a_j(d',e')) \wedge X^{p,q}(g_i(d,e),g_j(d',e'))\bigr) \end{array}$

Weak bisimulation

$\mathit{wbisim}(M,S) = \nu E_2\,\mu E_1$ , where

$\begin{array}{ccl} E_3 &:=& \{X^{M,S}(d,d') = \mathit{match}^{M,S}(d,d') \wedge \mathit{match}^{S,M}(d',d), \\ & & \phantom{\{} X^{S,M}(d',d) = X^{M,S}(d,d')\} \\[4pt] E_2 &:=& \{Y_{1,i}^{M,S}(d,d',e) = \mathit{close}_{1,i}^{M,S}(d,d',e) \mid i\in I_M, \\ & & \phantom{\{} Y_{2,i}^{M,S}(d,d') = \mathit{close}_{2,i}^{M,S}(d,d') \mid i\in I_M, \\ & & \phantom{\{} Y_{1,i}^{S,M}(d',d,e) = \mathit{close}_{1,i}^{S,M}(d',d,e) \mid i\in I_S, \\ & & \phantom{\{} Y_{2,i}^{S,M}(d',d) = \mathit{close}_{2,i}^{S,M}(d',d) \mid i\in I_S\} \end{array}$

with for all $i\in I_p$ and $(p,q)\in\{(M,S),(S,M)\}$ :

$\begin{array}{lcl} \mathit{match}^{p,q}(d,d') &=& \bigwedge_{i\in I_p}\forall_{e:E_i}.\bigl(c_i(d,e) \Rightarrow Y_{1,i}^{p,q}(d,d',e)\bigr) \\[4pt] \mathit{close}_{1,i}^{p,q}(d,d',e) &=& \begin{array}[t]{l} \left(\bigvee_{\{j\in I_q \mid a_j=\tau\}}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge Y_{1,i}^{p,q}(d,g_j(d',e'),e)\bigr)\right) \vee\,\mathit{step}_i^{p,q}(d,d',e) \end{array} \\[8pt] \mathit{step}_i^{p,q}(d,d',e) &=& \left\{\begin{array}{cl} a_i = \tau{:} & \mathit{close}_{2,i}^{p,q}(g_i(d,e),d') \\[4pt] a_i \neq \tau{:} & \bigvee_{j\in I_q}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge a_i(d,e) = a_j(d',e') \wedge \mathit{close}_{2,i}^{p,q}(g_i(d,e),g_j(d',e'))\bigr) \end{array}\right. \\[8pt] \mathit{close}_{2,i}^{p,q}(d,d') &=& X^{p,q}(d,d') \vee \bigvee_{\{j\in I_q \mid a_j=\tau\}}\exists_{e':E_j}.\bigl(c_j(d',e') \wedge Y_{2,i}^{p,q}(d,g_j(d',e'))\bigr) \end{array}$

Branching simulation equivalence

$\mathit{brsimeq}(M,S) = \nu E_2\,\mu E_1$ , where

$\begin{array}{ccl} E_2 &:=& \{X^{M,S}(d,d') = \mathit{match}^{M,S}(d,d') \wedge \mathit{match}^{S,M}(d',d), \\ & & \phantom{\{} X^{M,S}(d,d') = X^{S,M}(d',d), \\ & & \phantom{\{} X^{S,M}(d',d) = X^{M,S}(d,d')\} \\[4pt] E_1 &:=& \{Y_i^{M,S}(d,d',e) = \mathit{close}_i^{M,S}(d,d',e) \mid i\in I_M, \\ & & \phantom{\{} Y_i^{S,M}(d',d,e) = \mathit{close}_i^{S,M}(d',d,e) \mid i\in I_S\} \end{array}$

with $\mathit{match}$ , $\mathit{close}$ , and $\mathit{step}$ defined exactly the same as in branching bisimulation.