---
name: "lbt"
section: "1"
platform: "linux"
package: "lbt"
version: "1.2.2-7"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/lbt"
---

# lbt(1)

LTL to Büchi Translator

## 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)](/dotty/1.md).

## 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.