TCS / Software / lbtt

lbtt - an LTL-to-Büchi translator testbench

lbtt is a tool for testing programs that translate formulas expressed in propositional linear temporal logic (LTL) into Büchi automata. The goal of the tool is to assist in the correct implementation of LTL-to-Büchi translation algorithms by providing an automated testing environment for LTL-to-Büchi translators. Additionally, the testing environment can be used for very basic profiling of different LTL-to-Büchi translators to evaluate their performance.

(For more detailed information, see, for example, the article ``H. Tauriainen and K. Heljanko, Testing LTL formula translation into Büchi automata, International Journal on Software Tools for Technology Transfer (STTT) 4(1):57-70, 2002''. Some reference material is also provided in the tool documentation.)

Obtaining the source code

lbtt is developed using C++. The sources can be compiled into an executable with, for example, version 3.0 (or newer) of the GNU Compiler Collection (GCC).

lbtt is free software, you may change and redistribute it under the terms of the GNU General Public License. lbtt comes with NO WARRANTY. See the GNU General Public License for details.

Download the source code (version 1.2.0, released on 30th August 2005; MD5: a7d497bde12ce582b37828ef7b640ed9)

Documentation

After uncompressing the sources, see the README file for brief installation instructions.

The main documentation of the tool can be found in the user's guide. Use the following links to view the documentation (edition 1.2.0) in various formats.

Old versions

Old versions of the source code with precompiled binaries for some platforms are available here.

Links

This WWW form can be used for generating the FormulaOptions blocks used in lbtt configuration files. The form has limited support for specifying relative (instead of absolute) priorities for the formula operators.

Here are links (in alphabetical order) to some available LTL-to-Büchi translator programs and model checking tools including an LTL-to-Büchi translator module. The lbtt source distribution includes a utility for interfacing the tool with LBT, SPIN and Spot.

Last update: 24th November, 2005