SAT-based explicit LTL reasoning and its application to satisfiability checking

DOI10.1007/s10703-018-00326-5zbMath1425.68259OpenAlexW2907580149WikidataQ128686846 ScholiaQ128686846MaRDI QIDQ2335900

Geguang Pu, Shufang Zhu, Moshe Y. Vardi, Jianwen Li, Li-jun Zhang

Publication date: 18 November 2019

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-018-00326-5

zbMATH Keywords

linear temporal logicsatisfiability checkingSAT-based LTL checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Temporal logic (03B44)

Uses Software

• MiniSat
• SPIN
• NuSMV
• SPOT
• TRP++
• nuXmv
• InKreSAT
• Leviathan

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Variable and clause elimination for LTL satisfiability checking
• Optimized temporal monitors for SystemcC
• A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
• On Improving MUS Extraction Algorithms
• SAT-Based Model Checking without Unrolling
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• Accelerating LTL satisfiability checking by SAT solvers
• Building decision procedures for modal logics from propositional decision procedures — The case study of modal K
• Propositional Temporal Proving with Reductions to a SAT Problem
• InKreSAT: Modal Reasoning via Incremental Reduction to SAT
• Theory and Applications of Satisfiability Testing
• Interpolants and Symbolic Model Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Clausal temporal resolution
• Computer Aided Verification

This page was built for publication: SAT-based explicit LTL reasoning and its application to satisfiability checking