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)