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.)
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.1, released on 9 April 2008; MD5: 08413aefc82a06748ad2cc66e40eb83a)
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 of the source code are available here.
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.