Towards a notion of unsatisfiable and unrealizable cores for LTL
From MaRDI portal
Publication:433349
Recommendations
- Towards a notion of unsatisfiable cores for LTL
- Extracting unsatisfiable cores for LTL via temporal resolution
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Computing small unsatisfiable cores in satisfiability modulo theories
Cites work
- scientific article; zbMATH DE number 3930354 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 67448 (Why is no real title available?)
- scientific article; zbMATH DE number 3492660 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1979554 (Why is no real title available?)
- scientific article; zbMATH DE number 2081113 (Why is no real title available?)
- scientific article; zbMATH DE number 1487861 (Why is no real title available?)
- scientific article; zbMATH DE number 1798181 (Why is no real title available?)
- scientific article; zbMATH DE number 1903373 (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?)
- scientific article; zbMATH DE number 910719 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3189696 (Why is no real title available?)
- A Hybrid Algorithm for LTL Games
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
- A structure-preserving clause form translation
- An optimality result for clause form translation
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Before and after vacuity
- Beyond vacuity: towards the strongest passing formula
- Boolean Abstraction for Temporal Logic Satisfiability
- Clausal temporal resolution
- Computer Aided Verification
- Computer Aided Verification
- Correct Hardware Design and Verification Methods
- Coverage metrics for temporal logic model checking
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Deterministic generators and games for LTL fragments
- Diagnostic Information for Realizability
- Efficient detection of vacuity in temporal model checking
- Enhanced vacuity detection in linear temporal logic.
- Formal Methods in Computer-Aided Design
- Formal Methods in Computer-Aided Design
- Linear Encodings of Bounded LTL Model Checking
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- On the Notion of Vacuous Truth
- Open Implication
- Past is for free: On the complexity of verifying linear temporal properties with past
- Practically useful variants of definitional translations to normal form
- Requirements Validation for Hybrid Systems
- Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
- Solving Sequential Conditions by Finite-State Strategies
- Symbolic Implementation of Alternating Automata
- Symbolic model checking: \(10^{20}\) states and beyond
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Temporal induction by incremental SAT solving
- The Complexity of Generalized Satisfiability for Linear Temporal Logic
- The complexity of facets resolved
- The complexity of propositional linear temporal logics
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
- Towards a notion of unsatisfiable cores for LTL
- Using branching time temporal logic to synthesize synchronization skeletons
- Vacuity in Testing
- Verification, Model Checking, and Abstract Interpretation
Cited in
(9)- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Analysing sanity of requirements for avionics systems
- Tightening the contract refinements of a system architecture
- Diagnosis of deep discrete-event systems
- Debugging design errors by using unsatisfiable cores
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Towards a notion of unsatisfiable cores for LTL
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Extracting unsatisfiable cores for LTL via temporal resolution
This page was built for publication: Towards a notion of unsatisfiable and unrealizable cores for LTL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q433349)
