Man Linux: Main Page and Category List


       lbt - LTL to Büchi Translator


       lbt < formula.txt > automaton.txt
       lbt2dot < automaton.txt >


       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.


       echo G p0 | lbt | lbt2dot | dotty -




              The real documentation for LBT.


       This manual page was written by Marko Mäkelä <>, 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)