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

DOI10.1007/978-3-030-29026-9_1zbMath1435.68368OpenAlexW2969232040MaRDI QIDQ2180503

Angelo Montanari, Luca Geatti, Nicola Gigante

Publication date: 14 May 2020

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

zbMATH Keywords

temporal logicsatisfiabilitySATtableau 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)

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