Representation of ω-automata with state-based acceptance using MTBDDs.

We initially implemented a transition-based variant, before realizing that, when using MTBDDs, the transition-based and state-based versions of an automaton have exactly the same structure; the state-based version is even slightly more memory-efficient.

Although the transition-based variant still exists (see the mtdtwa.ipynb notebook), its state-based counterpart, presented here, is much more developed.

• Multi-Terminal-BDD-based Deterministic State-based ω-Automaton (MTDSwA))
• Automata operations on MTDSwAs
  • Products
  • Complement
  • Trimming unnecessary states
  • Quantifications
• SCC computations
• Translation from obligation formula to Deterministic Weak BA
• Moore's Minimization
• Löding's preprocessing for weak DBAs
• Converting sinks to states or constants
• Comparing obligation->minimal WDBA pipelines
• Synthesis

Multi-Terminal-BDD-based Deterministic State-based ω-Automaton (MTDSwA)¶

The MTBDD-based representation of these automata is very close to Mona's DFA representation. An mtdswa is simply a pair of arrays indexed by state numbers. The value of states[i] is an MTBDD encoding the successor states of state i, with terminals containing state indices. The value of colors[i] gives the set of colors associated with state i.

Compared to mtdtwa, the set of MTBDD nodes needed to represent an mtdswa is no larger than the one needed to represent an mtdtwa, because states with different colors but identical behavior can share their MTBDD. This representation seems much easier to work with.

When using as_twa(), the third argument allows you to choose between an incomplete TwA (rejecting sinks are removed) and a complete TwA (rejecting sinks are added). Adding sinks may require changing the acceptance condition.

Automata operations on MTDSwAs¶

Products¶

The Cartesian product of two MTDSwAs can be used to implement any Boolean operation. The Boolean operation just changes the way the acceptance conditions are combined, as well as some construction shortcuts for sinks. Each product state receives the colors of both original states, with colors from the right automaton shifted to avoid conflicts.

The following Boolean functions are available:

• product() implements $\land$
• product_or() implements $\lor$
• product_xor() implements $\oplus$
• product_xnor() implements $\leftrightarrow$
• product_implies() implements $\rightarrow$

Let's build two MTDSwAs so we can combine them:

Another example, a product with a more complex acceptance:

Products on automata with names will also combine their names:

In the previous two examples we can see the limitations of our implementation. We could try to avoid duplicating states and colors when possible.

Complement¶

Additionally, complement() does what's expected: The acceptance condition of the automaton is negated, and bddtrue and bddfalse leaves are swapped. Formula labels are also negated for looks.

Trimming unnecessary states¶

The trim() function removes different kinds of unnecessary states.

By default, it only removes states that are unreachable from the initial state.

If the optional trim_useless_sccs_too parameter is set to true, states from which a word will inevitably be accepted/rejected are also replaced with bddtrue/bddfalse respectively. This option is only slightly more expensive because it has to compute the SCCs of the MTDSwA. Note that trim() uses a simple check to detect some SCCs that cannot accept or that cannot reject, but on automata that are not weak, this can fail to detect and remove such SCCs.

Here is an example use of trim:

Here, states a & Fa & Gd & (Fa U c) and a & Gd lead to bddfalse (a rejecting sink). Any word reaching these states will then be rejected, so we can replace them directly with bddfalse.

Here is a hand-built example, showing most of the reductions made by trim:

In the original explicit automaton, states 13 and 14 are sinks that have already been converted into bddfalse/bddtrue by the dtwa_to_mtdswa() function. State 12 is the only unreachable state, so calling trim(m) will remove only this state. Calling trim(m, True) will remove much more. In the original automaton:

• SCC {5,6} is necessarily rejecting (it has no accepting combination of colors), and can only reach a rejecting sink, so it can be replaced by a rejecting sink.
• SCC {2,3} is the opposite: it is necessarily accepting and can only reach an accepting sink, so it can be replaced by an accepting sink.
• States 4, 7, and 11 are transient states that can only reach the rejecting sink, so they can be replaced by the rejecting sink.
• SCC {8,9} is always accepting, but the simple detection code based only on the colors occurring in the SCC does not detect this, so the SCC is kept.
• States 0, 1, and 10 are kept as well, since they can reach other states or sinks.

Quantifications¶

Weak MTDSwAs support quantifications of atomic propositions. \ (Beware that at the time of writing, weakness is not asserted; if you use this algorithm on non-weak automata, the result will not make sense.) Existentially quantifying a variable $a$ in a weak MTDSwA representing formula $\varphi$ produces an MTDSwA recognizing $\exists a : \varphi$. Universal quantification recognizes $\forall a : \varphi$.

A more visual example. Here, state 1 in the right automaton corresponds to the conjunction of states {1,2} from the left one. State 2 corresponds to states {3, 4, 5, 6}:

During quantification, sets of states need to be combined with OR / AND before being quantified. Unfortunately, this process can create many intermediate states that later become unused. For example, in the previous automaton, states $\{3, 5\}$ and $\{4, 6\}$ are created when computing the conjunction of $1$ and $2$, but are no longer needed after the quantification of $\{1, 2\}$ which creates $\{3, 4, 5, 6 \}$.

By default, quantify_exists and quantify_forall trim these states at the end. This can be disabled by passing False as a third parameter to the function.

SCC computations¶

The scc_vector assigns each state the index of a maximal SCC ordered topologically (each SCC can only reach an SCC with a smaller index).

The computation is performed in linear time by considering the MTDSwA as an oriented graph. Passing option 's' to show() highlights non-trivial SCCs, including their states and MTBDD nodes.