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

fullpage

parent 8e7a0cae
\documentclass{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
......@@ -257,7 +258,7 @@ Classic modal logic is linked to game semantics via model checking games~: compu
$q \in Q_S$ & S & $q' \in Q_D$ such that $(q,q') \in E$ \\
\midrule
$q \in Q_D$ & D & $q' \in Q_S$ such that $(q,q') \in E$ \\
\bottomrule\\
\bottomrule
\end{tabular}
\caption{Possible moves in a safety game}\label{tab:safety-game}
\end{table}
......@@ -295,7 +296,7 @@ Safety games are a special case of another type of games, parity games.
$q \in Q_S$ & S & $q' \in Q$ such that $(q,q') \in E$ & $\pr(q)$ \\
\midrule
$q \in Q_D$ & D & $q' \in Q$ such that $(q,q') \in E$ & $\pr(q)$ \\
\bottomrule\\
\bottomrule
\end{tabular}
\caption{Priorities and possible moves in a parity game}\label{tab:parity-game}
\end{table}
......@@ -1035,7 +1036,7 @@ We then get a smaller game, still characterizing codensity bisimilarities, that
$P \in \mathcal{G}$ & S & \makecell{$\sigma \in \Sigma$, $k : X \rightarrow \Omega_\sigma$ such that \\ $P \not\sqsubseteq (\tau_\sigma \circ Fk \circ c)^*\mathbf{\Omega}_\sigma$} \\
\midrule
$k : X \rightarrow \Omega_\sigma$ & D & $P \in \mathcal{G}$ such that $P \not\sqsubseteq k^*\mathbf{\Omega}_\sigma$ \\
\bottomrule\\
\bottomrule
\end{tabular}
\caption{Trimmed codensity safety game}\label{tab:trimmed-codensity-safety-game}
\end{table}
......@@ -1263,10 +1264,10 @@ Just as codensity bisimilarities (greatest fixed points of the univariate predic
\begin{tabular}{c c c c}
Position & Player & Possible moves & Priority \\
\toprule
\makecell{$i \in [1,m]$ \\ $u \in \mathbb{C}_X$} & S & \makecell{$i$, $u$, $\sigma \in \Sigma$, \\ $f : X \rightarrow \Omega_{i,\sigma}^m$ such that \\ $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} & $2i + \delta_{\eta_i = \mu}$ \\
\makecell{$i \in [1,m]$, $u \in \mathbb{C}_X$} & S & \makecell{$i$, $u$, $\sigma \in \Sigma$, $f : X \rightarrow \Omega_{i,\sigma}^m$ \\ such that $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} & $2i + \delta_{\eta_i = \mu}$ \\
\midrule
\makecell{$i \in [1,m]$ \\ $u \in \mathbb{C}_X$ \\ $\sigma \in \Sigma$ \\ $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} & $0$ \\
\bottomrule\\
\makecell{$i \in [1,m]$, $u \in \mathbb{C}_X$ \\ $\sigma \in \Sigma$, $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} & $0$ \\
\bottomrule
\end{tabular}
\caption{Codensity parity game}\label{tab:codensity-parity-game}
\end{table}
......@@ -1301,12 +1302,12 @@ Note that the actual choice of $\gamma$ is only a matter of reducing the state s
\begin{tabular}{c c c}
Position & Player & Possible moves \\
\toprule
\makecell{$i \in [1,m]$ \\ $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$} & S & \makecell{$i$, $u$, $(\seq{\alpha}{k})$, $\sigma \in \Sigma$, \\ $f : X \rightarrow \Omega_{i,\sigma}^m$ such that \\ $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} \\
\makecell{$i \in [1,m]$, $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$} & S & \makecell{$i$, $u$, $(\seq{\alpha}{k})$, $\sigma \in \Sigma$, $f : X \rightarrow \Omega_{i,\sigma}^m$ \\ such that $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} \\
\midrule
\makecell{$i \in [1,m] \mid \eta_i = \mu$ \\ $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$ \\ $\sigma \in \Sigma$ \\ $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$, \\ $(\seq{\delta}{k}) \in \gamma^k$ such that \\ $(\seq{\delta}{k}) \preceq_j (\seq{\beta}{k})$, \\ $(\seq{\beta}{k}) \prec_i (\seq{\alpha}{k})$ \\ for some $(\seq{\beta}{k})$ \\ and $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} \\
\makecell{$i \in [1,m] \mid \eta_i = \mu$ \\ $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$ \\ $\sigma \in \Sigma$, $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$, $(\seq{\delta}{k}) \in \gamma^k$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$ and, for some $(\seq{\beta}{k})$, \\ $(\seq{\delta}{k}) \preceq_j (\seq{\beta}{k}) \prec_i (\seq{\alpha}{k})$} \\
\midrule
\makecell{$i \in [1,m] \mid \eta_i = \nu$ \\ $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$ \\ $\sigma \in \Sigma$ \\ $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$, \\ $(\seq{\delta}{k}) \in \gamma^k$ such that \\ $(\seq{\delta}{k}) \preceq_j (\seq{\beta}{k})$, \\ $(\seq{\beta}{k}) \preceq_i (\seq{\alpha}{k})$ \\ for some $(\seq{\beta}{k})$ \\ and $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} \\
\bottomrule\\
\makecell{$i \in [1,m] \mid \eta_i = \nu$ \\ $u \in \mathbb{C}_X$ \\ $(\seq{\alpha}{k}) \in \gamma^k$ \\ $\sigma \in \Sigma$, $f : X \rightarrow \Omega_{i,\sigma}^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathbb{C}_X$, $(\seq{\delta}{k}) \in \gamma^k$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$ and, for some $(\seq{\beta}{k})$, \\ $(\seq{\delta}{k}) \preceq_j (\seq{\beta}{k}) \preceq_i (\seq{\alpha}{k})$} \\
\bottomrule
\end{tabular}
\caption{Codensity parity game with ordinals}\label{tab:codensity-parity-game-ordinals}
\end{table}
......@@ -1516,10 +1517,10 @@ Once again, the underlying graphs of codensity parity games are quite large, but
\begin{tabular}{c c c c}
Position & Player & Possible moves & Priority \\
\toprule
\makecell{$i \in [1,m]$ \\ $u \in \mathcal{G}$} & S & \makecell{$i$, $u$, $\sigma \in \Sigma$, \\ $f : X \rightarrow \Omega^m$ such that \\ $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} & $2i + \delta_{\eta_i = \mu}$ \\
\makecell{$i \in [1,m]$, $u \in \mathcal{G}$} & S & \makecell{$i$, $u$, $\sigma \in \Sigma$, $f : X \rightarrow \Omega^m$ \\ such that $u \not\sqsubseteq (\tau_{i,\sigma} \circ F_i f \circ c_i)^*\mathbf{\Omega}_{i,\sigma}$} & $2i + \delta_{\eta_i = \mu}$ \\
\midrule
\makecell{$i \in [1,m]$ \\ $u \in \mathcal{G}$ \\ $\sigma \in \Sigma$ \\ $f : X \rightarrow \Omega^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathcal{G}$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} & $0$ \\
\bottomrule\\
\makecell{$i \in [1,m]$, $u \in \mathcal{G}$ \\ $\sigma \in \Sigma$, $f : X \rightarrow \Omega^m$} & D & \makecell{$j \in [1,m]$, $v \in \mathcal{G}$ \\ such that $v \not\sqsubseteq f_j^*\mathbf{\Omega}_{i,\sigma}$} & $0$ \\
\bottomrule
\end{tabular}
\caption{Trimmed codensity parity game}\label{tab:trimmed-codensity-parity-game}
\end{table}
......@@ -1580,7 +1581,7 @@ For completeness, Theorem~\ref{theorem:transfer-codensity-bisimilarity} was also
% This result is the immediate consequence of Lemma~\ref{lemma:transfer-predicate-transformer} and Lemma~\ref{lemma:transfer-equational-systems}.
% \end{proof}
The proof is done in two times.
The proof follows from the two following lemmas.
\begin{lemma}\label{lemma:transfer-predicate-transformer}
Assume the context of Theorem~\ref{theorem:transfer-codensity-equational-systems}. Then, for all $i \in [1,m]$ and $\seq{P}{m} \in \mathbb{C}_X$,
......
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