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:
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?
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.
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...