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 in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1218137
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact