An explicit transition system construction approach to LTL satisfiability checking
From MaRDI portal
Publication:1707341
DOI10.1007/S00165-017-0442-2zbMATH Open1382.68142OpenAlexW2767756541MaRDI QIDQ1707341FDOQ1707341
Authors: Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi, Jifeng He, Lijun Zhang 
Publication date: 29 March 2018
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-017-0442-2
Recommendations
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- \(\mathrm{LTL}_{f}\) satisfiability checking
- Accelerating LTL satisfiability checking by SAT solvers
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
Cites Work
- Theory and Applications of Satisfiability Testing
- NuSMV: A new symbolic model checker
- Graph-Based Algorithms for Boolean Function Manipulation
- Depth-First Search and Linear Graph Algorithms
- Symbolic model checking: \(10^{20}\) states and beyond
- The complexity of propositional linear temporal logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Boolean Abstraction for Temporal Logic Satisfiability
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Clausal temporal resolution
- Symbolic Implementation of Alternating Automata
- Interpolation and SAT-based model checking.
- Title not available (Why is that?)
- SAT-Based Model Checking without Unrolling
- Bounded model checking using satisfiability solving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A decision procedure for propositional projection temporal logic with infinite models
- Towards a notion of unsatisfiable cores for LTL
- Title not available (Why is that?)
- Automata-Theoretic Model Checking Revisited
- Title not available (Why is that?)
- On the relationship between LTL normal forms and Büchi automata
Cited In (12)
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Checking simple properties of transition systems defined by Thue specifications
- Saturation-based incremental LTL model checking with inductive proofs
- Title not available (Why is that?)
- Accelerating LTL satisfiability checking by SAT solvers
- Variable and clause elimination for LTL satisfiability checking
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- An Asymptotically Correct Finite Path Semantics for LTL
- \(\mathrm{LTL}_{f}\) satisfiability checking
- Component-wise incremental LTL model checking
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- SAT-based explicit LTL reasoning and its application to satisfiability checking
Uses Software
This page was built for publication: An explicit transition system construction approach to LTL satisfiability checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1707341)
