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
- A new one-pass tableau calculus for PLTL
- 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 67448 (Why is no real title available?)
- scientific article; zbMATH DE number 177248 (Why is no real title available?)
- Improved automata generation for linear temporal logic
- Improving the encoding of LTL model checking into SAT
- Interpolation and SAT-based model checking.
- NuSMV 2: An OpenSource tool for symbolic 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
- Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs
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
- Efficient decision procedures for model checking of linear time logic properties
- 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)
