Previous chapter: Quantified Propositional Temporal Logic (QPTL)
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
Temporal logics like LTL and QPTL refer to the positions of the input word implicitly through the temporal operators. With S1S, we now introduce a logic that allows us to manipulate positions explicitly.
For example, the mutual exclusion property in LTL is $\square\neg(\ell_1\wedge m_1)$, where the Always operator $\square$ implicitly quantifies over all positions. In S1S, we use explicit universal quantifiers instead: $\forall x.\neg(x\in P_{\ell_1}\wedge x\in P_{m_1})$.
Definition
- Monadic: the second-order quantification is restricted to unary relations, i.e., sets,
- One successor: only have a single successor operation.
Later in the course, we will study monadic second-order logics of two or more successors (S2S, WS1S, etc.), which allow us to describe trees rather than words.
S1S syntax
In automaton, we use states; in LTL and QPTL, we use propositions, in S1S, we use positions.
Propositions in QPTL can be interpreted as set of positions that holds $\textit{true}$.
| basic variables | Defintiion | Example |
|---|---|---|
first-order variables |
store positions | $0,1,x,y,\dots$ |
second-order variables |
store sets of positions (refer to $p$ as $\exists p.\varphi$ in QPTL) | $X,Y,\dots$ |
successor operation |
$S$, allows us to navigate to the next position (same as $\bigcirc$ in LTL) | $S(t), S(2),\dots$ |
Terms and Formulas
Let $V_1=\lbrace x, y,\dots\rbrace$ be a set of first-order variables and $V_2=\lbrace X, Y,\dots\rbrace$ a set of second-order variables. Then the terms of S1S are defined by the following grammar:
$$t::=0\mid x\mid S(t)$$
The formulas`of S1S are defined by the following grammar:
$$\varphi::=t\in X\mid t=t\mid\neg\varphi\mid\varphi\wedge\varphi\mid\exists x.\varphi\mid\exists X.\varphi$$
The precedence order of the operators goes from left (highest precedence) to right (lowest precedence), as denoted by the grammar above. We still allow usual boolean connectives with the following abbreviations:
$
\begin{array}{ll}
\hspace{1cm}\cdot\hspace{0.5cm} \forall X.\varphi := \neg\exists X. \neg\varphi& \hspace{3cm}\cdot\hspace{0.5cm} \forall x.\varphi := \neg\exists x. \neg\varphi\newline
\hspace{1cm}\cdot\hspace{0.5cm} x\notin Y := \neg(x\in Y)& \hspace{3cm}\cdot\hspace{0.5cm} x\neq y:= \neg(x=y)
\end{array}
$
Variable Valuations
The semantics of an S1S formula is given relative to a valuation of the variables.
First-order Valuation: $\sigma_1:V_1\rightarrow\mathbb{N}$ assigns to eachfirst-order variablea natural number.Second-order Valuation: $\sigma_2:V_2\rightarrow 2^\mathbb{N}$ assigns to eachsecond-order variablea set of natural numbers.
The value of a term is then defined as follows:
$\begin{array}{lll}
\hspace{1cm}\cdot\hspace{0.5cm} \lbrack 0\rbrack_{\sigma_1} = 0 &
\hspace{4cm}\cdot\hspace{0.5cm} \lbrack x\rbrack_{\sigma_1} = \sigma_1(x) &
\hspace{3cm}\cdot\hspace{0.5cm} \lbrack S(t)\rbrack_{\sigma_1} =[t]_{\sigma_1}+1\newline
\end{array}$
Free, Bound and the Language of S1S
Again, we define the subsets of free first-order and free second-order variables as $V’_1\subseteq V_1$ and $V’_2\subseteq V_2$ respectively. An S1S formula $\varphi$ then defines the following language over the alphabet $2^{V’_1\cup V’_2}$:
$$\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$$
where $x\in\alpha_{\sigma_1,\sigma_2}(j)\text{ iff }=\sigma_1(x)$, and $X\in\alpha_{\sigma_1,\sigma_2}(j)\text{ iff }j=\sigma_2(X)$, and $\models$ is the smallest relation that satisfies the following:
$
\begin{array}{llllll}
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & t\in X & \text{iff} & \lbrack t\rbrack_{\sigma_1}\in\sigma_2(X)\newline
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & t_1=t_2 & \text{iff} &\lbrack t_1\rbrack_{\sigma_1}=\lbrack t_2\rbrack_{\sigma_1}\newline
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & \neg\psi & \text{iff} &\sigma_1,\sigma_2\not\models\psi\newline
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & \varphi_0\wedge \varphi_1 & \text{iff} &\sigma_1,\sigma_2\models\varphi_0\text{ and }\sigma_1,\sigma_2\models\varphi_1\newline
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & \exists x.\varphi & \text{iff} &\text{there is an }\alpha\in\mathbb{N}\text{ s.t. }\sigma’_1,\sigma_2\models\varphi\text{ and }\sigma’_1(y)=\left\lbrace\begin{array}{ll}\sigma_1(y)&\text{if }y\neq x \newline a&\text{if }x=y\end{array}\right.\newline
\hspace{1cm}\cdot & \sigma_1,\sigma_2 & \models & \exists X.\varphi & \text{iff} &\text{there is an }A\in\mathbb{N}\text{ s.t. }\sigma_1,\sigma’_2\models\varphi\text{ and }\sigma’_2(Y)=\left\lbrace\begin{array}{ll}\sigma_2(Y)&\text{if }Y\neq X\newline A&\text{if }X=Y\end{array}\right.
\end{array}
$
For Existence Operator $(\exists)$, the definition is similar to QPTL: We have $\sigma’_1$ that behave exactly the same for every first-order variable $y$. Except for some $x$, there is a value $a$ that $\sigma’_1$ can assign to $x$ so that $\varphi$ holds. Same definition apply on second-order variable $X$ resepctively.
Example
| Statement | Formula |
|---|---|
| $X$ is a subset of $Y$ | $X\subseteq Y\equiv\forall z.\ (z\in X\rightarrow z\in Y)$ |
| $X$ and $Y$ are equal | $X = Y\equiv X\subseteq Y \wedge Y\subseteq X$ |
| $X$ is upward closed | $\textit{Upwardclosed}(X)\equiv\forall y.\ (y\in X\rightarrow S(y)\in X)$ |
| $x$ is less than or equals to $y$ | $x\leq y\equiv\forall Z.\ (x\in Z\wedge\textit{Upwardclosed}(Z))\rightarrow y\in Z$ |
| $X$ is a finite set | $\textit{Fin}(X)\equiv\exists Y.\ (X\subseteq Y\wedge(\exists z.\ z\notin Y)\wedge(\forall z.\ (z\notin Y\rightarrow S(z)\notin Y)))$ |
| $X$ is the set of even numbers | $\textit{Even}(X)\equiv0\in X\wedge\neg S(0)\in X \wedge \forall y.\ (y\in X\leftrightarrow S(S(y))\in X)$ |
| Every even number in $X$ is in $Y$ | $\textit{EvenCount}(X,Y)\equiv\forall w.\ (\exists Z.\ \textit{Even}(Z)\wedge w\in Z)\rightarrow(w\in X\rightarrow w\in Y)$ |
Summary
In the next section, we will try to compare S1S with QPTL and see their expressiveness.
Next chapter: Express QPTL using S1S
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