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
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com