SAT-based explicit LTL reasoning and its application to satisfiability checking
From MaRDI portal
Publication:2335900
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
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
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