NAME
lbt - LTL to Büchi Translator
SYNOPSIS
lbt < formula.txt > automaton.txt
lbt2dot < automaton.txt > automaton.dot
DESCRIPTION
This manual page documents briefly the lbt and lbt2dot commands. This
manual page was written for the Debian GNU/Linux distribution because
the original program does not have a manual page. Instead, it has
documentation in HTML format; see below.
lbt is a filter that translates a linear temporal logic (LTL) formula
to a corresponding generalized Büchi automaton. The translation is
based on the algorithm by Gerth, Peled and Vardi presented at PSTV’95,
Simple on-the-fly automatic verification of linear temporal logic.
Hardly any optimizations are implemented, and the generated automaton
is often bigger than necessary. But on the other hand, it should
always be correct.
The filter lbt2dot can be used to translate Büchi automata from the lbt
output format to GraphViz format for visualization.
EXAMPLE
echo G p0 | lbt | lbt2dot | dotty -
SEE ALSO
dotty(1).
FILES
/usr/share/doc/lbt/html/index.html
The real documentation for LBT.
AUTHOR
This manual page was written by Marko Mäkelä <msmakela@tcs.hut.fi>, for
the Debian GNU/Linux system (but may be used by others). The lbt
program was written by Mauno Rönkkö and Heikki Tauriainen, and it was
optimized by Marko Mäkelä, who also wrote the lbt2dot filter. Please
see the copyright file in /usr/share/doc/lbt for details.
August 10, 2001 LBT(1)