Acceptance conditions when translating LTL to Büchi automaton?

Question

As an exercise in better understanding, I have been implementing the LTL to Generalized Büchi Automaton translation algorithm of Gerth, et al. (which is also discussed in Clarke, et al., Model Checking).

What I have ended up with seems incorrect, but also seems to accord with the discussion. Both of the presentations state that we should create a separate multiple sets of accepting states as follows: for each "subformula of $\phi$ [the LTL property to be checked] of the type $\mu U \psi$, there will be a[n accepting] set $F \in \cal F$ which includes the nodes $q \in Q$ such that either $\mu U \psi \not \in Old(q)$, or $\psi \in Old(q)$." By the standard translation of GBA to BA, the BA will be compelled to step through an accepting state for each of these component machines infinitely often.

Can someone clarify this definition? It seems wrong to me for a few reasons, which suggests I have failed to comprehend it:

1. As I understand it, the definition of "subformula" means that any formula contained, arbitrarily deeply, in $\phi$ would have its own acceptance condition. But surely this must be wrong, because, for example, an until condition buried in a release condition might not ever need to be satisfied. Even more simply, Clarke's textbook gives as an example the property $$ (A U B) \rightarrow F C) $$ which gets translated to $$( (\neg A) R (\neg B) ) \vee ( \top U C )$$ ($\top$ is the boolean constant true; Clarke, et al. use R for "release" where Gerth, et al. use V). In this case, the algorithm as described seems to demand that we satisfy $(\top U C)$, but this is only a disjunct. Perhaps that is correct because parts of the graph where this disjunct has not been introduced, will be accepting for it?

2. The following seems to be a more difficult example of the same question: $$((p U q) R r)$$ In this case, if r holds universally, then $(p U q)$ need never hold, so I don't believe I should have a GBA acceptance condition for it.

3. The discussion of the algorithm directs the implementer to translate into a negation normal form, which is what gives the subformula $( (\neg A) R (\neg B) )$, above. But this is not an "until" subformula, so does not give rise to any acceptance condition at all, which means that it's not possible to satisfy the above disjunction by satisfying this release condition. Is this an oversight? Should one be generating acceptance conditions for these subformulas, as well? Looking at the experimental results reported, I see that the expression $$\neg (p_1 U (p_2 U p_3))$$ is listed as not having any entries in the acceptance table. In a sense, this agrees with my expectation, because this is equivalent to $$\neg p_1 R (\neg p_2 R \neg p_3)$$ But surely this is satisfiable by infinite traces where, for example, $\neg p_3$ is always satisfied? So why are there no acceptance states? There's a caption to this example, but unfortunately, it's syntactically garbled: "The rightmost column represents the number of pairs in the acceptance table of the constructed automaton. Notice that for the safety property ...[described above]... there are no U subformulas satisfy [sic]. Yet, for the automaton to be nonempty, it has to contain a reachable cycle. [???]" I suppose in this case, it might be that when we translate this formula we get zero sets of accepting states and so vacuously any cycle is treated as accepting? But even so that would leave the earlier disjunctive case...

Answer 1

I will start with the last question and then come to the question at the top of your post.

1. The construction assumes that the LTL formula is given in negation normal form, so that no temporal operator occurs in negated form (as you wrote).
2. So $\neg (p_1 U (p_2 U p_3))$ gets translated to $\neg p_1 R (\neg p_2 R \neg p_3)$, and because in the latter formula, there is no Until subformula, we have 0 acceptance pairs in the Generalized Buchi automaton.
3. Now, a generalized Buchi automaton accepts all words for which there exists an infinite run on which all acceptance sets are visited infinitely often. If there are none, then this condition is vacuously true on any infinite run, which still has to exist. For example the word $(\{p_1,p_2\}^\omega)$ does not satisfy the LTL formula, and the corresponding generalized Buchi automaton has not infinite run for the word. If you model check with this automaton, every reachable cycle represents a case in which the LTL property holds. If you translate the generalized Buchi automaton to a Buchi automaton, then the standard construction makes every state in the latter accepting.
4. As far as the subformulas are concerned, you have to take the definition quite literally. For every Until-subformula in the NNF LTL property, you have an acceptance set. For instance, for $(a\,\mathcal{U}\,b)\,\mathcal{U}\,c$, you will have acceptance sets for $(a\,\mathcal{U}\,b)\,\mathcal{U}\,c$ and $(a\,\mathcal{U}\,b)$. For the All states in the generalized Buchi automaton containing $b$ or not containing $(a\,\mathcal{U}\,b)$ as a disjunct are accepting for the latter acceptance set. All states containing $c$ as a disjunct or not containing $(a\,\mathcal{U}\,b)\,\mathcal{U}\,c$ as a disjunct are labeled as contained in the acceptance set for $(a\,\mathcal{U}\,b)\,\mathcal{U}\,c$.
5. The example $((\neg A)R(\neg B))\vee(\top U C)$ that you mentioned is actually not problematic. Depending on how you write down the algorithm, either (1) no state will ever be labeled by $((\neg A)R(\neg B))\vee(\top U C)$, but only by $((\neg A)R(\neg B))$ or $(\top U C)$ (and you will have two initial states), or (2) all states labeled by $((\neg A)R(\neg B))\vee(\top U C)$ need to also be labeled by either $((\neg A)R(\neg B))$ or $(\top U C)$, and for determining in which acceptance set a state is, you only look at the whole subformulas, so a state labeled by $((\neg A)R(\neg B))$ would be accepting for all acceptance sets, while one also labeled by $(\top U C)$ would not be labeled by the acceptance set for $(\top U C)$ (unless it is also labeled by $C$).