Table of Contents


genltl - generate LTL formulas from scalable patterns


genltl [OPTION...]


Generate temporal logic formulas from predefined patterns.

Pattern selection:

--and-f=RANGE, --gh-e=RANGE




--and-gf=RANGE, --ccj-phi=RANGE, --gh-c2=RANGE



F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))


F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))

--ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) &


--dac-patterns[=RANGE], --spec-patterns[=RANGE]

Dwyer et al. [FMSP’98] Spec. Patterns for LTL (range should be included in 1..55)


Etessami and Holzmann [Concur’00] patterns (range should be included in 1..12)


G[0..n]((a S b) -> c) rewritten using future operators


F(p0 | XG(p1 | XG(p2 | ... XG(pn))))


(GFa1 & GFa2 & ... & GFan) <-> GFz


GF(a <-> X^n(a))


(GFa1 & GFa2 & ... & GFan) -> GFz


GF(a -> X^n(a))




(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))


!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))


G(p0 & XF(p1 & XF(p2 & ... XF(pn))))

--hkrss-patterns[=RANGE], --liberouter-patterns[=RANGE]

Holeček et al. patterns from the Liberouter project (range should be included in 1..55)


linear formula with doubly exponential DBA


quasilinear formula with doubly exponential DBA

--kv-psi=RANGE, --kr-n2=RANGE

quadratic formula with doubly exponential DBA









--or-fg=RANGE, --ccj-xi=RANGE


--or-g=RANGE, --gh-s=RANGE


--or-gf=RANGE, --gh-c1=RANGE


--p-patterns[=RANGE], --beem-patterns[=RANGE], --p[=RANGE]

Pelánek [Spin’07] patterns from BEEM (range should be included in 1..20)


Arbiter with n clients that sent requests (ri) and receive grants (gi). Standard semantics.


Arbiter with n clients that sent requests (ri) and receive grants (gi). Strict semantics.


(((p1 R p2) R p3) ... R pn)


(p1 R (p2 R (... R pn)))


n-bit counter


n-bit counter w/ carry


n-bit counter w/ carry (linear size)


n-bit counter (linear size)


Somenzi and Bloem [CAV’00] patterns (range should be included in 1..27)

--sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U



(GFa1&...&GFan) -> (GFb1&...&GFbn)




φ�\’,φ�\\,φ�\- from Sikert et al’s [CAV’16] paper (range should be included in 1..3)


G(p -> (q | Xq | ... | XX...Xq)


G(p -> (q | X(q | X(... | Xq)))


G(p -> (q & Xq & ... & XX...Xq)


G(p -> (q & X(q & X(... & Xq)))


G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...))))))

--u-left=RANGE, --gh-u=RANGE

(((p1 U p2) U p3) ... U pn)

--u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE

(p1 U (p2 U (... U pn)))

RANGE may have one of the following forms: ’INT’, ’INT..INT’, or ’..INT’. In the latter case, the missing number is assumed to be 1.

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

--format=FORMAT, --stats=FORMAT

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

-l, --lbt

output in LBT’s syntax


output using LaTeX macros

--negative, --negated

output the negated versions of all 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 ’>>’.


output the positive versions of all formulas (done by default, unless --negative is specified without --positive)

-p, --full-parentheses

output fully-parenthesized formulas

-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:


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 pattern

%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 argument of the pattern


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.


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.


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.

Prefixes used in pattern names refer to the following papers:


J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS’09.


M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property Specification Patterns for Finite-state Verification. Proceedings of FMSP’98.


K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. Proceedings of Concur’00. LNCS 1877.


J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin’06. LNCS 3925.


J. Holeček, T. Kratochvila, V. Řehák, D. � afránek, and P. � imeček: Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004.


P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. Proceedings of CAV’01. LNCS 2102.


O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic Automata. Proceedings of MoChArt’10. LNAI 6572.


O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. ACM Transactions on Computational Logic, 6(2):273-294, 2005.


D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata. Proceedings of GandALF’17. EPTCS 256.


R. Pelánek: BEEM: benchmarks for explicit model checkers Proceedings of Spin’07. LNCS 4595.


N. Piterman, A. Pnueli, and Y. Sa’ar: Synthesis of Reactive(1) Designs. Proceedings of VMCAI’06. LNCS 3855.


K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin’07. LNCS 4595.


F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. Proceedings of CAV’00. LNCS 1855.


S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi Automata for Linear Temporal Logic. Proceedings of CAV’16. LNCS 9780.


D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV’10. LNCS 6418.


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


Copyright © 2023 Laboratoire de Recherche de l’Epita (LRE) 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.


genaut(1), ltlfilt(1), randaut(1), randltl(1)