Previous chapter: LTL and Counting Languages
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
In the last section, we knew that LTL cannot express counting-languages. QPTL, which extends
LTL with quantification over propositions, repairs this deficiency.
Example
We knew $L=(\varnothing\varnothing)^\ast\lbrace p\rbrace^\omega$ is not LTL-definable. However, similar language $L’=(\varnothing\lbrace q\rbrace)^\ast\lbrace p\rbrace^\omega$ is LTL-definable:
$$\varphi=\neg q\wedge(\neg p\wedge(\neg q\leftrightarrow\bigcirc q))\ \mathcal{U}\ (\square(p\wedge\neg q))$$
Intuitively, $L’$ is the same language as $L$, except that there is an additional proposition $q$ that keeps track of odd and even positions. LTL has no means of introducing such “helpful” propositions that are not already present in the language we wish to define. In QPTL, we can introduce the proposition $q$ using a quantifier. The existential quantification $\exists q$. $\varphi$ expresses that there is a way to evaluate the new proposition $q$ such that, in the such extended word, $\varphi$ is true. In the example, the language of $\exists q.\ \varphi$ is thus precisely $L$.
Syntax
QPTL formulas over a set $AP$ of atomic propositions are generated by the following grammar, where $p\in AP$:
$$\psi ::= p\ \mid\ \neg\psi\ \mid\ \psi\wedge\varphi\ \mid\ \bigcirc\psi\ \mid\ \Diamond\psi\ \mid\ \exists p.\ \psi$$
The QPTL connectives have the same semantics and precedence as in LTL, except for propositional quantification, which has lowest precedence and the following semantics:
$$\begin{array}{lcr}\alpha\models\exists p.\ \varphi&\text{ iff }&\text{ there exists }\alpha’\in(2^{AP})^\omega\text{ such that }\alpha=_{AP\setminus\lbrace p\rbrace}\alpha’\text{ and }\alpha’\models\varphi\end{array}$$
where $\alpha=_P\alpha’$ for some $P\subseteq AP$ iff, for all $i\in\mathbb{N},\alpha(i)\cap P=\alpha’(i)\cap P$.
Every $AP$ in $\alpha$ is same as $\alpha’$, except $\alpha’$ can modify $p$ so that $\varphi$ holds for $\alpha’$
Until operator $\mathcal{U}$ in QPTL
We can express the Until operator $\mathcal{U}$ in the syntax of QPTL with quantifier and the meaning is equivalent:
$\varphi\ \mathcal{U}\ \psi:$ $\varphi$ must hold $\textit{true}$ until $\psi$ becomes $\textit{true}$.
$$\exists t.\ t\wedge\square(t\rightarrow(\psi\vee(\varphi\wedge\bigcirc t)))\wedge\Diamond\neg t:$$
$\exists t.\ t$: For some proposition $t$, $t$ holds at the beginning;
$\square(t\rightarrow(\psi\vee(\varphi\wedge\bigcirc t)))$: if $t$ holds, we repeatly check the following
- either $\psi$ becomes $\textit{true}$, or
- $\varphi$ must remain $\textit{true}$ and so as $t$ in the next step
(so that this if-clause check again in the next step);\$\Diamond\neg t$ : Eventually, $t$ will no longer hold.
- It enforces $\psi$ must become $\textit{true}$ at some point and then $t$ doesn’t need to hold anymore
- If it is weak until $\mathcal{W}$ then this part is not necessarily because we don’t enforce $\psi$ to be $\textit{true}$
Free and Bound Atomic Propositions
| Atomic Propositions | Defintiion |
|---|---|
Free |
NOT in the scope of a quantifier over the proposition |
Bound |
In the scope of a quantifier over the proposition |
Here, Bounded propositions are internal helpers to help us construct some logical conditions of the formula that do not directly appear in the language. (e.g. we need a counter for counting-language, but it doesn’t belongs to any proposition that refers to the alphabet or language.)
From QPTL formula to $\omega$-regular language
Let’s defined the set of free atomic propositions as $AP’\subseteq AP$. For every letter in the alphabet, we can describe them in $AP’$.
For exmaple, if $\lbrace a,b,c\rbrace=\Sigma$, the word $\lbrace ab\rbrace\in\Sigma$ will be $\lbrace a,b,\neg c\rbrace\in AP’$
Now, the language of QPTL is essentially the language over alphabet $2^{AP’}:\mathcal{L}(\varphi)=\lbrace\alpha\in{(2^{AP’})}^{\omega}\mid\alpha\models\varphi\rbrace$
In fact, it is exactly the $\omega$-regular languages that can be expressed in QPTL. And therefore, we can translate a given Büchi automaton with alphabet $2^{AP}$ into a QPTL formula:
$\textbf{Theorem 6.2. } \textit{For every Büchi automaton }\mathcal{A}\textit{ over }\Sigma=2^{AP}\textit{ there exists a QPTL formula }\varphi_{\mathcal{A}}\newline\textit{such that }\mathcal{L}(\varphi)=\mathcal{L}(\mathcal{A}).$
Proof
Reminder: here the automaton using atomic propositions $2^{AP}$, not the alphabet $\Sigma$. To translate states in automata into atomic proposition in QPTL formula, we introduce auxiliary proposition $at_q$ for each state $q\in Q$, where $Q=\lbrace q_1, q_2,\dots,q_n\rbrace$
Then QPTL formula $\varphi_\mathcal{A}$ for the Büchi automaton $\mathcal{A}$ so that $\mathcal{L}(\varphi)=\mathcal{L}(\mathcal{A})$ is defined as follows:
$$
\begin{array}{rll}
\varphi_\mathcal{A}:=\exists at_q,\dots,at_{q_n}.&&\underset{q\in I}{\bigvee}at_q\newline
&\wedge&\square\left(\underset{(q,A,q’)\in T}{\bigvee}at_q\wedge\bigcirc at_{q’}\wedge\left(\underset{p\in A}{\bigwedge}p\right)\wedge\left(\underset{p\in AP\setminus A}{\bigwedge}\neg p\right)\right)\newline
&\wedge&\square\left(\overset{n}{\underset{i=1}{\bigwedge}}\underset{j\neq i}{\bigwedge}\neg(at_{q_i}\wedge at_{q_j})\right)\newline
&\wedge&\square\Diamond\underset{q\in F}{\bigvee}at_q
\end{array}
$$
Explaination
To express a Büchi automaton in QPTL, we first need to know what features/characteristics we need express.
- Begins with Initial states and reaches the Accepting states infinitely often:
$$\textsf{Initial states: }\underset{q\in I}{\bigvee}at_q \hspace{3cm} \textsf{Accepting states: }\square\Diamond\underset{q\in F}{\bigvee}at_q$$
- There’s always transitions for any states, only using the letters available in the current state defined by set $A$:
$$\square\left(\underset{(q,A,q’)\in T}{\bigvee}at_q\wedge\bigcirc at_{q’}\wedge\left(\underset{p\in A}{\bigwedge}p\right)\wedge\left(\underset{p\in AP\setminus A}{\bigwedge}\neg p\right)\right)$$
- Additionally, we also need to ensure that there’s exactly one current state $q_i$, which is $at_{q_i}$ in propositions:
$$\square\left(\overset{n}{\underset{i=1}{\bigwedge}}\underset{j\neq i}{\bigwedge}\neg(at_{q_i}\wedge at_{q_j})\right)$$
Summary
As above, we can see that every feature of a Büchi automaton can be expressed in QPTL. What’s next? Can we use simpler syntax to express same formula?
Next chapter: Monadic Second-Order Logic of One Successor (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