This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
This is an example exercise to express LTL formula into Alternating Büchi Automata. For further definitions, you may check Section 7.2.
Question
Use the construction from the lecture to construct an alternating Büchi automaton $\mathcal{A}$ such that $$\mathcal{L(A)=L}((\Diamond p)\ \mathcal{U}\ (\square q))$$
Solution
we build the following alternating Büchi automaton $\mathcal{A} = (2^{p,q},Q,\varphi,\delta,\small\text{BÜCHI} \normalsize (F))$ which recognizes the models of $\varphi=(\Diamond p)\ \mathcal{U}\ (\square q)$. First we consider the transition function $\delta$ for an arbitrary symbol $a\in2^{p,q}:$
$\begin{array}{lll}
\hspace{1cm}\bullet &&\delta(\square q,a)\newline
&=&\delta(\neg(\textit{true}\ \mathcal{U}\ \neg q) ,a)\newline
&=&\overline{\delta(\textit{true}\ \mathcal{U}\ \neg q ,a)}\newline
&=&\overline{\delta(\neg q,a)\vee(\delta(\textit{true},a)\wedge(\textit{true}\ \mathcal{U}\ \neg q))}\newline
&=&\overline{\delta(\neg q,a)}\wedge\overline{(\delta(\textit{true},a)\wedge (\textit{true}\ \mathcal{U}\ \neg q))}&(\textit{true}\wedge \psi=\psi)\newline
&=&\overline{\delta(\neg q,a)}\wedge\overline{(\textit{true}\ \mathcal{U}\ \neg q)}&(\text{Using line 1})\newline
&=&\overline{\delta(\neg q,a)}\wedge\square q\newline
&=&\left\lbrace \begin{array}{lll}
\square q&\text{if }q\in a\newline
\textit{false}&\text{if }q\notin a\newline
\end{array}\right.
\end{array}
\ \newline \ \newline
\begin{array}{lll}
\hspace{1cm}\bullet &&\delta(\Diamond p,a)\newline
&=&\delta(\textit{true}\ \mathcal{U}\ p ,a)\newline
&=&\delta(p,a)\vee(\delta(\textit{true},a)\wedge\Diamond p)&(\textit{true}\wedge \psi=\psi)\newline
&=&\delta(p,a)\vee\Diamond p\newline
&=&\left\lbrace \begin{array}{lll}
\Diamond p&\text{if }p\notin a\newline
\textit{true}&\text{if }p\in a\newline
\end{array}\right.
\end{array}
$
By Substitution above result into $\delta((\Diamond p)\ \mathcal{U}\ (\square q),a)=\delta(\square q,a)\vee(\delta(\Diamond p,a)\wedge(\Diamond p)\ \mathcal{U}\ (\square q))$, we have:
$$\delta((\Diamond p)\ \mathcal{U}\ (\square q),a)=\left\lbrace
\begin{array}{lll}
\Diamond p\wedge((\Diamond p)\ \mathcal{U}\ (\square q))&\text{if }a =\varnothing &(\vee\ \textit{false}\text{ is omitted.})\newline
(\Diamond p)\ \mathcal{U}\ (\square q)&\text{if }a =\lbrace p\rbrace&(\wedge\ \textit{true}\text{ is omitted.})\newline
\square q\vee(\Diamond p\wedge((\Diamond p)\ \mathcal{U}\ (\square q)))&\text{if }a =\lbrace q\rbrace\newline
\square q\vee((\Diamond p)\ \mathcal{U}\ (\square q))&\text{if }a =\lbrace p,q\rbrace&(\wedge\ \textit{true}\text{ is omitted.})\newline
\end{array}\right.$$
For each case, when we see $\vee$, that’s a nondeterministic transitions, we need draw two seperate transitions for each successors. On the other hand $\wedge$ is a universal transitions, it is a single transition towards both successors, we split the extra branches from the path to indicate that. Thus we have the following automaton $\mathcal{A}$:
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