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.
import spot
import buddy
from spot.jupyter import display_inline
spot.setup()
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.
a2 = spot.translate("GFa <-> c", "generic", "deterministic", "SBAcc")
a2
m2 = spot.dtwa_to_mtdswa(a2)
display(m2)
for i, d in enumerate(m2.colors):
print(f"colors[{i}] = {d}")
a3 = spot.translate("Ga | Fb")
a3
m3 = spot.dtwa_to_mtdswa(a3)
m3
display_inline(m3.as_twa(), m3.as_twa(True))
display_inline(m2.as_twa(), m2.as_twa(True))
m2
i1 = spot.dtwa_to_mtdswa(spot.translate("G(c)", "det")); i1
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.
i1i = i1.as_twa(True, False, False)
i1c = i1.as_twa(True, False, True)
display_inline(i1i, i1i.prop_complete(), i1c, i1c.prop_complete())
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:
a1 = spot.translate("GFa", "generic", "deterministic", "complete", "SBAcc")
a2 = spot.translate("Gb | a", "generic", "deterministic", "complete", "SBAcc")
m1 = spot.dtwa_to_mtdswa(a1)
m2 = spot.dtwa_to_mtdswa(a2)
m1.sinks_as_constants()
m2.sinks_as_constants()
display_inline(m1, m2, per_row=2)
display_inline(spot.product_xor(m1, m2), spot.product_xnor(m1, m2), per_row=2)
display_inline(spot.product_implies(m1, m2))
Another example, a product with a more complex acceptance:
a1 = spot.translate("(p0 U p1) & GFp0 & GFp1 & FGp2", "generic", "deterministic", "complete", "SBAcc")
a2 = spot.translate("(p0 U p1) & GFp0 & GFp1 & FGp2", "generic", "deterministic", "complete", "SBAcc")
m1 = spot.dtwa_to_mtdswa(a1)
m2 = spot.dtwa_to_mtdswa(a2)
m1.sinks_as_constants()
m2.sinks_as_constants()
m12 = spot.product(m1, m2)
display_inline(m1, m2, m12, per_row=2)
Products on automata with names will also combine their names:
m1 = spot.obligation_to_mtdswa("Ga xor b")
m2 = spot.obligation_to_mtdswa("aUb -> Ga")
m12 = spot.product(m1, m2)
display_inline(m1, m2, m12)
In the previous two examples we can see the limitations of our implementation. We could try to avoid duplicating states and colors when possible.
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.
m = spot.obligation_to_mtdswa("Ga xor b")
mc = spot.complement(m)
display_inline(m, mc, per_row=2)
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:
f = spot.formula("\\forall a: Gd & (Fa U c) & (b xor Xa)")
swa = spot.obligation_to_mtdswa(f)
display_inline(swa)
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.
spot.trim(swa, True)
display_inline(swa)
Here is a hand-built example, showing most of the reductions made by trim:
a = spot.automaton('''
HOA: v1
name: "a"
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0 1 10
State: 1 5 8
State: 2 {0} 3 14
State: 3 {0} 2 14
State: 4 [t] 13
State: 5 6 13
State: 6 13 5
State: 7 [t] 13
State: 8 {0} [t] 9
State: 9 [t] 8
State: 10 2 11
State: 11 4 7
State: 12 [t] 4
State: 13 [f] 13
State: 14 {0} [t] 14
--END--
''')
display(a)
m = spot.dtwa_to_mtdswa(a)
print("m:")
display(m.show('s'))
print("trim(m):")
spot.trim(m)
display(m.show('s'))
print("trim(m, True):")
spot.trim(m, True)
display(m.show('s'))
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:
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$.
m = spot.obligation_to_mtdswa("Ga & Fb")
qm = spot.quantify_exists(m, spot.formula.ap('a'))
display_inline(m, qm, per_row=2)
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}:
t = spot.translate("(a & Xa & XXb) | (a & X!a & XXc) | (!a & Xa & XX(b | c)) | (!a & X!a & XX(b & c))", "deterministic", "complete", "SBAcc")
m = spot.dtwa_to_mtdswa(t)
m.sinks_as_constants()
qm = spot.quantify_forall(m, spot.formula.ap('a'))
display_inline(t, qm, per_row=2)
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.
print("untrimmed")
display(spot.quantify_forall(m, spot.formula.ap('a'), False))
print("trimmed")
display(spot.quantify_forall(m, spot.formula.ap('a'), True))
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.
a2 = spot.translate("GFa <-> c", "generic", "deterministic", "SBAcc")
m2 = spot.dtwa_to_mtdswa(a2)
a3 = spot.translate("Ga | Fb")
m3 = spot.dtwa_to_mtdswa(a3)
spot.scc_vector(m2)
spot.scc_vector(m3)
m2.show("s")
m3.show("s")
a = spot.translate("(a U b) | XG(c)", "det")
m4 = spot.dtwa_to_mtdswa(a)
print(spot.scc_vector(m4))
m4.show('s')
a = spot.translate("(a U b) & GFa & GFb & FGc", "det", "sbacc", "gen")
m5 = spot.dtwa_to_mtdswa(a)
m5.show('s')
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.)
a = spot.translate("true", "det")
m5 = spot.dtwa_to_mtdswa(a)
print(spot.scc_vector(m5))
m5.show('s')
... represented as an MTDSWA.
More details about this construction can be found in our CAV'26 paper.
The translation rules are even simpler than those 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 &= * &
& & & & \lnot * &= *
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).
t1 = spot.obligation_to_mtdswa('a W b U c')
t1.show('s')
t1.as_twa(True)
t2 = spot.obligation_to_mtdswa('Fa & Fb & Fc')
t2.show('s')
t2.as_twa(True)
t3 = spot.obligation_to_mtdswa('G(p1 <-> X!p1) | F(p0 & Xp1)')
t3.show('s')
t3.as_twa(True).show('.s')
Here is a list of obligation formulas to check that the new translation is equivalent to the old one.
obligations = ['Gp',
'Fr -> (!p U r)',
'(!r U (p & !r)) | G!r',
'Fr -> ((!p & !r) U (r | ((p & !r) U (r | ((!p & !r) U (r | ((p & !r) U (r | (!p U r)))))))))',
'Fr -> (p U r)',
'G(q -> Gp)',
'Fr -> (!p U (r | s))',
'Fr -> ((p -> (!r U (!r & s))) U r)',
'Fp -> (!p U (!p & s & X(!p U t)))',
'Fr -> (!p U (r | (!p & s & X(!p U t))))',
'F(s & XFt) -> (!s U p)',
'Fr -> (!(!r & s & X(!r U (!r & t))) U (p | r))',
'Fr -> ((p -> (!r U (!r & s & X(!r U t)))) U r)',
'Fr -> ((p -> (!r U (!r & s & !z & X((!r & !z) U t)))) U r)',
'Fp',
'G!q | F(q & Fp)',
'(!p U s) | Gp',
'Fr -> (((s & X(!r U t)) -> X(!r U (t & Fp))) U r)',
'G(p1 <-> X!p1) | F(p0 & Xp1)',
'Ga W Gb', # <- can trigger an infinite loop if propositional equivalence is not done
]
for obl in obligations:
t1 = spot.obligation_to_mtdswa(obl).as_twa(True) # non-minimized, via MTBDDs
t2 = spot.translate(obl, 'deterministic', xargs='new-oblig=0') # minimized via historical/explicit construction
print(t1.num_states(), t2.num_states(), spot.are_equivalent(t1, t2), obl)
Let's look at one case where the new translation produces one extra state compared to the reference implementation (which is already minimized).
f = spot.formula('Fr -> (!(!r & s & X(!r U (!r & t))) U (p | r))')
a = spot.obligation_to_mtdswa(f)
a.show('s')
b1 = a.as_twa(True, False)
b1
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.)
b2 = f.translate('deterministic', xargs='new-oblig=0')
b2
spot.are_equivalent(b1, b2)
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:
am = spot.minimize_mtdswa(a)
display("before:", a, "after:", am)
spot.are_equivalent(a.as_twa(), am.as_twa())
Let's look at a simple example to understand the problem why DFA minimization does not work immediately on weak deterministic ω-automata.
t4 = spot.obligation_to_mtdswa('a | Ga | F(b & Xa)')
t4.show('s')
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 difference in acceptance between those two states does not threaten to the validity of the translation: when the formula a | Ga | F(b & Xa) is translated into MTBDD, the superfluous Ga naturally disappears, 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 in acceptance prevents those two states from being merged by the DFA minimization algorithm.
spot.minimize_mtdswa(t4).show('s')
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 assigns each SCC a rank such that:
bddfalse and bddtrue implicitly have rank 0 and 1The way to compute these ranks is quite straightforward and can be done in linear time: compute an SCC decomposition, then process it bottom-up, assigning 0 or 1 to the bottommost SCC depending on its acceptance. Moving upward, the rank of a transient state is the maximum 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.
spot.loding_weak_ranking(t4)
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:
spot.loding_weak_ranking(t4, True)
t4
And now we can minimize this like a DFA:
spot.minimize_mtdswa(t4)
Here is a larger example:
t5 = spot.obligation_to_mtdswa('XXFa & ((b & Fc) | XGa)')
display(t5.as_twa(True, False), t5.show('0'))
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:
print(t5.num_roots(), "roots, minimized to", spot.minimize_mtdswa(t5).num_roots(), "roots.")
t5rank = spot.loding_weak_ranking(t5, True); t5rank
t5.show("0")
t5m = spot.minimize_mtdswa(t5)
print(t5.num_roots(), "roots, minimized to", t5m.num_roots(), "roots.")
display(t5m.show('0'), t5m.as_twa(True, False))
While this is not mentioned 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 alternations between accepting and rejecting SCCs that can be reached from there, two states can only be merged if they have the same rank.
t5m = spot.minimize_mtdswa(t5, t5rank) # <- initial partition given as second argument.
print(t5.num_roots(), "roots, minimized to", t5m.num_roots(), "roots.")
# The result is the same as above.
Earlier we said that the implemented minimization does not work well if accepting and rejecting sinks are represented as constants, because the minimization only focuses on merging states. The sinks_as_states() and states_as_sinks() rewrites the MTBDDs to change that representation.
display("before", am)
am.sinks_as_states();
display("after", am)
am.sinks_as_constants(); am.show('s')
Replacing constants with states may require changing the acceptance condition...
a1 = spot.dtwa_to_mtdswa(spot.translate('Ga', 'det', xargs="new-oblig=0")); a1
a1.sinks_as_states(); a1
# Coming back to constants do not change the acceptance condition back
a1.sinks_as_constants(); a1
a2 = spot.obligation_to_mtdswa('Fa'); a2
a2.sinks_as_states(); a2
# The optional argument asks to uses constants, but without removing the original sink states.
a2.sinks_as_constants(True); a2
a2.sinks_as_constants(); a2
Here is a case where the minimization fails because the sinks are constants instead of states. (Using loding_weak_ranking would not help here, as there are no transient states.)
o1 = spot.obligation_to_mtdswa('Ga | F!a')
o1m = spot.minimize_mtdswa(o1)
display_inline(o1, o1m)
# Switch to sinks to minimize
o1.sinks_as_states()
o1m = spot.minimize_mtdswa(o1)
display_inline(o1, o1m)
# Then back to constants if desired
o1.sinks_as_constants()
o1m.sinks_as_constants()
display_inline(o1, o1m)
New version of the pipeline, using the data structures and algorithms developed above:
def oblig2minwdba_mtdswa(f):
aut = spot.obligation_to_mtdswa(f)
aut.sinks_as_states()
ranks = spot.loding_weak_ranking(aut, True)
aut = spot.minimize_mtdswa(aut, ranks)
return aut
oblig2minwdba_mtdswa('Ga & X(Fb) | F(d & X!a)')
The old pipeline does a bit more:
Keep in mind that the two pipelines construct equivalent automata with different representations.
def oblig2minwdba_old(f):
return spot.translate(f, 'det', 'complete', 'low',
# Disable some specific preprocessings for fairer comparisons.
# Eventually, the new translation will benefit from those as well.
xargs='relabel-bool=0,relabel-overlap=0,ltl-split=0,new-oblig=0')
oblig2minwdba_old('Ga & X(Fb) | F(d & X!a)')
The new-oblig=1 option, which is actually the default, allows translate() to return a TwA that has been translated using the MTDSWA-based construction. The minimized MTDSWA is then converted into the TwA class. So the overhead of oblig2minwdba_new() over oblig2minwdba_mtdswa() is just the translation to MTDSWA.
def oblig2minwdba_new(f):
return spot.translate(f, 'det', 'complete', 'low',
# Disable some specific preprocessings for fairer comparisons.
# Eventually, the new translation will benefit from those as well.
xargs='relabel-bool=0,relabel-overlap=0,ltl-split=0,new-oblig=1')
oblig2minwdba_new('Ga & X(Fb) | F(d & X!a)')
⚠️ BIG WARNING ⚠️ The comparison below cannot be taken very seriously because all translations share the same BDD cache. Thus, when testing scalable patterns, some BDD operations are very likely to be cached between patterns. A more serious benchmark (still showing trends comparable to those seen here) is included in a submitted paper.
from timeit import default_timer as timer
def compare(f):
f = spot.formula(f) # parse it once
f2 = str(f)
t1 = timer()
a_new = oblig2minwdba_mtdswa(f)
t2 = timer()
a_new2 = oblig2minwdba_new(f)
t3 = timer()
a_old = oblig2minwdba_old(f)
t4 = timer()
if len(f2) > 60: f2 = f2[:59] + "…"
n_new = a_new.num_states()
n_new2 = a_new2.num_states()
n_old = a_old.num_states()
print(f"{t2-t1:6.3f}s {t3-t2:6.3f}s {t4-t3:6.3f}s {n_new:6} {f2}")
assert n_old == n_new
assert n_new == n_new2
if n_old < 2000: # Don't verify the automata big automata to save time.
assert spot.are_equivalent(a_new.as_twa(True), a_old)
assert spot.are_equivalent(a_new2, a_old)
import spot.gen as gen
print("-------- time -------- | |")
print(" new new old | |")
print("(MTDSWA) (TwA) (TwA)| states | formula")
for pat in ((gen.LTL_AND_F, 6, 10),
(gen.LTL_CCJ_ALPHA, 4, 7),
(gen.LTL_CCJ_BETA, 16, 20),
(gen.LTL_R_LEFT, 9, 12),
(gen.LTL_R_RIGHT, 11, 15),
(gen.LTL_U_LEFT, 6, 9),
(gen.LTL_U_RIGHT, 10, 13),
(gen.LTL_TV_F1, 5, 9),
(gen.LTL_TV_G1, 5, 9),
(gen.LTL_TV_F2, 5, 9),
(gen.LTL_TV_G2, 5, 9),
(gen.LTLF_CHOMP_MEALY, 1, 1),
(gen.LTLF_CHOMP_MEALY, 2, 2),
(gen.LTLF_CHOMP_MEALY, 3, 2), # 3x3 is too big for 32-bit architectures
gen.LTL_DAC_PATTERNS,
(gen.LTL_KR_N_DELTA1, 1, 3),
(gen.LTL_KR_NLOGN_DELTA1, 1, 3),
):
if type(pat) is tuple:
name=f"{gen.ltl_pattern_name(pat[0])} {pat[1]}{'…' if pat[1] < pat[2] else ','}{pat[2]}"
else:
name=f"{gen.ltl_pattern_name(pat)}"
print(f" -- {name}")
for f in gen.ltl_patterns(pat):
if f.is_syntactic_obligation(): # to filter the DAC patterns
compare(f)
The difference between the two NEW versions is mostly due to the automaton representation. In the second column, the MTDSWA has to be converted into a TwA, and this conversion (which requires enumerating the paths in the MTBDDs and creating labels for each of them) has significant overhead. However, even with this overhead, the new approach outperforms the old one most of the time.
It is interesting to see that there are two families where it is slower, namely, kr-n-delta1 and kr-nlogn-delta1. These are linear and quasilinear formulas for which the minimal DBA is at least doubly exponential; i.e., the worst case of the translation.
I investigated the behavior of the old and new pipelines on kr-nlogn-delta1=3:
Seeing that the new pipeline was spending a lot of time performing propositional-equivalence checks on all the LTL formulas labeling BDD leaves, I worked on that a bit. I added some missing caches to propositional equivalence, moved the prop.eq. into a second pass after computing $\mathit{tr}(\cdot)$ instead of performing it during the computation on each intermediate terminal, and added a few shortcuts. This significantly reduced the runtime, but, as seen above, it is still very long. Currently, propositional equivalence in the new pipeline (to MTDSWA) amounts for 65% of the time spent translating kr-nlogn-delta1=3. The translation of the old pipeline (Couvreur's) also performs some kind of propositional equivalence, but I think it is helped by two factors:
If we want to solve synthesis with Mealy semantics, we can declare input variables before output variables, and mark output variables as "controllable". This way the automaton can be interpreted as a game:
f = 'G(a <-> X!a) | F(b & Xa)'
with spot.bdd_dict_preorder("b") as d:
aut = spot.obligation_to_mtdswa(f, dict=d)
aut.set_controllable_variables(['a'])
display(aut.show('s'))
The synthesis algorithm actually solves the game while building the automaton, hopefully avoiding the computation of some states. The following example shows some of the intermediate steps of the construction.
The constructed automaton is explored using a DFS that tracks strongly connected components. When backtracking from an SCC any state that is undetermined (i.e., not yet marked as winning for either player) is marked according to the nature of the SCC: if the SCC is accepting, any cycle it contains is winning for the output player, if the SCC is rejecting, any cycle it contains is winning for the input player. The algorithm terminates as soon as the initial state is determined.
In the following intermediate outputs,
States in the debug output are also marked with ❹ or ❺ when their corresponding terminals are winning for the input or output player. This is a workaround to a limitation of our Graphviz printer that we can only color BDD nodes (including terminals) but the "state labels" that point to the roots of those BDDs. All this cosmetic work is of course performed only when the debug option is given.
Note also that, contrary to the output above, the acceptance of each state is not computed during the on-the-fly construction. We only need to compute the acceptance of one state per SCC when we remove it. Ultimately, all losing states will be removed from the automaton, and any infinite path in the remaining automaton will be a valid controller.
with spot.bdd_dict_preorder("b") as d:
for step in (0,1,2,3,4,5,7,9,10,11,14):
print("step", step)
display(spot.obligation_synthesis(f, ['a'], dict=d, debug=step))
Each step above represents one iteration of the DFS loop: either considering one possible successor for the current state (if a state was highlighted in yellow at step N, it will be the state developed at step N+1) or backtracking in the DFS (if no state is highlighted at step N, the next step is a backtrack). The entire process is described above.
Currently the output of spot.obligation_synthesis, without the debug option, is a crude output obtained by replacing all non-winning nodes (not green) by bddfalse, and for each output node (diamond) that has two winning successors, selecting one successor by redirecting the other to bddfalse (the backpropagation code simply remembers the edge that contributed to marking a node as winning). Probably we could improve that.
with spot.bdd_dict_preorder("b") as d:
aut = spot.obligation_synthesis(f, ['a'], dict=d)
display(aut)
m = spot.mtdswa_strategy_to_mealy(aut)
display(m, spot.reduce_mealy(m))
Here is the same specification, but with input and output swapped, so that it becomes unrealizable. In this case, we can see the algorithm abort before visiting all states.
with spot.bdd_dict_preorder("a") as d:
for step in (0,1,2,3,4,5,7,9,10):
print("step", step)
display(spot.obligation_synthesis(f, ['b'], dict=d, debug=step))
The full algorithm without debug mode simply returns an automaton with a single state equal to bddfalse (and acceptance f) in case the specification is not realizable.
with spot.bdd_dict_preorder("a") as d:
aut = spot.obligation_synthesis(f, ['b'], dict=d)
display(aut)
Here is another example, taken from SyntComp's tsl_paper/OneCounterInRangeA2.tlsf.
g = 'G!((o1 & !(o0 | o2)) <-> (!o1 & !((!o0 & o2) <-> (o0 & !o2)))) & ((i2 & G!(i0 & i1) & G((i2 & o0) -> Xi2) & G((i4 & o2) -> Xi2)) -> (G(o2 <-> (i1 & i4)) & G(o1 <-> (i0 & i3)) & Gi2))'
with spot.bdd_dict_preorder("i0", "i1", "i2", "i3", "i4") as d:
for step in (0,1,2,3,4,5,6,9):
print("step", step)
aut = spot.obligation_synthesis(g, ['o0', 'o1', 'o2'], dict=d, debug=step)
display(aut.show('0'))
print("output")
aut = spot.obligation_synthesis(g, ['o0', 'o1', 'o2'], dict=d)
display(aut)