## 1 Overview

`lbtt` is a tool for testing programs that translate
formulas expressed in propositional linear temporal logic (LTL) into
Büchi automata. These finite-state automata over infinite words are
used e.g. in automata-theoretic model checking
[VW86],
[Var96],
where they can help in detecting errors in the specifications of finite-state
hardware or software systems. Usually the model checking procedure involves
first composing an
automaton with a formal model of a given system, and the result of the
composition reveals whether any computation path of the system violates
some property that the automaton represents.
(For an introduction to model checking techniques in general, see,
for example,
[CGP99].)

The property to be model checked can be specified as an
LTL formula, and the Büchi automaton used for model checking is obtained
automatically from the formula with a translation algorithm.
(For descriptions and optimization techniques for such algorithms, see the
references, for example,
[VW86],
[Isl94],
[GPVW95],
[Cou99]
[DGV99],
[Ete99],
[SB00],
[EH00],
[EWS01],
[GO01],
[Gei01],
[Sch01],
[Wol01],
[Ete02],
[GL02],
[GSB02],
[Thi02],
[Fri03],
[GO03],
[Lat03],
[ST03].)
In practice, ensuring the correctness of the implementation of such a
translation algorithm is crucial to guarantee the soundness of the
implementation of a model checking procedure.

The goal of `lbtt` is to assist implementing LTL-to-Büchi
translation algorithms correctly by providing an automated
testing environment for LTL-to-Büchi translators. Testing consists of running
LTL-to-Büchi translators on randomly generated (or user-specified) LTL
formulas as input and then performing simple consistency checks on the
resulting automata to test whether the translators seem to function correctly
in practice. (See
[TH02]
for more information on the theory behind the testing methods.) If the test
results suggest that there is an error in an implementation,
`lbtt` can generate sample data which causes
a test failure and which may also be useful for debugging the
implementation.

Additionally, the testing environment can be used for very basic profiling of
different LTL-to-Büchi translators to evaluate their performance.

*Note: although *lbtt* might be able to detect inconsistent
behavior in an LTL-to-Büchi translator, it is only a testing tool and is
therefore incapable of formally proving any translation algorithm
implementation to be correct. Therefore, the test results should never be used
as the sole basis for any formal conclusions about the correctness of an
implementation.
*