AGV 6.6 -- Express QPTL using S1S
Previous chapter: Monadic Second-Order Logic of One Successor (S1S)
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
We already showed, in Theorem 6.2, that every Büchi-recognizable language is QPTL-definable. We now complete a full circle by showing that every QPTL-definable language is S1S-definable, and that every S1S-definable language is Büchi-recognizable. Hence, QPTL, S1S, and Büchi automata are equally expressive.
$\textbf{Theorem 6.3. } \textit{Every QPTL-definable language is S1S-definable.}$
Proof
In section 6.4, we defined the language of QPTL as: $\mathcal{L}(\varphi)=\lbrace\alpha\in{(2^{AP’})}^{\omega}\mid\alpha\models\varphi\rbrace$, and
In section 6.5, we defined the language of S1S as: $\mathcal{L}(\varphi)=\lbrace \alpha_{\sigma_1,\sigma_2}\in(2^{V’_1\cup V’_2})^\omega\mid\sigma_1,\sigma_2\models\varphi\rbrace$
Notice main difference comes from $\alpha\models\varphi$ and $\sigma_1,\sigma_2\models\varphi$. Also, QPTL uses propositions but S1S uses term. We thus define S1S formula as $T(\varphi,t)$, where $\varphi$ is a QPTL-formula over $AP$ and $t$ is a S1S-term. Lastly, with $V_2=AP$, we can now define a S1S formula for all $\alpha\in(2^{AP})^\omega$,
$$\alpha\lbrack\lbrack t\rbrack_{\sigma_1},\infty\rbrack\models_{QPTL}\varphi\hspace{0.5cm}\text{iff}\hspace{0.5cm}\sigma_1,\sigma_2\models_{S1S}T(\varphi,t)\varphi,\hspace{1cm}\text{where }\ \sigma_2:P\mapsto\lbrace i\in\mathbb{N}\mid P\in\alpha(i)\rbrace$$
$\begin{array}{llll}
\hspace{1cm}\cdot&T(P,t)&=&t\in P\text{, for }P\in AP\newline
\hspace{1cm}\cdot&T(\neg\varphi,t)&=&\neg T(\varphi,t)\newline
\hspace{1cm}\cdot&T(\varphi\wedge\psi,t)&=&T(\varphi,t)\wedge T(\psi,t)\newline
\hspace{1cm}\cdot&T(\bigcirc\varphi,t)&=&T(\varphi,S(t))\newline
\hspace{1cm}\cdot&T(\Diamond\varphi,t)&=&\exists x.(x\geq t\wedge T(\varphi, x))\newline
\hspace{1cm}\cdot&T(\exists P.\varphi,t)&=&\exists P. T(\varphi,t)\newline
\end{array}$
Therefore, the language of $\varphi$ is then defined by the S1S formula $T(\varphi, 0)$.
Explanation
We apply every basic QPTL operators into $\varphi$, and transform them using S1S operators.
For proposition $P$, we can assign its value based on the temporal state when it holds. For example, for $\alpha={PPQPQQQ\dots}$, $P$ is in position $\alpha[0], \alpha[1], \alpha[3]$. So $\sigma_2:P\mapsto\lbrace0,1,3\rbrace$
And $T(P,t)$ is true when $t$ have value equals to {1,2,3}.
For the Finally operator $\Diamond$, it is expressed as true when the value is greater than or equals to t.
Next chapter: S1S$_0$ and Büchi-recognizable Language
AGV 6.6 -- Express QPTL using S1S