lbt - LTL to Büchi Translator

       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 MaunoRönkkö and HeikkiTauriainen,  and  it  was
       optimized  by  MarkoMäkelä,  who  also  wrote  the  lbt2dot  filter.   Please see the copyright file in
       /usr/share/doc/lbt for details.

                                                 August 10, 2001                                          LBT(1)

       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, Simpleon-the-flyautomaticverificationoflineartemporallogic.  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.

echo G p0 | lbt | lbt2dot | dotty -

/usr/share/doc/lbt/html/index.html
              The real documentation for LBT.

       lbt - LTL to Büchi Translator

dotty(1).

lbt < formula.txt > automaton.txtlbt2dot < automaton.txt > automaton.dot