BLACK¶
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 is open-source and released under the MIT license. For its source code, look at its GitHub repository.