LTLFSYNT(1) User Commands LTLFSYNT(1) NAME ltlfsynt - check realizability of LTLf formulas SYNOPSIS ltlfsynt [OPTION...] [FORMULA...] DESCRIPTION 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 in- teger, assume a CSV file and read column COL; use a negative COL to drop the first line of the CSV file --ins=PROPS comma-separated list of uncontrollable (a.k.a. input) atomic propo- sitions, interpreted as a regex if enclosed in slashes --lbt-input read all formulas using LBT's prefix syntax --lenient parenthesized blocks that cannot be parsed as subformulas are con- sidered as atomic properties --outs=PROPS comma-separated list of controllable (a.k.a. output) atomic propo- sitions, interpreted as a regex if enclosed in slashes --part-file=FILENAME read the I/O partition of atomic propositions from FILENAME --semantics=Moore|Mealy Whether to work under Mealy (input-first) or Moore (output-first) semantics. The default is Mealy. --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. Fine tuning: --backprop=nodes|states|trival-states whether backpropagation should be done at the node or state level (nodes by default) --composition=size|ap If the translation is set to "compositional" this option specify how to order n-ary compositions: by increasing size, or trying to group operands based on their APs (the default). --decompose=yes|no whether to decompose the specification as multiple output-disjoint problems to solve independently (enabled by default) --global-equivalence=yes|no|before-decompose whether to remove atomic propositions that are always equivalent to another one (enabled by default, both before and after decomposi- tion) --minimize=yes|no Minimize the automaton (disabled by default except for the composi- tional translation). Has no effect on on-the-fly translations. --one-step-preprocess=yes|no attempt check one-step realizability or unrealizability of each state during on-the-fly or restricted translations (enabled by de- fault) --polarity=yes|no|before-decompose whether to remove atomic propositions that always have the same po- larity in the formula to speed things up (enabled by default, both before and after decomposition) --simplify-formula=yes|no simplify the LTLf formula with cheap rewriting rules (enabled by de- fault) --translation=full|compositional|re- stricted|bfs-on-the-fly|dfs-on-the-fly|dfs-strict-on-the-fly The type of translation to use: (full) is a direct translation to MTDFA, (compositional) breaks the specification on Boolean operators and builds the MTDFA by compositing minimized subautomata, (re- strict) is a direct translation but that is restricted to the only part useful to synthesis, (dfs-on-the-fly) is the on-the-fly version of "restrict" that follow a dfs order that stop on previously seen BDD nodes, solving the game as the automaton is generated, (dfs-strict-on-the-fly) stops on visited states, (bfs-on-the-fly) same as dfs-on-the-fly but using bfs order. The default is bfs-on-the-fly. Output options: --aiger[=ite|isop|both[+ud][+dc][+sub0|sub1|sub2]] encode the winning strategy as an AIG circuit and print it in AIGER format. The first word indicates the encoding to used: "ite" for If-Then-Else normal form; "isop" for irreducible sum of products; "both" tries both and keeps the smaller one. Other options further refine the encoding, see aiger::encode_bdd. Defaults to "ite". -d, --dot[=game|strategy:OPT|aig:OPT] Use dot format when printing the result (game, strategy, or AIG cir- cuit). The options that may be used as OPT depend on the nature of what is printed. For strategy, standard automata rendering options are supported (e.g., see ltl2tgba --dot). For AIG circuit, use (h) for horizontal and (v) for vertical layouts. --hide-status Hide the REALIZABLE or UNREALIZABLE line. (Hint: exit status is enough of an indication.) -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 au- tomata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transi- tion-based acceptance, (k) use state labels when possible, (l) sin- gle-line output, (v) verbose properties -q, --quiet suppress all normal output --realizability realizability only, do not compute a winning strategy Miscellaneous options: --help print this help --verbose verbose mode --version print program version Mandatory or optional arguments to long options are also mandatory or op- tional for any corresponding short options. BIBLIOGRAPHY The following paper describes how LTLf synthesis using MTDFA works in ltlf- synt. * Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman, Giuseppe De Gia- como, and Moshe Y. Vardi: Engineering an LTLf Synthesis Tool. Pro- ceedings of CIAA'25. LNCS 15981. pp. 129a147. REPORTING BUGS Report bugs to <spot@lrde.epita.fr>. COPYRIGHT Copyright (C) 2025 by the Spot authors, see the AUTHORS File for details. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/li- censes/gpl.html>. This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. SEE ALSO ltlf2dfa(1) ltlsynt(1) ltlfsynt (spot) 2.14.5 January 2026 LTLFSYNT(1)
NAME | SYNOPSIS | DESCRIPTION | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.FreeBSD.org/cgi/man.cgi?query=ltlfsynt&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>