I'm currently preparing a presentation about LTL and a book says that the language $L = (a(a \cup b))^\omega$ cannot be described by any LTL (or FO) formula which is understandable but how does the corresponding Büchi automaton $\mathcal{A}$ look like with $L(\mathcal{A}) = L$?
$\begingroup$
$\endgroup$
-
1$\begingroup$ What have you tried and where did you get stuck? (Which acceptance criterion do you use; the 'basic' one?) $\endgroup$ – Raphael♦ Feb 10 '15 at 21:33
$\begingroup$
$\endgroup$
Intuitively, the language is exactly the set of words that have $a$ in all the odd places. Thus, the corresponding NBW (in fact, $DBW$) has three states, $q,s,r$, where $q$ is initial, $s$ is accepting, and $r$ is a rejecting sink. The transitions are $\delta(q,a)=s, \delta(q,b)=r$, and $\delta(s,a)=\delta(s,b)=q$.
-
$\begingroup$ I see. Would it be possible to remove the state $r$ since the remaining states still accepts all words $w \in L$ due to being in $q$ infinitely often. $\endgroup$ – PeterMcCoy Feb 10 '15 at 18:59
-
$\begingroup$ If you want a DBW - then no, you need $q$ since the transition function needs to be full. However, if you use an NBW, then you can set $\delta(q,b)=\emptyset$, and then you don't need $r$. $\endgroup$ – Shaull Feb 10 '15 at 20:09
