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.