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

DOI10.1007/978-3-030-29026-9_1zbMATH Open1435.68368OpenAlexW2969232040MaRDI QIDQ2180503FDOQ2180503

Authors: Luca Geatti, Nicola Gigante, Angelo Montanari 

Publication date: 14 May 2020

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

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

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)

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

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)