ltlf2dfa

Internally, the translation builds a DFA that is stored as an array of Multi-Terminal BDDs. Such a structure is called MTDFA in Spot (for Multi-Terminal DFA). It can be presented as follows:

ltlf2dfa --keep-names 'G(q -> Fr) | GFc' --mtdfa-dot

The blue rectangles at the top of the diagram are not part of the Multi-Terminal BDDs: they are just giving a name to each BDD and can be interpreted as state names. The magenta rectangles at the bottom are "terminals" labeled by destination states.

A path going down from a blue rectangle to a magenta rectangle corresponds to a transition labeled by the Boolean conjunction specified by that path. As usual in BDD diagrams, plain edges indicate that the variable above it is true, and edges are doted if the variable is false. If the terminal is accepting, as indicated with a doubled enclosure, the automaton can accept after reading that transition. In any case, the execution can continue from the blue state labeled with LTLf formula that was reached.

That structure can be converted to a transition-based DFA where accepting transition are marked with a ⓿. Any finite run is accepted if the last transition it went through is marked with ⓿. Note that empty runs cannot be accepted.

ltlf2dfa --keep-names 'G(q -> Fr) | GFc' --dot=.A

As a special optimization, the false and true LTLf formulas are represented in MTDFAs as the false and true BDDs constants. Those are depicted as orange squares:

ltlf2dfa --keep-names 'a M b' --mtdfa-dot

These false and true constants should be interpreted as rejecting and accepting sinks. When representing the automaton in a more traditional way, we omit paths going to the rejecting sink.

ltlf2dfa --keep-names 'a M b' --dot=.A

Spot currently has very limited support for DFAs, and does not know any format to represent these automata. Currently, we can abuse the HOA format to write those DFAs as if they were transition-based Büchi automata.

ltlf2dfa --keep-names 'a M b' -H

HOA: v1
name: "a M b"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0 "a M b"
[!0&1] 0
[0&1] 1 {0}
State: 1 "1"
[t] 1 {0}
--END--

In fact, even if we print the automaton with --dot without the A option (that hides the acceptance condition), we can see that the above automaton is represented as a Büchi automaton:

ltlf2dfa --keep-names 'a M b' --dot

Two options allow studying the MTDFA: --mtdfa-dot and --mtdfa-stats.

The former has already been used above, and prints the MTDFA in DOT format.

ltlf2dfa --keep-names 'a U b U c U d' --mtdfa-dot

For larger automata, it can be useful to stop tracking the name of states (do not use the --keep-names option). In that case the terminals are simply numbered, and one should pay attention not to confuse the terminals 0 and 1 (in magenta rounded rectangles) with the constants 0 and 1 (in orange squares).

ltlf2dfa 'a U b U c U d' --mtdfa-dot

The --mtdfa-stats options replace the output by some statistics about the MTDFA. By default, it just prints some statistics that can be obtained in constant time (after construction)

ltlf2dfa 'a U b U c U d' --mtdfa-stats

states: 3
aps: 4
BuDDy nodenum: 524288 (8192KB)
BuDDy freenodes: 524241 (99.99%)
BuDDy produced: 45
BuDDy cachesize: 16384 (256KB * 6 = 1536KB)
BuDDy hashsize: 524288 (2048KB)
BuDDy gbcnum: 0

The first lines are about the automaton itself:

• states is the number of blue nodes, i.e., the number of state in the automaton (not counting any sink state)
• ap is the number of atomic proposition that were involved in the construction of the automaton (the automaton may use fewer in practice)

The next lines, starting with BuDDy, give statistics about the BuDDy library's usage. Those statistics are global, so if multiple automata are translated in a single run of ltlf2dfa, these statistics will likely be different if automata are translated one at a time.

• nodenum is the total number of nodes currently allocated by the BuDDy library. Each node occupies 16 bytes. This number in enlarged as needed when BuDDy runs out of space, it is never decreased.
• freenodes is the number of unused nodes.
• produced is the total number of nodes ever produced (false and true are not counted).
• cachesize is the size of each operation cache of BuDDy. Each entry in a cache is 16 bytes, and BuDDy as 6 such caches. The MTBDD operations needed to translate LTLf to DFA will allocate a couple additional temporary caches of that same size, but this is not accounted here.
• hashsize is the size the BuDDy's hash table used to ensure unicity of nodes. It needs only 4 bytes per entry.
• gbcnum is the number of garbage collection performed by BuDDy since its initialization.

With the --mtdfs-stats=nodes options, additional information about the node usage of the automaton is retrieved. This requires a linear scan of the entire DAG.

ltlf2dfa 'a U b U c U d' --mtdfa-stats=nodes

states: 3
aps: 4
internal nodes: 7
terminal nodes: 3
constant nodes: 2 (false and true)
total nodes: 12 (0KB)
BuDDy nodenum: 524288 (8192KB)
BuDDy freenodes: 524241 (99.99%)
BuDDy produced: 45
BuDDy cachesize: 16384 (256KB * 6 = 1536KB)
BuDDy hashsize: 524288 (2048KB)
BuDDy gbcnum: 0

• internal nodes is the number of white nodes in the above pictures
• terminal nodes counts magenta nodes
• constants nodes counts the orange nodes
• total nodes is the sum of the above three.

With --mtdfa-stats=paths we additionally count paths and edges. This computation can be exponential in the number of atomic propositions.

ltlf2dfa 'a U b U c U d' --mtdfa-stats=paths

states: 3
aps: 4
internal nodes: 7
terminal nodes: 3
constant nodes: 2 (false and true)
total nodes: 12 (0KB)
paths: 15
edges: 9
BuDDy nodenum: 524288 (8192KB)
BuDDy freenodes: 524241 (99.99%)
BuDDy produced: 45
BuDDy cachesize: 16384 (256KB * 6 = 1536KB)
BuDDy hashsize: 524288 (2048KB)
BuDDy gbcnum: 0

• paths is the number of different paths leading from a blue node to a leave (excluding paths leading to the rejecting sink)
• edges is the number of pairs (state, leaf) that are connected by a paths (again, paths leading to false rejecting sink are not considered)

If we want to estimate the memory consumption of a MTDFA, each node (white, magenta, or orange) costs 16 bytes in BuDDy (four int), and each state (blue node) needs 4 bytes (one int). This is ignoring the cost of storing state names if requested (an LTLf formula AST is stored as DAG in which subformulas are shared with other LTLf formulas)

The --quiet option computes the MTDFA and exit without printing anything. This can be used for benchmarking the translation without the cost of printing the automaton, computing statistics on that automaton, or many even converting it to another automaton representation.

The --translation option can be used to select between two translation algorithms:

• With --translation=direct, the entire formula is translated directly. The resulting MTDFA can only be minimized after the translation.
• With --translation=compositional, the formula is split according to the Boolean operators that appear above temporal operators. Maximal subformulas whose top-level operator is temporal are translated directly. Then the resulting MTDFAs are combined according to the Boolean operator that are above it. This approach gives the opportunity to minimize the intermediate MTDFAs before they get combined.

Pass --minimize=no to turn off MTDFA minimization.

The --keep-names option, already illustrated above, requests that every algorithm keeps track of a formula labeling each state. The direct translation has to track those formulas anyway. For minimization and compositions this requires some extra work and memory, but it is usually negligible compared to size of the automaton.