LTLF2DFA

ltlf2dfa - translate LTLf formulas into DFA

ltlf2dfa [OPTION...] [FORMULA...]

Convert LTLf formulas to transition-based deterministic finite automata.

If multiple formulas are supplied, several automata will be output.

Input options:

-f, --formula=STRING

process the formula STRING

-F, --file=FILENAME[/COL]

process each line of FILENAME as a formula; if COL is a positive integer, assume a CSV file and read column COL; use a negative COL to drop the first line of the CSV file

--lbt-input

read all formulas using LBT’s prefix syntax

--lenient

parenthesized blocks that cannot be parsed as subformulas are considered as atomic properties

--negate

negate each formula

--tlsf=FILENAME[/VAR=VAL[,VAR=VAL...]]

Read a TLSF specification from FILENAME, and call syfco to convert it into LTLf. Any parameter assignment specified after a slash is passed as ’-op VAR=VAL’ to syfco.

Processing options:

--composition=size|ap

How to order n-ary compositions in the compositional translation. By increasing size, or trying to group operands based on their APs.

--keep-names

Keep the names of formulas that label states in the output automaton.

--minimize=yes|no

Minimize the automaton (enabled by default).

--simplify-formula=yes|no

simplify the LTLf formula with cheap rewriting rules (disabled by default)

--translation=direct|compositional

Whether to translate the formula directly as a whole, or to assemble translations from subformulas. Default is compositional.

Output options:

-d, --dot[=options]

print the automaton in DOT format

-H, --hoaf[=1.1|b|i|k|l|m|s|t|v]

Output the automaton in HOA format (default). Add letters to select (1.1) version 1.1 of the format, (b) create an alias basis if >=2 AP are used, (i) use implicit labels for complete deterministic automata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transition-based acceptance, (k) use state labels when possible, (l) single-line output, (v) verbose properties

--mtdfa-dot

print the MTDFA in DOT format

--mtdfa-stats[=basic|nodes|paths]

print statistics about the MTDFA: ’basic’ (the default) displays only the number of states and atomic propositions (this is obtained in constant time), ’nodes’ additionally displays nodes counts (computing those is proportional to the size of the BDD) ’paths’ additionally displays path counts (this can be exponential in number of atomic propositions

-q, --quiet

suppress all normal output

Miscellaneous options:

--version

print program version

Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options.

Spot currently has little support for finite automata, and does not really support any DFA output format at the moment. When the --dot or --hoaf opetions are used, the DFA is converted into a Büchi automaton before being displayed.

The following paper describes how direct translation from LTLf to MTDFA works.

Report bugs to <spot@lrde.epita.fr>.

Copyright © 2025 by the Spot authors, see the AUTHORS File for details. License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.

ltlfsynt(1)