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

DOI10.1007/978-3-030-29026-9_1MaRDI QIDQ2180503zbMATH OpenOpenAlexFDO

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)

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

Describes a project that uses

Uses Software

• nuXmv
• MathSAT

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)