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.