debian man page for lbt

LBT(1)							      General Commands Manual							    LBT(1)

NAME
       lbt - LTL to Buchi 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 Buchi 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 Buchi 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 Makela <msmakela@tcs.hut.fi>, for the Debian GNU/Linux system (but may be used by others).  The lbt
       program was written by Mauno Ronkko and Heikki Tauriainen, and it was optimized by Marko Makela, who also wrote the lbt2dot filter.  Please
       see the copyright file in /usr/share/doc/lbt for details.

								  August 10, 2001							    LBT(1)