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)