BLACK, short for Bounded Ltl sAtisfiability ChecKer, is a recently developed software tool for satisfiability checking of Linear Temporal Logic (LTL) formulas. It supports formulas using both future and past operators, interpreted over both infinite and finite traces. At its core, BLACK uses an incremental SAT encoding of the one-pass tree-shaped tableau for LTL recently developed by Reynolds, which guarantees completeness thanks to its particular pruning rule. This paper gives an overview of the tool, surveys the main design choices underlying its implementation, describes its features and discusses potential future developments.
BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker
Luca Geatti;Angelo Montanari
2021-01-01
Abstract
BLACK, short for Bounded Ltl sAtisfiability ChecKer, is a recently developed software tool for satisfiability checking of Linear Temporal Logic (LTL) formulas. It supports formulas using both future and past operators, interpreted over both infinite and finite traces. At its core, BLACK uses an incremental SAT encoding of the one-pass tree-shaped tableau for LTL recently developed by Reynolds, which guarantees completeness thanks to its particular pruning rule. This paper gives an overview of the tool, surveys the main design choices underlying its implementation, describes its features and discusses potential future developments.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
