Commit 959b7a3b authored by Quentin Aristote's avatar Quentin Aristote
Browse files

small corrections

parent 1744813b
......@@ -1544,15 +1544,7 @@ This version of the game gives the first interesting instance of codensity parit
\begin{example}[Codensity parity game for model checking of \Cmu{} formulas]
Via Proposition~\ref{prop:semantics-predicate-transformer}, any equational system involving the semantics of \Cmu{} formulas can be written as a codensity equational system. The corresponding trimmed codensity parity game (with the generating set from Example~\ref{example:generating-sets}) characterizes it~: an element $x$ in the base set $X$ has truth value at least $\omega$ if and only if $\delta_x^\omega$ is a winning position in the game.
In the particular case of classic modal logic, the trimmed codensity parity game is reminescent of the classic parity game for model checking of modal formulas~\cite{gradelModelCheckingGames2002}. For exemple, in a position $(i,x) \in m \times X$,
\begin{itemize}
\item if $\phi = \phi_1 \wedge \phi_2$, $\tau$ can be written $\tau = {\wedge} \circ (\tau_1,\tau_2)$, therefore choosing $f$ such that $\top \not\sqsubseteq (\tau_1 \circ Ff_1 \circ c)(x)$ and $f_2 = \top$ (for example) is enough for having $\top \not\sqsubseteq (\tau \circ Ff \circ c)(x)$~: S chooses the subformula to play on with, as D has to reply with $(1,\delta_y^\top)$ such that $\top \not\sqsubseteq f_1(y)$~;
\item if $\phi = \phi_1 \vee \phi_2$, $\tau$ can be written $\tau = {\vee} \circ (\tau_1,\tau_2)$, therefore having $\top \not\sqsubseteq (\tau \circ Ff \circ c)(x)$ requires that $\top \not\sqsubseteq (\tau_1 \circ Ff_1 \circ c)(x)$ and $\top \not\sqsubseteq (\tau_2 \circ Ff_2 \circ c)(x)$~: D chooses the subformula to play on with~;
\item if $\phi = \square \phi'$, $\tau$ can be written $\tau = {\forall} \circ \tau'$, therefore choosing $f$ such that $\tau' \circ Ff$ is equal to $\bot$ on only one state in $c(x)$ is enough for having $\top \not\sqsubseteq (\tau \circ Ff \circ c)(x)$~: S chooses a state in $c(x)$ to play on with, as D has to reply with that very state~;
\item if $\phi = \lozenge \phi'$, $\tau$ can be written $\tau = {\exists} \circ \tau'$, therefore having $\top \not\sqsubseteq (\tau \circ Ff \circ c)(x)$ requires that $f(y) = \bot$ for all $y$ in $c(x)$~: D chooses the state in $c(x)$ to play on with.
\end{itemize}
In the particular case of classic modal logic, the trimmed codensity parity game is reminescent of the classic parity game for model checking of modal formulas~\cite{gradelModelCheckingGames2002} : the idea of S or D choosing the subformula to play on with still appears in this new game.
\end{example}
Although parity games for any kind of equational system (and thus in particular for model checking of arbitrary coalgebraic modal logic) already exist~\cite{baldanAbstractionUptoTechniques2020}, the games presented here have the advantage of being smaller (as soon as the fiber $\mathbb{C}_X$ is bigger then $\Hom(X,\Omega)$), and differ in that they are based on double negation, following the philosophy of codensity. For these reasons, a paper on model checking of coalgebraic modal logic \textit{via} codensity games will be submitted to the \href{https://etaps.org/2021/fossacs}{24th International Conference on Foundations of Software Science and Computation Structures} (FoSSaCS'21).
......@@ -1607,9 +1599,9 @@ The proof follows from the two following lemmas.
If $\family{l^\mathrm{sol}}{i}{i \in [1,m]}$ and $\family{\widetilde{l}^\mathrm{sol}}{i}{i \in [1,m]}$ are the respective solutions of the two following equational systems,
\begin{align*}
u_1 &=_{\eta_1} f_1(\seq{u}{m}) &&& \widetilde{u}_1 &=_{\eta_1} \widetilde{f}_1(\seq{\widetilde{u}}{m}) \\
&\vdots &&& &\vdots \\
u_m &=_{\eta_m} f_m(\seq{u}{m}) &&& \widetilde{u}_m &=_{\eta_m} \widetilde{f}_m(\seq{\widetilde{u}}{m})
u_1 &=_{\eta_1} f_1(\seq{u}{m}) & \widetilde{u}_1 &=_{\eta_1} \widetilde{f}_1(\seq{\widetilde{u}}{m}) \\
&\vdots & &\vdots \\
u_m &=_{\eta_m} f_m(\seq{u}{m}) & \widetilde{u}_m &=_{\eta_m} \widetilde{f}_m(\seq{\widetilde{u}}{m})
\end{align*}
then for all $i \in [1,m]$,
\[ T\left(l^\mathrm{sol}_i\right) = \widetilde{l}^\mathrm{sol}_i \]
......
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