I would like to indicate in the property: line if an automaton is weak.
For Büchi automata, it is customary to distinguish two kinds of weakness:
weak Büchi automata are those in which, for each SCC, either all states are accepting, or all states are non-accepting
inherently weak automata are those whose SCCs do not mix accepting cycles with non-accepting cycles.
Of course any weak automaton is also inherently weak, and any inherently weak automaton can be converted to a weak automaton by adjusting the acceptance set.
Essentially, a weak automaton is one in which the acceptance condition could be specified in terms of SCCs (instead of transitions or states). Presented this way (please see the wording in 947375b) the "weak" property generalizes nicely to non-Büchi automata.
I would like to indicate in the property: line if an automaton is weak.
For Büchi automata, it is customary to distinguish two kinds of weakness:
Of course any weak automaton is also inherently weak, and any inherently weak automaton can be converted to a weak automaton by adjusting the acceptance set.
Essentially, a weak automaton is one in which the acceptance condition could be specified in terms of SCCs (instead of transitions or states). Presented this way (please see the wording in 947375b) the "weak" property generalizes nicely to non-Büchi automata.