confusion about what terminal means
Traditionally a Büchi automaton is terminal if the only accepting transitions/states belong to an accepting sink state. The notion of "sink" state can be extended to "sink SCC" (a weak an complete SCC). The intent is that when running the emptiness check on a terminal automaton, you can conclude that the automaton is non-empty as soon as you reach an accepting transition/state. Our couvreur99new
implementation uses that to abord earlier.
The question is what is a terminal automaton when t
acceptance is used, and does the above optimization makes sense for them.
In the HOA format this is worded as follows:
terminal
hints that the automaton is weak, that no non-accepting cycle can be reached from any accepting cycle, and that each SCC containing an accepting cycle is complete
According to that HOA definition, the following automaton (for Xa
) should be terminal:
If that automaton is tagged as terminal
our couvreur99new
algorithm would stop on the first transition (because it is accepting according to the acceptance condition) and declare the automaton as non-empty. This makes no sense to me, as the algorithm does not yet has proof that a loop exist.
(Note that even for Büchi, the HOA definition does not imply that accepting transitions are only present in accepting SCCs. We could have accepting transitions between SCCs, so the emptiness check optimisation wouldn't really make sense with this.)
The LTL translator knows that any syntactic guarantee will be translated as a terminal automaton (in the HOA sense), so it tags those as such.
However the strength-checking code has a different opinion. It will call the above automaton non-terminal, because its first transition is an accepting transition that is going to a rejecting SCC. In practice it is going to a trivial SCC, but trivial SCCs are considered as rejecting because they don't have any accepting cycle. That decision does not match the HOA definition, as this initial transition cannot reach a rejecting cycle, however it matches the emptiness check expectation.
I can see how to fix the strength-checking code to match the HOA definition, but that won't help the emptiness check. Or do we need to change the HOA definition of terminal
?