Commit 5b8b73fb authored by Quentin Aristote's avatar Quentin Aristote
Browse files

introduction

parent 1810298a
This diff is collapsed.
......@@ -53,6 +53,25 @@
\maketitle
\section*{Introduction}
\paragraph{Background.}
Bisimulations~\cite{milnerCommunicationConcurrency1989,parkConcurrencyAutomataInfinite1981} are a widely-used tool in software verification, as they allow to show that two transition systems, for example Kripke frames (sets of states equipped with transition functions between states) or automata (Kripke frames where some states are chosen to be accepting), have the same behavior (whether they accept the same input words for instance). In other words, by modeling a program as a transition system, one can show using bisimulations that the program behaves as expected~\cite{leroyFormalVerificationRealistic2009}.
In practice, Kripke frames or classic automata are usually too simple a framework to fully express the semantics of a program. Extensive work has thus been done in order to generalize the notion of bisimulation, mainly in three different directions. To account for new kinds of behaviours, bisimulations have been generalized to new kinds of transitions systems~: for instance, one can define a notion of bisimulation relation on probabilistic transition systems such as Markov chains~\cite{larsenBisimulationProbabilisticTesting1991}. On these probabilistic transition systems, one can also define the notion of bisimulation distance~\cite{desharnaisMetricsLabelledMarkov2004}, that not only expresses whether two states have the exact same behavior or not, but also expresses how much these states differ in behavior~: these are quantitative (instead of qualitative) bisimulations. Finally, notions of bisimulation have also been defined to take into account new kinds of accepting conditions~: for B\"uchi automata (an automata where an infinite word is accepted if a corresponding run goes an infinite amount of times through accepting states), modeling reactive systems, two states related by the fair or the delayed bisimulations will accept the same words~\cite{etessamiFairSimulationRelations2005}.
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{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}.
\paragraph{Goals.} or my internship under the supervision of \href{https://group-mmm.org/~ichiro/}{Ichiro Hasuo} 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.
% \paragraph{Structure.}
% In Section~\ref{sec:preliminaries}, we recall the definitions and results we will be using throughout the work. In Section~\ref{sec:codensity-parity-games}, after recalling the theoretical development of~\cite{komoridaCodensityGamesBisimilarity2019a}, we mimick and extend it, introducing codensity equational systems and codensity parity games and showing these two notions are equivalent. Finally in Section~\ref{sec:codensity-parity-games-bisimilarity} we show how the theoretical results could be applied to give categorical generalizations of bisimulation notions for B\"uchi automata. % we use our new theoretical results to introduce the categorical definition of fair bisimulation that instantiates our notion of fair bisimulation distance.
\bibliography{biblio.bib}
\bibliographystyle{splncs04}
......
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