Theory Strong_Bisimilarity
theory Strong_Bisimilarity
imports Labelled_Transition_Systems
begin
section ‹Strong Bisimilarity›
text ‹\label{sec:strong_bisimilarity}›
text ‹As discussed in the previous section, LTSs can describe the behaviour of reactive systems, and this behaviour is observable by the environment (in terms of the transitions performed by the system). This begets a notion of behavioural equivalence, where two processes are said to be behaviourally equivalent if they exhibit the same (observable) behaviour @{cite reactivesystems}.
Bisimilarity (or \emph{strong bisimilarity}, to be precise) is the \enquote{\emph{finest extensional behavioural equivalence} \textelp{} on processes} @{cite ‹section 0.1› introBC}, an extensional property being one that treats the system in question as a black box, i.e.\@ the specific state space of the system remains hidden and performed transitions are only observable in terms of their action-label. This distinguishes bisimilarity from stronger graph equivalences like \emph{graph isomorphism}, where the (intensional) identity of processes (graph nodes) is relevant @{cite advBC_origins}.
\example{%
The processes $p$ and $q$ are strongly bisimilar (written $p \leftrightarrow q$, following @{cite rbs}), as both can always perform exactly two a-transitions and no further transitions afterwards. There is no isomorphism between the left and right subgraphs, as they have a different number of nodes.
\lts{
\node[state] (p0) {$p$};
\node[state] (p1) [below left of=p0] {$p_1$};
\node[state] (p2) [below of=p1] {$p_2$};
\node[state] (p3) [below right of=p0] {$p_3$};
\node[state] (p4) [below of=p3] {$p_4$};
\node[state] (q0) [right of=p0,xshift=2cm] {$q$};
\node[state] (q1) [below of=q0] {$q_1$};
\node[state] (q2) [below of=q1] {$q_2$};
\path (p0) edge node[above left] {$a$} (p1)
edge node {$a$} (p3)
(p1) edge node[left] {$a$} (p2)
(p3) edge node[left] {$a$} (p4)
(q0) edge node {$a$} (q1)
(q1) edge node {$a$} (q2);
}}
\pagebreak
It is important to note that not only transitions that are performable, but also those that are not, are relevant.
\example{%
The processes $p$ and $q$ are not strongly bisimilar, as $p$ can perform an $a$-transition into a subsequent state, where it can perform no further transitions, whereas $q$ can always perform two $a$-transitions in sequence.
\lts{
\node[state] (p0) {$p$};
\node[state] (p1) [below left of=p0] {$p_1$};
\node[state] (p2) [below of=p1] {$p_2$};
\node[state] (p3) [below right of=p0] {$p_3$};
\node[state] (q0) [right of=p0,xshift=2cm] {$q$};
\node[state] (q1) [below of=q0] {$q_1$};
\node[state] (q2) [below of=q1] {$q_2$};
\path (p0) edge node[above left] {$a$} (p1)
edge node {$a$} (p3)
(p1) edge node[left] {$a$} (p2)
(q0) edge node {$a$} (q1)
(q1) edge node {$a$} (q2);
}}
Strong bisimilarity is the \emph{finest} extensional behavioural equivalence, because all actions are thought of as observable. An example of a coarser equivalence is \emph{weak bisimilarity}, which treats the aforementioned hidden action $\tau$ as unobservable. However, weak bisimilarity is of no further relevance for this thesis and the interested reader is referred to @{cite ‹Chapter 3.4› reactivesystems}.
The notion of strong bisimilarity can be formalised through \emph{strong bisimulation} (SB) relations, introduced originally by David Park in @{cite park81}. A binary relation $\mathcal{R}$ over the set of processes $\Proc$ is an SB iff for all $(p,q) \in \mathcal{R}$:
\begin{align*}
&\forall p' \in \Proc,\; \alpha \in \Act .\; p \xrightarrow{\alpha} p' \longrightarrow
\exists q' \in \Proc .\; q \xrightarrow{\alpha} q' \wedge (p',q') \in \mathcal{R}, \text{ and}\\
&\forall q' \in \Proc,\; \alpha \in \Act .\; q \xrightarrow{\alpha} q' \longrightarrow
\exists p' \in \Proc .\; p \xrightarrow{\alpha} p' \wedge (p',q') \in \mathcal{R}.
\end{align*}›
subsection ‹Isabelle›
text ‹Strong bisimulations are straightforward to formalise in Isabelle, using the \enquote{curried} definition approach discussed in \cref{chap:isabelle}.›
context lts begin
definition SB :: ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where ‹SB R ≡ ∀ p q. R p q ⟶
(∀ p' α. p ⟼α p' ⟶ (∃ q'. (q ⟼α q') ∧ R p' q')) ∧
(∀ q' α. q ⟼α q' ⟶ (∃ p'. (p ⟼α p') ∧ R p' q'))›
text ‹\pagebreak
Two processes $p$ and $q$ are then strongly bisimilar iff there is an SB that contains the pair $(p, q)$.›
definition strongly_bisimilar :: ‹'s ⇒ 's ⇒ bool›
(‹_ ↔ _› [70, 70] 70)
where ‹p ↔ q ≡ ∃ R. SB R ∧ R p q›
text ‹The following corollaries are immediate consequences of these definitions.›
corollary strongly_bisimilar_step:
assumes
‹p ↔ q›
shows
‹p ⟼a p' ⟹ (∃ q'. (q ⟼a q') ∧ p' ↔ q')›
‹q ⟼a q' ⟹ (∃ p'. (p ⟼a p') ∧ p' ↔ q')›
using assms SB_def strongly_bisimilar_def by (smt (verit))+
corollary strongly_bisimilar_symm:
assumes ‹p ↔ q›
shows ‹q ↔ p›
using assms unfolding strongly_bisimilar_def
proof
fix R
assume ‹SB R ∧ R p q›
let ?R' = ‹λ a b. R b a›
have ‹SB ?R' ∧ ?R' q p› using SB_def ‹SB R ∧ R p q› by presburger
thus ‹∃R. SB R ∧ R q p› by auto
qed
end
end