SAT meets tableaux for linear temporal logic satisfiability

DOI10.1007/S10817-023-09691-1MaRDI QIDQ6611959zbMATH OpenFDO

Authors Luca Geatti, Nicola Gigante, Angelo Montanari

Publication date 27 September 2024

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-023-09691-1

zbMATH Keywords

linear temporal logicSATtableaux

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A new rule for LTL tableaux
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• A one-pass tree-shaped tableau for LTL+past
• A PLTL-prover based on labelled superposition with partial model guidance
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• Computer Aided Verification
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• scientific article; zbMATH DE number 5604077 (Why is no real title available?)
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• Linear Encodings of Bounded LTL Model Checking
• LTL on finite and process traces: complexity results and a practical reasoner
• One-pass and tree-shaped tableau systems for \(\mathrm{TPTL}\) and \(\mathrm{TPTL}_b+\mathrm{Past}\)
• One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
• Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker
• Planning for temporally extended goals.
• Propositional temporal logics: decidability and completeness
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• The MathSAT5 SMT solver
• Theory and Applications of Satisfiability Testing

Cited in

(2)

• Inconsistency measurement in \(\mathrm{LTL_f}\) based on minimal inconsistent sets and minimal correction sets
• An optimal pastification algorithm for \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{F} \rbrack\) and \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{G} \rbrack \)

This page was built for publication: SAT meets tableaux for linear temporal logic satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6611959)