| Autor: |
Geatti, Luca, Gigante, Nicola, Montanari, Angelo, Venturato, Gabriele |
| Předmět: |
|
| Zdroj: |
Journal of Automated Reasoning; Jun2024, Vol. 68 Issue 2, p1-32, 32p |
| Abstrakt: |
Linear temporal logic ( LTL ) and its variant interpreted on finite traces ( LTL f ) 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 LTL and LTL f formulas, 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 LTL and LTL f satisfiability checking based on Reynolds' tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
Full text from SpringerLink