generalize the BA-typeness check
The is_scc_tba_type()
internal function used by tra_to_tba()
is currently specialized to Rabin acceptance.
However, the original paper [Krishnan et al., ISAAC'94] presents the check in a way that works regardless of the acceptance condition. Take an automaton A with arbitrary acceptance condition:
- find the set of "final transitions" F, i.e., transitions that cannot be part of a rejecting cycle
- check if A is still accepting after you have removed all final transitions F.
If A - F is not accepting anymore, then the input automaton is equivalent to a Büchi automaton with the same transition structure as A, but acceptance Inf(F).
The difficult point is the first one. Finding a rejecting cycle can be done by complementing the acceptance condition and looking for an accepting cycle, however we do not yet have that for arbitrary acceptance. (At the time of writing, the generic emptiness checks on the adl/generic-ec
branch only return true/false
answers, but it feels like it would not be too difficult to teach them to return an accepting cycle.)
The paper then goes on and points that a DRA is DBA-realizable iff it is DBA-type, and this does not hold for all acceptance conditions. However we still have that a BA-type automaton is clearly BA-realizable, so it still makes sense to try this algorithm before attempting some other conversion that add states. For instance the Streett-to-TGBA could be simplified on SCCs that are BA-type, and so would the default strategy of remove_fin()
. Also the recurrence check based on LTL->TGBA->DPA->DRA->is_DBA_type?
could skip the DPA->DRA
step.
In the long run, we should probably aim to refine remove_fin()
so that the different strategies can be applied at the SCC level instead of the entire automaton.