Commit beedb536 authored by Quentin Aristote's avatar Quentin Aristote
Browse files

removed comma in introduction

parents f232c745 02ee2069
......@@ -67,7 +67,7 @@ In practice, Kripke frames or classic automata are usually too simple a framewor
In many cases finding under-approximations of the bisimulation is enough, as, for instance, to show that two states have the same behavior it suffices to compute whether these two states in particular are bisimilar and it is not necessary to compute the whole relation. For several notions of bisimulation, these under-approximations can be characterized through game theory by winning positions in well-crafted games~\cite{stirlingBisimulationModalLogic1999,fijalkowExpressivenessProbabilisticModal2017,konigMetricBisimulationGames2018,henzingerFairSimulation2002}. \\
Members of the \href{https://group-mmm.org/eratommsd/about-2/}{Erato MMSD Project}, introduced a category theoretical framework, codensity liftings, which instantiates many different notions of bisimulation~\cite{sprungerFibrationalBisimulationsQuantitative2018}. Using this framework, a categorical link between bisimulations and game theory was then established by introducing the codensity safety game that characterizes these notions of bisimulation~\cite{komoridaCodensityGamesBisimilarity2019a}. Altough the categorical setting allows for the definition of new bisimilarity-like notions, these works only deal with bisimulations that can be expressed as greatest fixed point, which is not enough for complex acceptance conditions. For example, the fair and delayed bisimulations fail to be instantiated by this framework as they are characterized by parity games, i.e.\ nested alternating fixed points~\cite{hasuoLatticetheoreticProgressMeasures2016}.
Members of the \href{https://group-mmm.org/eratommsd/about-2/}{Erato MMSD Project} introduced a category theoretical framework, codensity liftings, which instantiates many different notions of bisimulation~\cite{sprungerFibrationalBisimulationsQuantitative2018}. Using this framework, a categorical link between bisimulations and game theory was then established by introducing the codensity safety game that characterizes these notions of bisimulation~\cite{komoridaCodensityGamesBisimilarity2019a}. Altough the categorical setting allows for the definition of new bisimilarity-like notions, these works only deal with bisimulations that can be expressed as greatest fixed point, which is not enough for complex acceptance conditions. For example, the fair and delayed bisimulations fail to be instantiated by this framework as they are characterized by parity games, i.e.\ nested alternating fixed points~\cite{hasuoLatticetheoreticProgressMeasures2016}.
\paragraph{Goals.}
During my internship, under the supervision of \href{https://group-mmm.org/~ichiro/}{Ichiro Hasuo} and \href{https://group-mmm.org/~dubut/}{J\'er\'emy Dubut}, I thus visited the T\=oky\=o site of the Erato MMSD Project in order to extend these previous works to nested alternating fixed points, by characterizing their under-approximants as winning positions in well-crafted games. The hope was then that this would enable generalizations of fair and delayed (bi)simulations, in particular to bisimulation distances for B\"uchi-like probabilistic transition systems.
......@@ -1811,7 +1811,6 @@ Recall now from Example~\ref{example:codensity-bisimulations} that if $r^\mathrm
\[\left(\forall x' \in c(x), \exists y' \in c(y), r^{eq}(x',y')\right) \wedge \left(\forall y' \in c(y), \exists x' \in c(x), r^{eq}(y',x')\right)\]
holds if and only if $\Phi_c^{{\Leftrightarrow},\exists}\left(r\right)(x,y) = 1$. As the fair bisimulation is an equivalence relation, it thus makes sense to generalize the fair bisimulation to other complete lattices $\Omega$ as follows. In this definition the role of $\mathbf{\Omega}_{i,j,\epsilon}$ and $\tau_\epsilon$ is to make sure $\mathrm{fbisim}_{i,j}^{(b)}$ is equal to $\bot$ outside of $X_i \times X_j$.
% \begin{definition}[fair $\Omega$-bisimulation]\label{def:fair-omega-bisimulation}
% Let $\mathcal{A} = (X_1,X_2,\Sigma,c : X \rightarrow FX)$, with $X = X_1 + X_2$, be a B\"uchi-like transition system for a functor $F$, and let $\Omega$ be a complete lattice. For $\tau = (\tau_\sigma : F\Omega_\sigma \rightarrow \Omega_\sigma)_{\sigma \in \Sigma}$ and $\mathbf{\Omega} = (\mathbf{\Omega}_\sigma : \Omega_\sigma^2 \rightarrow \Omega_\sigma)_{\sigma \in \Sigma}$, we define Equational System~\eqref{eq:fair-omega-bisimulation-codensity-equational-system} (read in columns), the \emph{equational system for fair $\Omega$-bisimulation} of $\mathcal{A}$, computed in $\ERel{} \rightarrow \mathbf{Set}$.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment