Support for alternating automata

The following automata are what we will use as examples.

Various display options

Here is the default output, using the bav options as set by default in the first cell.

If the state labels take too much space, you can reduce the size of the automaton by forcing states to be numbered with option 1. The original label is still displayed as a tooltip when the mouse is over the state.

Note that passing option show=... to display_inline is similar to calling aut.show(...) on each argument.

When working with alternating automata, it is quite common to hide "true states", and display "exiting transitions instead". You can do that with option u.

Let's make sure that option u and s (to display SCCs) work well together:

Alternation removal

The remove_alternation() function works on any alternating automaton that is weak (not necessarily very weak), i.e., in each SCC all transition should belong to the same accepting sets.

The second argument of remove_alternation(), set to True below, simply asks for states to be labeled to help debugging. As the function builds Transition-based Generalized Büchi acceptance, it can be worthwhile to apply scc_filter() in an attempt to reduce the number of acceptance sets.

The next cell shows this two-step process on our first example automaton.

Let's apply this process to the other 4 automata (which are not very-weak, unlike aut1). The states marked with ~ are part of a break-point construction.

The following demonstrates that very weak (non-alternating) Büchi automata can be complemented via alternation removal.