BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker

Luca Geatti; Nicola Gigante; A Montanari

Back

BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker

Conference proceeding

Open access

Peer reviewed

BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker

Luca Geatti, Nicola Gigante and A Montanari

Proceedings of the 3rd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis, Vol.2987, pp.7-12

CEUR Workshop Proceedings, 2987

3rd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (Padova, 22/09/2021 - 22/09/2021)

2021

Handle:

https://hdl.handle.net/10863/23933

Abstract

Linear temporal logic

SAT

Tableaux methods

BLACK, short for Bounded Ltl sAtisfiability ChecKer, is a recently developed software tool for satisfia- bility 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.

Files and links (2)

pdf

paper2721.84 kBDownload View

Open Access

url

http://ceur-ws.org/Vol-2987/View

Details

Title: BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker
Creators: Luca Geatti
Nicola Gigante
A Montanari
Publication Details: Proceedings of the 3rd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis, Vol.2987, pp.7-12
Editor(s): Della Monica D, Pozzato GL, Scala E
ISSN: 1613-0073
Conference: 3rd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (Padova, 22/09/2021 - 22/09/2021)
Series / Volume: CEUR Workshop Proceedings
2987
Publisher: CEUR-WS
Format: Online
Number of pages: 6
Identifiers: (UNIBZ)45726622
991006321597801241
Scopus ID: 2-s2.0-85118197572
Academic Unit: Faculty of Computer Science
Language: English
Resource Type: Conference proceeding
Author Names String: Geatti L, Gigante N, Montanari A
Additional Description: Editors/Supervisors: Della Monica D, Pozzato GL, Scala E

Metrics

42 File views/ downloads

21 Record Views