man lbt2dot (Commandes) - LTL to Bchi Translator

NAME

lbt - LTL to Bchi 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 Bchi 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 Mkel <msmakela@tcs.hut.fi>, for the Debian GNU/Linux system (but may be used by others). The lbt program was written by Mauno Rnkk and Heikki Tauriainen, and it was optimized by Marko Mkel, who also wrote the lbt2dot filter. Please see the copyright file in /usr/share/doc/lbt for details.