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
Authors: Viktor Schuppan 
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- 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)
- 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
- Diagnosis of deep discrete-event systems
- Tightening the contract refinements of a system architecture
- Towards a notion of unsatisfiable cores for LTL
- Debugging design errors by using unsatisfiable cores
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
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)
