A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL

DOI10.1007/978-3-030-29026-9_1MaRDI QIDQ2180503zbMATHOpenAlexFDO

Authors Luca Geatti, Nicola Gigante, Angelo Montanari

Publication date 14 May 2020

Full work available at URL http://hdl.handle.net/11390/1167562

zbMATH Keywords

SATsatisfiabilitytemporal logictableau system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• A one-pass tree-shaped tableau for LTL+past
• A new rule for LTL tableaux
• An explicit transition system construction approach to LTL satisfiability checking
• scientific article; zbMATH DE number 2086516
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

Cited in

(4)

• SAT meets tableaux for linear temporal logic satisfiability
• A one-pass tree-shaped tableau for LTL+past
• Maximum satisfiability of mission-time linear temporal logic
• Towards certified model checking for PLTL using one-pass tableaux

Describes a project that uses

Uses Software

• MathSAT
• nuXmv

This page was built for publication: A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL

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