Theory HML_SRBB
text ‹\newpage›
section ‹ Stability-Respecting Branching Bisimilarity (HML$_\text{SRBB}$) \label{sect:hmlSRBB} ›
theory HML_SRBB
imports Main LTS_Semantics
begin
text ‹This section describes the largest subset of the full HML language in section \ref{sect:HML} that we are
using for purposes of silent step spectroscopy. It is supposed to characterize the most fine grained
behavioural equivalence that we may decide: Stability-Respecting Branching Bisimilarity (SRBB). While
there are good reasons to believe that this subset truly characterizes SRBB (c.f.\cite{bisping2023lineartimebranchingtime}),
we do not provide a formal proof. From this sublanguage smaller subsets are derived
via the notion of expressiveness prices (\ref{sect:ExpressivenessMeasure}). ›
text ‹
The mutually recursive data types @{term ‹hml_srbb›}, @{term ‹hml_srbb_inner›} and @{term ‹hml_srbb_conjunct›}
represent the subset of all @{term ‹hml›} formulas, which characterize stability-respecting branching
bisimilarity (abbreviated to 'SRBB').
\\\\
When a parameter is of type @{term ‹hml_srbb›} we typically use ‹φ› as a name,
for type @{term ‹hml_srbb_inner›} we use ‹χ› and for type @{term ‹hml_srbb_conjunct›} we use ‹ψ›.
The data constructors are to be interpreted as follows:
\begin{itemize}
\item in @{term ‹hml_srbb›}:
\begin{itemize}
\item @{term ‹TT›} encodes ‹⊤›
\item ‹(Internal χ)› encodes ‹⟨ε⟩χ›
\item ‹(ImmConj I ψs)› encodes $\bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
\end{itemize}
\item in @{term ‹hml_srbb_inner›}
\begin{itemize}
\item ‹(Obs α φ)› encodes ‹(α)φ› (Note the difference to \cite{bisping2023lineartimebranchingtime})
\item ‹(Conj I ψs)› encode $\bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
\item ‹(StableConj I ψs)› encodes $\neg\langle\tau\rangle\top \land \bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
\item ‹(BranchConj α φ I ψs)› encodes $(\alpha)\varphi \land \bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
\end{itemize}
\item in @{term ‹hml_srbb_conjunct›}
\begin{itemize}
\item ‹(Pos χ)› encodes ‹⟨ε⟩χ›
\item ‹(Neg χ)› encodes ‹¬⟨ε⟩χ›
\end{itemize}
\end{itemize}
For justifications regarding the explicit inclusion of @{term ‹TT›} and
the encoding of conjunctions via index sets @{term ‹I›} and mapping from indices to conjuncts @{term ‹ψs›},
reference the @{term ‹TT›} and @{term ‹Conj›} data constructors of the type @{term ‹hml›} in section \ref{sect:HML}.
›