Towards a notion of unsatisfiable and unrealizable cores for LTL
From MaRDI portal
Publication:433349
DOI10.1016/j.scico.2010.11.004zbMath1242.68075OpenAlexW2149150933MaRDI QIDQ433349
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
Logic in computer science (03B70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (6)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Analysing sanity of requirements for avionics systems ⋮ Tightening the contract refinements of a system architecture ⋮ Diagnosis of Deep Discrete-Event Systems ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Reactive synthesis with maximum realizability of linear temporal logic specifications
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Coverage metrics for temporal logic model checking
- Before and after vacuity
- Using branching time temporal logic to synthesize synchronization skeletons
- A structure-preserving clause form translation
- The complexity of facets resolved
- Symbolic model checking: \(10^{20}\) states and beyond
- An optimality result for clause form translation
- 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
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Towards a Notion of Unsatisfiable Cores for LTL
- On the Notion of Vacuous Truth
- Open Implication
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
- The Complexity of Generalized Satisfiability for Linear Temporal Logic
- Requirements Validation for Hybrid Systems
- Synthesis of Communicating Processes from Temporal Logic Specifications
- The complexity of propositional linear temporal logics
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Deterministic generators and games for Ltl fragments
- Tools and Algorithms for the Construction and Analysis of Systems
- Linear Encodings of Bounded LTL Model Checking
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- Boolean Abstraction for Temporal Logic Satisfiability
- Diagnostic Information for Realizability
- A Hybrid Algorithm for LTL Games
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Vacuity in Testing
- Formal Methods in Computer-Aided Design
- Formal Methods in Computer-Aided Design
- Correct Hardware Design and Verification Methods
- Solving Sequential Conditions by Finite-State Strategies
- Computer Aided Verification
- Clausal temporal resolution
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- Symbolic Implementation of Alternating Automata
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Efficient detection of vacuity in temporal model checking
This page was built for publication: Towards a notion of unsatisfiable and unrealizable cores for LTL
