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)