Table of Contents


ltlfilt - filter files or lists of LTL/PSL formulas


ltlfilt [OPTION...] [FILENAME[/COL]...]


Read a list of formulas and output them back after some optional processing.

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


read all formulas using LBT’s prefix syntax


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

Error handling:


discard erroneous lines (default)


do not report syntax errors


output erroneous lines as-is without processing

Transformation options:


rewrite Boolean subformulas as irredundant sum of products (implies at least -r1)


when used with --relabel or --relabel-bool, output the relabeling map using #define statements


if any of those APs occur in the formula, add a term ensuring two of them may not be true at the same time. Use this option multiple times to declare independent groups of exclusive propositions.


transform LTLf (finite LTL) to LTL by introducing some ’alive’ proposition


negate each formula


rewrite formulas in negative normal form


relabel all atomic propositions, alphabetically unless specified otherwise


relabel Boolean subexpressions, alphabetically unless specified otherwise


rewrite operators W and M using U and R (this is an alias for --unabbreviate=WM)


remove X operators (valid only for stutter-insensitive properties)

-r, --simplify[=LEVEL]

simplify formulas according to LEVEL (see below); LEVEL is set to 3 if omitted


remove all occurrences of the operators specified by STR, which must be a substring of "eFGiMRW^", where ’e’, ’i’, and ’^’ stand respectively for <->, ->, and xor. If no argument is passed, the subset "eFGiMW^" is used.

The simplification LEVEL may be set as follows.


No rewriting


basic rewritings and eventual/universal rules


additional syntactic implication rules


better implications using containment

Filtering options (matching is done after transformation):


keep formulas that accept WORD


match formulas with a number of atomic propositions in RANGE


match Boolean formulas


match formulas with Boolean size in RANGE


match formulas equivalent to FORMULA


match pure eventualities


match guarantee formulas (even pathological)


match formulas implied by FORMULA


match formulas implying FORMULA


match liveness properties


match only LTL formulas (no PSL operator)


match obligation formulas (even pathological)


match persistence formulas (even pathological)


match recurrence formulas (even pathological)


keep formulas that reject WORD


match safety formulas (even pathological)


match formulas with size in RANGE

--stutter-insensitive, --stutter-invariant

match stutter-insensitive LTL formulas


synonym for --universal --eventual


match syntactic-guarantee formulas


match syntactic-obligation formulas


match syntactic-persistence formulas


match syntactic-recurrence formulas


match syntactic-safety formulas

--syntactic-stutter-invariant, --nox

match stutter-invariant formulas syntactically (LTL-X or siPSL)


match purely universal formulas

-u, --unique

drop formulas that have already been output (not affected by -v)

-v, --invert-match

select non-matching formulas

RANGE may have one of the following forms: ’INT’, ’INT..INT’, ’..INT’, or ’INT..’

WORD is lasso-shaped and written as ’BF;BF;...;BF;cycle{BF;...;BF}’ where BF are arbitrary Boolean formulas. The ’cycle{...}’ part is mandatory, but the prefix can be omitted.

Output options:

-0, --zero-terminated-output

separate output formulas with \0 instead of \n (for use with xargs -0)

-8, --utf8

output using UTF-8 characters

-c, --count

print only a count of matched formulas

--format=FORMAT, --stats=FORMAT

specify how each line should be output (default: "%f")

-l, --lbt

output in LBT’s syntax


output using LaTeX macros

-n, --max-count=NUM

output at most NUM formulas

-o, --output=FORMAT

send output to a file named FORMAT instead of standard output. The first formula sent to a file truncates it unless FORMAT starts with ’>>’.

-p, --full-parentheses

output fully-parenthesized formulas

-q, --quiet

suppress all normal output

-s, --spin

output in Spin’s syntax


output in Spot’s syntax (default)


output in Wring’s syntax

The FORMAT string passed to --format may use the following interpreted sequences:


the part of the line before the formula if it comes from a column extracted from a CSV file


the part of the line after the formula if it comes from a column extracted from a CSV file


a single %


the Boolean-length of the formula (i.e., all Boolean subformulas count as 1)


the formula (in the selected syntax)


the name of the input file

%h, %[vw]h

the class of the formula is the Manna-Pnueli hierarchy ([v] replaces abbreviations by class names, [w] for all compatible classes)


the original line number in the input file


the nesting depth of operator OP. OP should be a single letter denoting the operator to count, or multiple letters to fuse several operators during depth evaluation. Add ’~’ to rewrite the formula in negative normal form before counting.


wall-clock time elapsed in seconds (excluding parsing)


CPU time (excluding parsing), in seconds; Add LETTERS to restrict to(u) user time, (s) system time, (p) parent process, or (c) children processes.


the length (or size) of the formula


number of atomic propositions used in the


add LETTERS to list atomic propositions

with (n) no quoting, (s) occasional double-quotes

with C-style escape, (d) double-quotes with C-style escape, (c) double-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions

Miscellaneous options:


print this help


print program version

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

Exit status:


if some formulas were output (skipped syntax errors do not count)


if no formulas were output (no match)


if any error has been reported


If you would like to give a reference to this tool in an article, we suggest you cite the following paper:

Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA’13. LNCS 8172.

The following papers describe algorithms used by ltlfilt:

Kousha Etessami: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters 75(6): 261-263 (2000).

Describes the transformation behind the --remove-x option.

Thibaud Michaud and Alexandre Duret-Lutz: Practical stutter-invariance checks for ω-regular languages. Proceedings of SPIN’15. LNCS 9232.

Describes the algorithm used by --stutter-insensitive option.

Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA’07. LNCS 4762.

Describes the checks implemented by the --safety, --guarantee, and --obligation options.

Ivana Černá, Radek Pelánek: Relating Hierarchy of Temporal Properties to Model Checking. Proceedings of MFCS’03. LNCS 2747.

Describes the syntactic LTL classes matched by the --syntactic-safety, --syntactic-guarantee, --syntactic-obligation options, --syntactic-persistence, and --syntactic-recurrence options.

Kousha Etessami, Gerard J. Holzmann: Optimizing Büchi Automata. Proceedings of CONCUR’00. LNCS 1877.

Describe the syntactic LTL classes matched by --eventual, and --universal.

Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. Proceedings of IJCAI’13.

Describe the transformation implemented by --from-ltlf to reduce LTLf model checking to LTL model checking.


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


Copyright © 2018 Laboratoire de Recherche et Développement de l’Epita. 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.


randltl(1), ltldo(1)