Linear temporal logic (LTL) and its variant interpreted on finite traces (LTLf) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for LTLand LTLfformulas, for which many techniques have been devised during the last decades. Among these are tableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for LTLand LTLfsatisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.
SAT Meets Tableaux for Linear Temporal Logic Satisfiability
Geatti L.;Montanari A.;
2024-01-01
Abstract
Linear temporal logic (LTL) and its variant interpreted on finite traces (LTLf) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for LTLand LTLfformulas, for which many techniques have been devised during the last decades. Among these are tableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for LTLand LTLfsatisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.File | Dimensione | Formato | |
---|---|---|---|
s10817-023-09691-1.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Licenza:
Creative commons
Dimensione
2.42 MB
Formato
Adobe PDF
|
2.42 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.