• MTBDDs
• LTLf semantics
• Conversion from LTLf to MTBDD
• Examples of outputs for tr
• Building a MTBDD-based DFA
• Propositional equivalence
• Simplifying terminals
• Detecting empty or universal translations
• Conversion from MTDFA to Twa
• More examples
• DFA Minimization
• Minimal MTDFA does not imply minimal state-based DFA
• Examples that caused problems to the minimization at some point
• Boolean operations on MTDFAs
• Converting from TwA to MTDFA
• Compositional translation
• Game interpretation
• Different ways to solve such a game
• Building a restricted MTBDD-based DFA for synthesis
• Strategy to AIG

MTBDDs¶

(If you are familiar with Mona's MTBDDs, skip directly to the last paragraph of this section.)

A Binary Decision Diagram represents a Boolean formula $f(a_1,a_2,\ldots,a_n): \mathbb{B}^n\to\mathbb{B}$ as a DAG in which each internal node is labeled by one of the $a_i$s (always in the same order) and has two children corresponding to $a_i=\bot$ and $a_i=\top$. The leaves of the DAG represent the values of $f$ when its arguments are assigned to the values represented on the path leading to that leave. This is typically implemented by storing all nodes in an array of triplets of integers $(i,low,high)$ where $i$ denotes variable $a_i$, $low$ is the index of the triplet for the $a_i=\bot$ branch, and $high$ is the index of the triplet for the $a_i=\top$ branch.
Special triplets $(n+1,0,0)$ and $(n+1,1,1)$ are stored at index 0 and 1 and represent the output values $\bot$ and $\top$. (The fact that they are stored at indices 0 and 1 makes it easy to recognize those constants from their indices without having to look at the triplets.)

Multi-Terminal BDDs generalize the co-domain of the representable functions to $\mathbb{N}$. So the DAG now stores functions of the form $f(a_1,a_2,\ldots,a_n): \mathbb{B}^n\to\mathbb{N}$. In this context, each leaf of the DAG should store a value $v\in\mathbb{N}$. Mona represents this by a triplet of the form $(\mathrm{MAXINT}, 1, v)$. (The value 1 does not mean anything, but both Mona and BuDDy use $low=-1$ to denote a unused triplet, so that makes it dangerous to repurpose the $low$ field.)

In both cases, a typical binary operation takes two BDDs, recursively descends in both BDDs in a way to explore all combinations of variables, combine the leaves once they are reached on both sides, and rebuild the resulting BDD from the bottom up while backtracking. The combinations of leaves correspond to Boolean operations in the $\mathbb{B}$ case. They can be arbitrary $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ functions in the MTBDD case. However, even of the two cases look very similar at a high-level, they are quite different in practice:

• In the Boolean case, the set of Boolean operations that can be used for combinations is small. Therefore a BDD library can implement them all, share a cache for all these operations, and implement shortcuts (for instance $\top\land f$ can return $f$ right away without having to recurse all the way down to the leaves of $f$ to rebuild $f$ from the bottom).

• In the Multi-Terminal case, an arbitrary $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ operation has to be supplied by the user as a function pointer. The facts that (1) the combination function works only on the terminals, and that (2) the apply function does not know what it does, makes it impossible for apply to "shortcut" the recursion. It also makes it difficult to cache multiple operations in the same cache because the combination function will likely use some global state (the function pointer is therefore not a good key for a hash table). Mona solves the cache issue by letting users manage the cache.

The version of BuDDy that ships with Spot has already been modified in many ways. It now supports integer-valued terminals in addition to the usual false and true nodes. You can build pure MTBDDs that do not use false and true, like in Mona. You can build standard BDDs that you only false and true, like BuDDy has always supported. And you may also build MTBDDs that mix integer-terminals and Boolean leaves. So in effect you can represent functions of $\mathbb{B}^n\to\mathbb{N}\cup\mathbb{B}$. The latter mix makes sense when some of the terminals would have semantics equivalent to false and true, and the applied operations also behave like Boolean operations: in that case we can specify the Boolean operation performed (in addition to passing the combination function that performs it on terminal) so that apply() knows how to shortcut its recursion when it reaches the false or true nodes on for one of its arguments.

LTLf semantics¶

This describes the standard LTLf semantics over non-empty words.

Given a set of atomic propositions $AP$, we consider LTLf formulas built over $AP$, using constants $\bot$, $\top$, unary operators $\mathsf{X}$, $\mathsf{X[!]}$, $\mathsf{F}$, $\mathsf{G}$, $\lnot$ and binary operators $\mathsf{U}$, $\mathsf{R}$, $\mathsf{W}$, $\mathsf{M}$, $\land$, $\lor$, $\rightarrow$, $\leftrightarrow$, $\oplus$.
Let $\sigma\in\Sigma^n$ be a non-empty word of $n>0$ letters of $\Sigma=2^{AP}$, let $i\in\{0,\ldots,n-1\}$ be some position on $\sigma$, and let $\varphi$ be an LTLf formula. The satisfaction of $\sigma$ by an LTLf formula at position $i$, denoted $\sigma,i\models \varphi$, is defined as follows:

$$ \begin{aligned} \sigma,i &\models \bot && \iff i=n \\ \sigma,i &\models \top && \iff i<n \\ \text{for }p\in\mathit{AP}\quad \sigma,i &\models p && \iff p\in\sigma(i) \\ \sigma,i &\models \lnot \varphi && \iff \lnot(\sigma,i \models \varphi)\\ \text{for }\odot\in\{\land,\lor,\rightarrow,\leftrightarrow,\oplus\}\quad\sigma,i&\models \varphi_1\odot\varphi_2 &&\iff (\sigma,i\models \varphi_1)\odot(\sigma,i\models \varphi_2) \\ \sigma,i &\models \mathop{\mathsf{X}}\varphi &&\iff (i+1=n)\lor(\sigma, i+1\models \varphi)\\ \sigma,i &\models \mathop{\mathsf{X[!]}}\varphi &&\iff (i+1<n)\land(\sigma, i+1\models \varphi)\\ \sigma,i &\models \varphi_1\mathbin{\mathsf{U}}\varphi_2 &&\iff \exists j\in \{i,\ldots,n-1\}, (\sigma,j\models \varphi_2) \land (\forall k\in\{i,\ldots,j-1\}, \sigma,k\models \varphi_1)\\ \sigma,i &\models \varphi_1\mathbin{\mathsf{R}}\varphi_2 &&\iff \forall j\in \{i,\ldots,n-1\}, (\sigma,j\models \varphi_2) \lor (\exists k\in\{i,\ldots,j-1\}, \sigma,k\models \varphi_1)\\ \sigma,i &\models \varphi_1\mathbin{\mathsf{M}}\varphi_2 &&\iff \exists j\in \{i,\ldots,n-1\}, (\sigma,j\models \varphi_1) \land (\forall k\in\{i,\ldots,j\},\phantom{{}-1} \sigma,k\models \varphi_2)\\ \sigma,i &\models \varphi_1\mathbin{\mathsf{W}}\varphi_2 &&\iff \forall j\in \{i,\ldots,n-1\}, (\sigma,j\models \varphi_1) \lor (\exists k\in\{i,\ldots,j\},\phantom{{}-1} \sigma,k\models \varphi_2)\\ \sigma,i &\models \mathop{\mathsf{F}}\varphi &&\iff \exists j\in[i,n), \sigma,j\models \varphi\\ \sigma,i &\models \mathop{\mathsf{G}}\varphi &&\iff \forall j\in[i,n), \sigma,j\models \varphi\\ \end{aligned} $$

A word $\sigma$ is accepted by $\varphi$ if $\sigma,0\models \varphi$.

Note that there exists an alternative definition of LTLf that considers the empty word. However one then needs two different negation operators to distinguish $\bar p$ (meaning $|\sigma|>0 \land p\not\in\sigma(0)$) from $\lnot p$ (meaning $|\sigma|=0 \lor p\in\sigma(0)$). Giacomo et al. avoid that problem by using only LTLf formulas in negative normal form. In what follows, we ignore the empty word and support arbitrary formulas that are not necessarily in negative normal form.

Conversion from LTLf to MTBDD¶

Given an LTLf formula labeling one automaton state, we want to construct an MTBDD that represents the set of its outgoing transitions: terminals will represent LTL formulas labeling the destination states, and one path in such an MTBDD will represent one outgoing transition. The $tr$ function defined below constructs such an MTBDD. (A full automaton will eventually be represented by an array of MTBDDs, one per state.)

In this context, we will use the terminals to represent pairs $(f,b)$ where $f$ is an LTLf formula, and $b$ is a Boolean. For simplicity we write $term(f,b)$ but in practice the terminal stores an integer, and this integer allows to find $f$ and $b$. The terminal $term(f,b)$ can be understood as representing a destination state labeled by $f$, and that state should be accepting iff $b=\top$. Or equivalently, you could think of $term(f,\top)$ as meaning $f\lor \varepsilon$; i.e., $b$ indicates whether the empty word is meant to be accepted after reaching that destination state.

We can apply a binary operator $\odot\in\{\land,\lor,\rightarrow,\leftrightarrow,\oplus\}$ to two MTBDDs using the aforementioned apply() algorithm, by using the convention that $term(f_1,b_1)\odot term(f_2,b_2) = term(f_1\odot f_2,b_1\odot b_2)$. The negation operator is handled similarly: $\lnot term(f,b) = term(\lnot f,\lnot b)$.

The translation of an LTLf formula to MTBDD is done using the following rules:

• $tr(\top) = term(\top,\top)\qquad$ (See optimization below)
• $tr(\bot) = term(\bot,\bot)\qquad$ (See optimization below)
• $tr(p) = p\land term(\top, \top)\quad$ for any atomic proposition $p\in AP$
• $tr(\lnot \alpha) = \lnot tr(\alpha)$
• $tr(\alpha \odot \beta)= tr(\alpha)\odot tr(\beta)$ for any $\odot\in\{\land,\lor,\rightarrow,\leftrightarrow,\oplus\}$
• $tr(\mathop{\mathsf{X}}\alpha) = term(\alpha,\top)$
• $tr(\mathop{\mathsf{X[!]}}\alpha) = term(\alpha,\bot)$
• $tr(\alpha \mathbin{\mathsf{U}} \beta) = tr(\beta) \lor (tr(\alpha)\land term(\alpha \mathbin{\mathsf{U}} \beta, \bot))$
• $tr(\alpha \mathbin{\mathsf{W}} \beta) = tr(\beta) \lor (tr(\alpha)\land term(\alpha \mathbin{\mathsf{W}} \beta, \top))$
• $tr(\alpha \mathbin{\mathsf{M}} \beta) = tr(\beta) \land (tr(\alpha)\lor term(\alpha \mathbin{\mathsf{M}} \beta, \bot))$
• $tr(\alpha \mathbin{\mathsf{R}} \beta) = tr(\beta) \land (tr(\alpha)\lor term(\alpha \mathbin{\mathsf{R}} \beta, \top))$
• $tr(\mathop{\mathsf{F}}\alpha) = tr(\alpha)\lor term(\mathop{\mathsf{F}}\alpha,\bot)$
• $tr(\mathop{\mathsf{G}}\alpha) = tr(\alpha)\land term(\mathop{\mathsf{G}}\alpha,\top)$

Note that the argument of $tr$ does not have to be in negative normal form.

Optimization: The above definition of $tr$ creates a pure MTBDD in which all leaves are terminal nodes. This unfortunately implies that whenever two MTBDD are combined, apply() has to recurse to the bottom of both operands to perform operations on terms. To help apply() shortcut some operations, we replace $term(\top,\top)$ and $term(\bot,\bot)$ by the true and false BDD constants respectively. A consequence of that is that for any Boolean formula $b$, $tr(b)$ is the traditional BDD representing the formula $b$, not involving any terminal.

Implementation details: Assuming there exists a mapping $M$ from LTLf formulas to integers, we actually represent $term(f,b)$ as a terminal with integer value $2M(f)+b$. In other words the lowest significant bit of the terminal value is used to remember whether the associated formula is allowed to satisfy the empty word.

Related work

This draws inspiration from several sources.

• Brzozowski's derivatives is a way to construct a DFA from a regular expression. The automaton is labeled by regular expressions, successors are obtained using a function $\delta_\ell(r)$ that computes the regular expression that one should go to after reading $\ell$ from a state labeled by $r$. The technique support regular expressions using any Boolean operator, not just disjunction. However for each state, it requires iterating over $\ell\in\Sigma$, so this can become quite slow for a large $\Sigma$.
• Giacomo et al.'s formula progressions is the equivalent of Brzozowski's derivatives, but applied to LTLf with semantics that consider the empty word. It requires the formula to be in negative normal form (that appears to be a consequence of allowing the empty word but not willing to complement it). Since LTLf is defined over a propositional alphabet, we have $\Sigma=2^{AP}$, and for each state we unfortunately have to loop over all letters $\ell\in\Sigma$ to compute the progressions, as in Brzozowski's derivatives.
• Antimirov's linear forms is a way compute all successors of a state labeld by a regular expression $r$ in a single pass. The linear form $\mathit{lf}(r)$ is a set $\{(\ell_1,r_1),...,(\ell_n,r_n)\}$ where $l_i$ are letters and $r_i$s are regular expressions, such that $L(r)\setminus\{\varepsilon\}=\bigvee_i \ell_i\cdot L(r_i)$. One can use that to construct an NFA (when multiple $\ell_i$ can be equal) or a DFA (after merging the pairs with identical $\ell_i$: $\{...,(\ell,r),(\ell,s),...\} \to \{...,(\ell,r\lor s),...\}$). Altought Antimirov only worked with classical regular expressions where disjunction is the only Boolean operator, deteriministic linear forms are easy to adapt to arbitrary Boolean operators. The linear form $\mathit{lf}(r)$ can be seen as a way to compute all derivatives in a single pass (the set of formulas obtained are not always syntactically equal to the set of derivatives, but they are equivalent).
• Martin et al.'s linear forms is an adaptation of Antimirov's linear forms to the semi-extended regular expressions (SERE) that appear in PSL or SVA. These expressions are defined over a propositional alphabet, so that makes the use of linear-forms (that can be computed in a single pass independent of the size of $\Sigma$) pertinent. This work also shows that two states that can have the same linear form can be merged when using finite automata with transition-based acceptance.
• Couvreur's LTL translation creates transition-based generalized Büchi automata from LTL. It uses BDDs to encode the outgoing transitions of a state labeled by a LTL formula. Extra BDD variables are used to store destination state as well as promises that have yet to be fulfilled. That BDD is computed recursively from the LTL label, using a set of rules similar to those of $tr$. Transitions can be recovered from the BDD by computing its prime implicants. Couvreur also suggests merging state represented by identical BDDs, and that transition naturally lends itself to transition-based acceptance. This algorithm is actually the core LTL translation in Spot, and computing those prime implicants is a costly part of the process.
• Mona uses MTBDDs to represent DFAs. My understanding is that their translation of WS1S to DFA is implemented as DFA operations over that representation. They do not really build their DFA state-by-state as in the previous techniques.

An MTBDD is actually very good data structure to represent a deterministic linear form over a propositional alphabet. The MTBDD computed by $tr(\alpha)$ above can be seen as a symbolic linear form for $tr(\alpha)$. This can equivalently be seen as a way to compute all formula progressions at once (modulo the semantics differences for the empty word). As done in Martin at al. and Couvreur's papers, we can merge two states that have the same MTBDD and benefit from transition-based acceptance (as will be shown below).

Examples of outputs for $tr$¶

Recall that $tr(\alpha)$ computes an MTBDD representing the outgoing edges of a single state labeled by $\alpha$.

The following example shows how the two MTBDDs for $a$ and $\mathop{\mathsf{X}}a$ can be combined in an MTBDD for $a\land \mathop{\mathsf{X}}$

The cyan rounded rectangles at the top of the DAGs are not part of the MTBDD, they are just giving a name to that MTBDD root to help us read the picture. A terminal $term(f,b)$ is shown as a magental rounded rectangle labeled by $f$, and that leaf has a double enclosure iff $b=\top$. The BDD constants false and true are shown in orange squares, but since true is actually a replacement for $term(\top,\top)$, it is also displayed with a double enclosure. White round nodes are labeled by atomic propositions. Below white nodes, dotted edges represent low links, and plain edges are high link. Hovering over the pictures with the mouse will display additional informations like bdd node numbers.

Below we learn that from a state labeled by $a\land \mathop{\mathsf{X}}$, we should not read $\lnot a$ (because that path would go to false, which is not accepting), and that if we read $a$, we can either accept the word if that was the last letter (because the terminal reached is marked as accepting), or go to a state labeled by formula $b$ to read the suffix of the word.

Here are the outputs of $tr$ on some basic operators, just to double-check their definitions.

The following plays with Boolean operators that are not used when forulas are in negative normal forms. However this translation does not require the input to be in negative normal form.

Building a MTBDD-based DFA¶

Iterating the use of tr() over all formulas appearing on terminals, we can build a MTBDD-based DFA. This is an array of MTBDDs, as in Mona. We call those MTDFA. The initial MTBDD (or initial state if you prefer) is indicated with a down arrow. The different MTBDD denoting the states can of course share part of their BDDs.

Different LTLf formulas can have the same MTBDD representation. Above, we can see that $tr(a \mathbin{\mathsf{U}} (b \mathbin{\mathsf{U}} c))=tr((b \mathbin{\mathsf{U}} c) \lor a \mathbin{\mathsf{U}} (b \mathbin{\mathsf{U}} c))$.

Since the successors of these states are identical, it makes sense to fuse them. This is actually what ltlf_to_mtdfa() does by default.

When fusing states, we must be cautious about the acceptance of these states.

Here is an example where this is clearly visible:

Here, $(\mathop{\mathsf{F}}a)\land (\mathop{\mathsf{G}}\mathop{\mathsf{F}}a)$ and $\mathop{\mathsf{G}}\mathop{\mathsf{F}}a$ are equivalent, so the algorithm simply remembers the first formula it has seen. Distinguishing the acceptance of the terminal nodes is not a problem.

Implementation details: A MTDFA is represented using two arrays:

• formula names[n];
• bdd states[n];

The MTBDD stored in states[i] encodes the outgoing edges of state i. State 0 is always the initial state. The terminal in those MTBDDs store integers of the form 2j+a were j is the index of the destination state, and a is a boolean indicating whether that destination is accepting. The names array is purely cosmetic: names[i] is the LTLf formula associated to state i, it can be used for rendering (names can be empty if one does not want to label the states).

Automaton aut1 above automaton has n=2 roots for a U b U c and b U c, but one will usually want to consider 1 as a state. The state for formula 1 is not stored, because it is always encoded as true. (People who prefer to work with complete DFAs, might want to consider 0 as a state too.) The mtdfa class has two methods to return its size: num_roots() counts the number of roots stored in the DFA (i.e., the size of the states and names array), and num_states() adds one to num_roots() if any root can reach true.

Propositional equivalence¶

The approach for building a MTDFA described above does not always terminate.

For instance consider $\varphi_1=(\mathop{\mathsf{G}}a) \mathbin{\mathsf{W}} (\mathop{\mathsf{G}}b)$. The MTBDD constructed by $tr(\varphi)$ will contain a path labeled $a\land b$ with destination $term(\varphi_2, \top)$ where $\varphi_2=(\mathop{\mathsf{G}}b) \lor ((\mathop{\mathsf{G}}a) \land \varphi_1)$. The formula MTBDD for $tr(\varphi_2)$ will in turn contain a path labeled by $a\land b$ with destination $term(\varphi_3, \top)$ where $\varphi_3=(\mathop{\mathsf{G}}b) \lor ((\mathop{\mathsf{G}}a) \land ((\mathop{\mathsf{G}}b) \lor ((\mathop{\mathsf{G}}a) \land \varphi_1)))$. The series could continue indefinitely like this adding new terms as it progress.

To avoid this, we say that two LTLf formulas are propositionally equivalent iff, when we interpret their maximal subformulas starting with a temporal operator as if they were propositions, the two formulas are equivalent. For instance formulas $\varphi_2$ and $\varphi_3$ are propositionally equivalent, because if we replace $\mathop{\mathsf{G}}a$, $\mathop{\mathsf{G}}b$, and $\varphi_1$ by the propositions $p_1$, $p_2$, and $p_3$ (respectively), we have:

$$ \begin{aligned} \varphi_2 &= p_2 \lor (p_1 \land p_3) \\ \varphi_3 &= p_2 \lor (p_1 \land (p_2 \lor (p_1 \land p_3))) = p_2 \lor (p_1 \land p_3) \end{aligned} $$

The equivalence between these two Boolean formulas can easily be established by encoding them in BDDs.

The implementation keeps track of one BDD representing the "propositional representation" of each LTLf used in a terminal, and everytime it attempts to create $term(g,b)$, it will replace it by $term(f,b)$ if a formula $f$ propositionally equivalent to $g$ has already been seen.

Doing so ensure termination, because the formula we translate has a finite number $m$ of subformulas, and the set of Boolean combinations of those formulas has only $2^{2^m}$ propositionally-equivalent classes.

Aside: Implementing this wasn't fun at all, because new terminals are created by a callback function called deep into the apply recursion. Propositional equivalence has to be checked inside that recursion, but it also require running other BDD operations and creating new BDD variables... So BuDDy had to learn how to run a BDD operation from within another BDD operation, and how to introduce new variables during a BDD operation.

Simplifying terminals¶

In an earlier example, we have seen that the translation of $\mathop{\mathsf{G}}\mathop{\mathsf{F}}a$ produces two different states labeled by $\mathop{\mathsf{G}}\mathop{\mathsf{F}}a$ and $\mathop{\mathsf{F}}a\land\mathop{\mathsf{G}}\mathop{\mathsf{a}}$. These two states have exactly the same MTBDD encoding, so that can be detected and fixed in a second pass after the translation. The only problem is that we did have to translate both formulas into MTBDDs.

The situation can get a lot worse: $\bigwedge_{i=1}^n \mathop{\mathsf{G}}\mathop{\mathsf{F}}p_i$ will create $2^n$ different terminals, but all these terminal are labeled by formulas that translate identically.

To avoid that, the propeq_representative function, that is already applied to each terminal formula to detect if it is propositionally equivalent to a previous formula, also implements the following cheap simplifications:

$$ \begin{aligned} (\alpha \mathbin{\mathsf{U}} \beta)\lor \beta &\equiv \alpha \mathbin{\mathsf{U}} \beta \\ (\alpha \mathbin{\mathsf{W}} \beta)\lor \beta &\equiv \alpha \mathbin{\mathsf{W}} \beta \\ (\alpha \mathbin{\mathsf{M}} \beta)\land \beta &\equiv \alpha \mathbin{\mathsf{M}} \beta \\ (\alpha \mathbin{\mathsf{R}} \beta)\land \beta &\equiv \alpha \mathbin{\mathsf{R}} \beta \\ (\mathop{\mathsf{F}}\beta) \lor \beta &\equiv \mathop{\mathsf{F}}\beta \\ (\mathop{\mathsf{G}}\beta) \land \beta &\equiv \mathop{\mathsf{G}}\beta \end{aligned} $$

There is one such rule for each temporal operator, for a pattern likely to occur in the output of $tr(\cdot)$.

In practice, for the $\bigwedge_{i=1}^n \mathop{\mathsf{G}}\mathop{\mathsf{F}}p_i$ formula mentionned above, those rules reduce all terminals to the input formula, causing a single state to be created. And there are no identical state to merges aferwards.

Detecting empty or universal translations¶

If the result of the translation has no accepting terminal (including true), or if it has no rejecting terminal (including false), then the formula is equivalent to true or false, and the automaton can be simplified to have a single state.

This simplification is enabled by default. Here is an example when we disable it:

By default, the translation will build the above, realize it has no accepting terminal, and therefore return a "false" automaton instead.

Conversion from MTDFA to TwA¶

TwA is the standard data-structure of Spot used to represent ω-automata.
Since Spot has no class for representing DFA explicitly, this conversion is just a hack to allow a more traditional representation where we just ignore the acceptance condition.

The conversion to transition-based acceptance is straightforward: each root of the MTBDD corresponds to a state, and each path from a root to a terminal corresponds to a transition, and that transition is accepting iff the terminal is odd. Paths going to the true BDD constant become transitions leading to an accepting sink.

With transition-based DFA, a word is accepted if its last letter was read by a transition marked with a ⓿.

The conversion to state-based acceptance is not more difficult: the acceptance is simply pushed onto the destination state.

Below, the as_twa() returns a transition-based automaton by default. as_twa(True) asks for a state-based output.

More examples¶

On the above example, we can see how transition-based acceptance can save three states (copies of 0, 2, and 4). Here is the state-based version for comparison.

DFA Minimization¶

The MTBDD-based DFA allows a very simple implementation of minimization by partition refinement, similar to what is used in Mona.

1. Assume all terminal belong to the same class, numbered 0.
2. Rewrite all MTBDDs by relabeling each terminal by its class number (preserving the acceptance bit)
3. Group all states in new classes according to their new BDD representation, giving each class a new number.
4. Loop to 2 until the number of classes is stable.

For the purpose of the above algorithm, false, and true should treated as terminals (i.e., assigned a class and rewritten). The actual implementation then performs a final pass on the result to put false and true back.

Let's find some formulas on which this minimization is effective by trying the examples from Lily. (These are LTL examples, but we interpret them as LTLf here.)