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

We initially implemented a transition-based variant, before realizing that 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.

So even if 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)¶

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

Compared to mtdtwa, the set of MTBDD nodes needed to represent a mtdswa is not bigger than the one used to represent an mtdtwa as states that have different colors but behave the same will share their MTBDD. This representation seems much easier to work with.

When using as_twa(), the third argument allow to chose between incomplete (rejecting sinks are removed) and complete (rejecting sinks are added) TwA. Adding sinks may require to change the acceptance condition.

SCC computations¶

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

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

TODO: The linking above is not optimal. Since all states 1,2,3,4,5 recognize the same language, it would be better to always jump on the same state when entering this SCC. That way the two transient "b" node above false could be merged. Currently we don't care too much because those nodes were converted from an explicit representation. However, when we start building translating LTL to mtdswa directly, we can probably do better.

The false and true automata don't display very well because they have to introduce a state that points to the constant. But that should be interpreted as a single SCC. (Technically, the blue nodes at the top of the figures do not really belong to the SCCs.)

Translation from obligation formula to Deterministic Weak BA¶

... represented as MTDSWA.

The translation rules are even simpler than those of for translating LTLf to MTDFA (see the CIAA'25 paper or the ltlf2dfa notebook).

Let us use $\boxed{\varphi}$ to denote a terminal labeled by LTL formula $\varphi$. Let us further assume that applying any Boolean operator $\odot\in\{\land,\lor,\leftarrow,\leftrightarrow,\oplus,...\}$ between two terminals results in a terminal labeled by the result of applying $\odot$ on the two labels, i.e., $\boxed{\alpha}\odot\boxed{\beta}=\boxed{\alpha\odot\beta}$. Using that convention, the standard apply2() operation of BDD can be extended to support Boolean operation on MTBDD labeled by LTL formulas.

Then the translation of an LTL formula to MTBDD with LTL terminals following the standard expansion rules of LTL:

\begin{align} \mathit{tr}(b) &= \text{BDD representation of $b$}& \text{for any Boolean formula $b$} \\ \mathit{tr}(\mathop{\mathsf{X}}\varphi) &= \boxed{\varphi} \\ \mathit{tr}(\lnot\varphi) &= \lnot\mathit{tr}(\varphi) \\ \mathit{tr}(\alpha \odot \beta) &= \mathit{tr}(\alpha)\odot \mathit{tr}(\beta) & \text{for any Boolean operator $\odot\in\{\land,\lor,\leftarrow,\leftrightarrow,\oplus,...\}$}\\ \mathit{tr}(\alpha \mathbin{\mathsf{U}} \beta) &= \mathit{tr}(\beta)\lor(\mathit{tr}(\alpha)\land\boxed{\alpha \mathbin{\mathsf{U}} \beta}) \\ \mathit{tr}(\alpha \mathbin{\mathsf{W}} \beta) &= \mathit{tr}(\beta)\lor(\mathit{tr}(\alpha)\land\boxed{\alpha \mathbin{\mathsf{W}} \beta}) \\ \mathit{tr}(\alpha \mathbin{\mathsf{M}} \beta) &= \mathit{tr}(\beta)\land(\mathit{tr}(\alpha)\lor\boxed{\alpha \mathbin{\mathsf{M}} \beta}) \\ \mathit{tr}(\alpha \mathbin{\mathsf{R}} \beta) &= \mathit{tr}(\beta)\land(\mathit{tr}(\alpha)\lor\boxed{\alpha \mathbin{\mathsf{R}} \beta}) \\ \mathit{tr}(\mathop{\mathsf{F}} \varphi) &= \mathit{tr}(\varphi)\lor\boxed{\mathop{\mathsf{F}}\varphi} \\ \mathit{tr}(\mathop{\mathsf{G}} \varphi) &= \mathit{tr}(\varphi)\land\boxed{\mathop{\mathsf{G}}\varphi} \\ \end{align}

The above rules for $\mathit{tr}(\varphi)$ can be used to obtain the MTBDD representing the outgoing edges of a state $\varphi$. By iterating this for all formulas that label terminals reachable from $\varphi$, we can build the structure of the automaton for $\varphi$.

For termination, each formulas that appear in terminal are assumed to be replaced by one unique representative of their propositional equivalence classes. See the ltlf2dfa notebook for details.

What remains is to decide for each state whether it is accepting. The $\lambda$ function below does that by just checking the top-level temporal operators. That states labeled by strong operators ($\mathsf{F}$, $\mathsf{U}$, $\mathsf{M}$) should not be accepting, and states labeled by weak operators ($\mathsf{G}$, $\mathsf{W}$, $\mathsf{R}$) should be accepting. Combinations of those follow the semantics of the Boolean operators.

\begin{align} \lambda(\top)&=\top\\ \lambda(\bot)&=\bot\\ \lambda(a) &= * & \text{for any atomic proposition}\\ \lambda(\lnot\varphi) &= \lnot\lambda(\varphi)\\ \lambda(\mathop{\mathsf{X}}\varphi) &= \lambda(\varphi) \\ \lambda(\alpha \odot \beta) &= \lambda(\alpha)\odot\lambda(\beta) & \text{for any Boolean operator $\odot\in\{\land,\lor,\leftarrow,\leftrightarrow,\oplus,...\}$} \\ \lambda(\alpha \mathbin{\mathsf{U}} \beta) &= \bot \\ \lambda(\alpha \mathbin{\mathsf{M}} \beta) &= \bot \\ \lambda(\mathop{\mathsf{F}}\varphi) &= \bot \\ \lambda(\alpha \mathbin{\mathsf{W}} \beta) &= \top \\ \lambda(\alpha \mathbin{\mathsf{R}} \beta) &= \top \\ \lambda(\mathop{\mathsf{G}}\varphi) &= \top \\ \end{align}

Here the value $*$ should be interpreted as a joker that can simply be ignored when being combined with other Boolean operations: \begin{align} \top\land * &= \top & \bot \land * &= \bot & * \land * &= * \\ \top\lor * &= \top & \bot \lor * &= \bot & * \lor * &= * \\ \top\rightarrow * &= \bot & \bot \rightarrow * &= \top & * \rightarrow * &= * & * \rightarrow \top &= \top & * \rightarrow \bot &= \bot & \\ \top\leftrightarrow * &= \top & \bot \leftrightarrow * &= \top & * \leftrightarrow * &= * \\ \top\oplus * &= \top & \bot \oplus * &= \top & * \oplus * &= * \\ & & & & \lnot * &= * \end{align}

By construction, one can see that the only formulas $\varphi$ for which $\lambda(\varphi)=*$ must be obtained by using only atomic propositions, Boolean operators and $\mathop{\mathsf{X}}$ operators, this corresponds to formulas that are both safety and co-safety syntactically. If such a formula labels a state, that state cannot be part of any cycle, i.e., it is a transient state, and its acceptance is irrelevant. Hence the use of a joker.

For the construction, states labeled by a formula $\varphi$ such that $\lambda(\varphi)=\top$ should be tagged as accepting, states where $\lambda(\varphi)=\bot$ must be tagged as rejecting, and states for which $\lambda(\varphi)=*$ can be tagged either way without impact on the language.

In the implementation we do not actually use the above ternary logic. Instead we have $\lambda(a)=\bot$, and the Boolean operators (which are n-ary in the case of $\land$ and $\lor$) are modified to ignore the arguments that are both safety and co-safety syntactically (Spot maintains this class membership as a property bit in each formula, so this can be tested in constant time).

Here is a list of obligation formulas to check that the new translation is equivalent to the old one.

Let's look at one case where the new translation produces one extra state compared to the reference implementation (which is already minimized).

State 1 and 3 can be merged. Here is the minimized output from the historical translation. (If you see new-oblig=0 appearing in the calls to translate() in this notebook, it is because translate() was also changed to use the new MTBDD-based obligation translation presented later in this notebook. Passing new-oblig=0 forces Spot to use the old non-MTBDD-based obligation translation.)

Moore's Minimization¶

Moore's DFA minimization algorithm is easy to implement on MTBDD-based ω-automata, just using the color of the states for the initial partition. However, despite its name, it does not guarantee a minimal automaton when applied to ω-automata. (There is a way to fix that for weak deterministic ω-automata, as we will see later.) Moore's minimization algorithm is quadratic (unlike Hopcroft's which does it in $O(n \log n)$), but it is very suited to MTBDD-based representation because to perform one iteration of the algorithm, we just have to replace each terminal by its current class number, and after rewriting the MTBDDs states the new partition can be read by looking which state have the same MTBDD representation.

The minimization currently forces the bddtrue and bddfalse terminals in separate classes. So, for instance, if you build a MTDSWA that contains a bddtrue terminal, and another accepting state that loops over itself with label "true", these two states won't be merged. The minimization for mtdfa used to deal with this case, but that made the code more complex and harder to maintain. In practice, the bddtrue and bddfalse terminals are only useful during the recursive translation, where they help shortcut BDD operations, but they are more annoying to deal with afterwards. Hence this implementation of the minimization does not make any effort regarding those.

In a few sections we will show how to change between constant-based (bddtrue, bddfalse), or state-based representations of sinks. Therefore, for precise minimization, one should call a.sinks_as_states() before spot.minimize_mtdswa(a).

In the meantime, we can still use this algorithm to merge the two equivalent states in automaton a:

Löding's preprocessing for weak DBAs¶

Let's look at a simple example to understand the problem why DFA minimization does not work immediately on weak deterministic ω-automata.

On this example, we can see that the initial state is labeled by a | Ga | F(b & Xa). Because this disjunction contains the safety formula Ga, the state is marked as accepting. However, this formula is equivalent to a | F(b & Xa), which would be rejecting. The different acceptance for those two states is not a threat to the validity of the translation: when the formula a | Ga | F(b & Xa) is translated into MTBDD, the superfluous Ga naturally disappear, so a | Ga | F(b & Xa) only occurs as a transient SCC, and its acceptance has no impact on the language of the automaton. However, the difference of acceptance prevent those two states from being merged by the DFA minimization algorithm.

An easy fix here would be to detect that a | Ga | F(b & Xa) and a | F(b & Xa) have the same MTBDD encoding, and because a | Ga | F(b & Xa) is a transient state, decide to replace it by the other state.

Löding's preprocessing00183-6) is a more general solution that decides for each transient state of a weak deterministic ω-automata whether it should be accepting or rejecting, in such a way that applying DFA minimization on the preprocessed ω-automata will ensure minimality of the result. Spot implements a variant of this preprocessing that assign to each SCC a rank such that:

• SCCs are accepting iff they have odd rank
• ranks can only decrease along a run of the automaton
• bddfalse and bddtrue implicitly have rank 0 and 1
• the rank assigned to each SCC is the minimal one that could be assigned given the above constraint.

The way to compute those ranks is quite straight forward and can be done in linear time: compute an SCC decomposition, then process it in a bottom-up way, assigning 0 or 1 to the bottommost depending on its acceptance. Moving up, the rank of a transient state is the maximum of the rank of its successors. If an SCC is not transient, that computed maximum may have to be incremented by one to match the acceptance of the current SCC.

Even if the rank is SCC-based, the return value of loding_weak_ranking is an array giving the rank of each state.

In this case all states have rank 2, so they should be rejecting. bddtrue has rank 1 implicitly, but this is not indicated in the return.

We can also ask loding_weak_ranking to fix the acceptance of the transient states in the provided automaton:

And now we can minimize this like a DFA:

Here is a larger example:

What is visible in the output above is that states 1, 4, and 8, could be merged after changing the acceptance of 1 and 4. Without that, Moore's algorithm will not reduce anything:

While this is not mentionned in Löding's paper, the ranking computed by loding_weak_ranking can be used to speed up Moore's minimization by interpreting it as the initial partition of the states. Since the ranking is related both to the acceptance of the state, and to the number of alternation between accepting and rejecting SCCs that be reached from there, two states can only be merged if they have the same rank.