Commit 51a8aa15 authored by Quentin Aristote's avatar Quentin Aristote
Browse files

conclusion

parent beedb536
......@@ -2210,7 +2210,7 @@ Then, for all $p,q \in 2$, $\chi \in [0,m-1]$, $r_{p,q}^{(\chi)} \sqsubseteq s_{
Using similar proof methods one may for example also show that when the $\mathbf{\Omega}_\sigma$ are equivalence relations (a notion that can be defined as soon as $\Omega$ is a quantale), then so is the fair $\Omega$-bisimulation.
Unfortunately, the same proof method also shows that fair $\Omega$-bisimulations are actually ordinary bisimulations as soon as the $\mathbf{\Omega}_\sigma$ are symmetric, and thus that Definition~\ref{def:fair-omega-bisimulation} fails to instantiate the fair bisimulation for B\"uchi automata.
Unfortunately, the same proof method also shows that fair $\Omega$-bisimulations are actually ordinary bisimulations as soon as the $\mathbf{\Omega}_\sigma$ are symmetric, and thus that Definition~\ref{def:fair-omega-bisimulation} fails to instantiate the fair bisimulation for B\"uchi automata. There are other way to define fair (bi)simulations, but nothing satisfying was found.
Some additional time will still be put into trying to instantiate the fair and delayed bisimulations with codensity equational systems as such a definition would give rise to new notions of quantitative fair and delayed bisimulations for B\"uchi-like automata, for which the codensity parity game point of view could give intuitive methods of showing soundness results (for instance, showing that if two states are fairly $\omega$-bisimilar then the truth values of a coalgebraic modal formula differ at most by $\omega$).
......@@ -2526,8 +2526,11 @@ Some additional time will still be put into trying to instantiate the fair and d
\section*{Conclusion}
\textit{In fine}, we developed the notion of codensity equational systems, a formalism for nested alternating fixed points involving codensity liftings, and showed that their solutions are characterized by the winning positions of well-crafted parity games called codensity parity games. From this result, we derived a new kind of parity games for model checking of coalgebraic modal logic, reminescent of the classic model checking game for classic modal logic, and which will be the topic of a future paper.
Unfortunately, we did not manage to instantiate fair and delayed bisimulations, our main motivation for developing codensity equational systems. This will be the subject of future research. \\
Still, our work on this question lead to the use of an interesting proof method that uses game semantics to derive inequalities. Formalizing and studying this proof method in a categorical framework adapted to game theory may also be the subject of future research.
\printbibliography
% \bibliography{biblio.bib}
% \bibliographystyle{splncs04}
\end{document}
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