Towards a notion of unsatisfiable and unrealizable cores for LTL
From MaRDI portal
Publication:433349
DOI10.1016/J.SCICO.2010.11.004zbMATH Open1242.68075OpenAlexW2149150933MaRDI QIDQ433349FDOQ433349
Publication date: 13 July 2012
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.11.004
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
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- A structure-preserving clause form translation
- The complexity of facets resolved
- Symbolic model checking: \(10^{20}\) states and beyond
- Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
- The complexity of propositional linear temporal logics
- Title not available (Why is that?)
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Linear Encodings of Bounded LTL Model Checking
- Computer Aided Verification
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- Boolean Abstraction for Temporal Logic Satisfiability
- Diagnostic Information for Realizability
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Clausal temporal resolution
- Symbolic Implementation of Alternating Automata
- Computer Aided Verification
- Efficient detection of vacuity in temporal model checking
- Title not available (Why is that?)
- Using branching time temporal logic to synthesize synchronization skeletons
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- An optimality result for clause form translation
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the Notion of Vacuous Truth
- Computer Aided Verification
- Title not available (Why is that?)
- Deterministic generators and games for Ltl fragments
- The Complexity of Generalized Satisfiability for Linear Temporal Logic
- Temporal induction by incremental SAT solving
- Verification, Model Checking, and Abstract Interpretation
- Solving Sequential Conditions by Finite-State Strategies
- Before and after vacuity
- Practically useful variants of definitional translations to normal form
- Past is for free: On the complexity of verifying linear temporal properties with past
- Beyond vacuity: towards the strongest passing formula
- Towards a notion of unsatisfiable cores for LTL
- Open Implication
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
- Requirements Validation for Hybrid Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Hybrid Algorithm for LTL Games
- Vacuity in Testing
- Formal Methods in Computer-Aided Design
- Formal Methods in Computer-Aided Design
- Correct Hardware Design and Verification Methods
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- Coverage metrics for temporal logic model checking
Cited In (8)
- Extracting unsatisfiable cores for LTL via temporal resolution
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Analysing sanity of requirements for avionics systems
- Tightening the contract refinements of a system architecture
- Towards a notion of unsatisfiable cores for LTL
- Debugging design errors by using unsatisfiable cores
- Diagnosis of Deep Discrete-Event Systems
- Reactive synthesis with maximum realizability of linear temporal logic specifications
Uses Software
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)
