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
Geatti L.;Montanari A.
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 | Dimensione | Formato | |
|---|---|---|---|
|
paper2.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
721.84 kB
Formato
Adobe PDF
|
721.84 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
