Extracting unsatisfiable cores for LTL via temporal resolution

DOI10.1007/s00236-015-0242-1zbMath1338.68170arXiv1212.3884OpenAlexW3099891702MaRDI QIDQ266863

Viktor Schuppan

Publication date: 7 April 2016

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1212.3884

Mathematics Subject Classification ID

Related Items (2)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance

Uses Software

• Boost C++ Libraries
• NuSMV
• TSPASS
• Boost
• MUP
• VaqUoT
• TRP++
• VaqTree
• BGL

Cites Work

• 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
• Resolution proof transformation for compression and interpolation
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• The propositional dynamic logic of deterministic, well-structured programs
• A structure-preserving clause form translation
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal resolution using a breadth-first search algorithm
• Minimal sets on propositional formulae. Problems and reductions
• The complexity of propositional linear temporal logics in simple cases
• A transformation-based synthesis of temporal specification
• Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
• Minimally Unsatisfiable Boolean Circuits
• Implementing a fair monodic temporal logic prover
• Deductive verification of simple foraging robotic behaviours
• Interpolant Strength
• The complexity of propositional linear temporal logics
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Compressing Propositional Refutations
• Tools and Algorithms for the Construction and Analysis of Systems
• The Description Logic Handbook
• Linear Encodings of Bounded LTL Model Checking
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Debugging Unrealizable Specifications with Model-Based Diagnosis
• Boolean Abstraction for Temporal Logic Satisfiability
• Diagnostic Information for Realizability
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Clausal temporal resolution
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Sanity Checks in Formal Verification
• Symbolic Implementation of Alternating Automata
• Computer Aided Verification
• Software reliability methods. Foreword by Edmund M. Clarke
• Efficient detection of vacuity in temporal model checking

This page was built for publication: Extracting unsatisfiable cores for LTL via temporal resolution