An explicit transition system construction approach to LTL satisfiability checking
From MaRDI portal
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
- A decision procedure for propositional projection temporal logic with infinite models
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Automata-Theoretic Model Checking Revisited
- Boolean Abstraction for Temporal Logic Satisfiability
- Bounded model checking using satisfiability solving
- Clausal temporal resolution
- Depth-First Search and Linear Graph Algorithms
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 3937153 (Why is no real title available?)
- scientific article; zbMATH DE number 1189110 (Why is no real title available?)
- scientific article; zbMATH DE number 67448 (Why is no real title available?)
- scientific article; zbMATH DE number 177248 (Why is no real title available?)
- scientific article; zbMATH DE number 2086516 (Why is no real title available?)
- scientific article; zbMATH DE number 1903365 (Why is no real title available?)
- scientific article; zbMATH DE number 2102695 (Why is no real title available?)
- scientific article; zbMATH DE number 2102710 (Why is no real title available?)
- Interpolation and SAT-based model checking.
- NuSMV: A new symbolic model checker
- On the relationship between LTL normal forms and Büchi automata
- SAT-Based Model Checking without Unrolling
- Symbolic Implementation of Alternating Automata
- Symbolic model checking: \(10^{20}\) states and beyond
- The complexity of propositional linear temporal logics
- Theory and Applications of Satisfiability Testing
- Towards a notion of unsatisfiable cores for LTL
Cited in
(12)- Checking simple properties of transition systems defined by Thue specifications
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- An Asymptotically Correct Finite Path Semantics for LTL
- Accelerating LTL satisfiability checking by SAT solvers
- scientific article; zbMATH DE number 2102708 (Why is no real title available?)
- Component-wise incremental LTL model checking
- Saturation-based incremental LTL model checking with inductive proofs
- \(\mathrm{LTL}_{f}\) satisfiability checking
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Variable and clause elimination for LTL satisfiability checking
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)
