Bounded Lᴛʟ sAtisfiability ChecKer
Welcome to BLACK’s website.
BLACK is a tool for testing the satisfiability of formulas in Linear Temporal Logic (LTL) and related logics.
LTL is a very popular specification language in the fields of formal verification and artificial intelligence. In these fields, it is important to be able to understand whether a given specification is satisfiable, unsatisfiable, or vacuously true. BLACK helps with this task.
BLACK consists of two components:
libblack, a C++ library with a well-defined API that can be linked by
any client application; and
black, a command-line tool that interfaces the library with the user.
This website documents the usage of both.
BLACK is open-source and released under the MIT license. For its source code, look at its GitHub repository.