Enhancing unsatisfiable cores for LTL with information on temporal relevance
From MaRDI portal
Publication:507378
DOI10.1016/j.tcs.2016.01.014zbMath1356.68146arXiv1306.2694OpenAlexW2169191644MaRDI QIDQ507378
Publication date: 6 February 2017
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1306.2694
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (3)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance
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
- Extracting unsatisfiable cores for LTL via temporal resolution
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- The propositional dynamic logic of deterministic, well-structured programs
- Results on the propositional \(\mu\)-calculus
- The complementation problem for Büchi automata with applications to temporal logic
- A structure-preserving clause form translation
- A theory of diagnosis from first principles
- A correction to the algorithm in Reiter's theory of diagnosis
- Symbolic model checking: \(10^{20}\) states and beyond
- Temporal resolution using a breadth-first search algorithm
- Tools and algorithms for the construction and analysis of systems. 10th international conference, TACAS 2004, held as part of the joint conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 -- April 2, 2004. Proceedings.
- A fully automatic theorem prover with human-style output
- Theory and applications of satisfiability testing -- SAT 2006. 9th international conference, Seattle, WA, USA, August 12--15, 2006. Proceedings.
- Algorithms for computing minimal unsatisfiable subsets of constraints
- Vacuity Checking in the Modal Mu-Calculus*
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
- Temporal logic can be more expressive
- Extended Resolution Proofs for Conjoining BDDs
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- Principles of Constraint Programming
- Explaining Counterexamples Using Causality
- Deductive verification of simple foraging robotic behaviours
- The complexity of propositional linear temporal logics
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- A clausal resolution method for CTL branching-time temporal logic
- Search strategies for resolution in temporal logics
- Efficient Construction of Semilinear Representations of Languages Accepted by Unary Nondeterministic Finite Automata
- Chrobak Normal Form Revisited, with Applications
- Reconstructing proofs at the assertion level
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- The Description Logic Handbook
- Theory and Applications of Satisfiability Testing
- Boolean Abstraction for Temporal Logic Satisfiability
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- A Machine-Oriented Logic Based on the Resolution Principle
- On Context-Free Languages
- Clausal temporal resolution
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
- Sanity Checks in Formal Verification
- Symbolic Implementation of Alternating Automata
- Computer Aided Verification
- Efficient detection of vacuity in temporal model checking
This page was built for publication: Enhancing unsatisfiable cores for LTL with information on temporal relevance
