Extracting unsatisfiable cores for LTL via temporal resolution

DOI10.1007/S00236-015-0242-1zbMATH Open1338.68170arXiv1212.3884OpenAlexW3099891702MaRDI QIDQ266863FDOQ266863

Authors: Viktor Schuppan 

Publication date: 7 April 2016

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

Abstract: Unsatisfiable cores (UCs) are a well established means for debugging in a declarative setting. Still, there are few tools that perform automated extraction of UCs for LTL. Existing tools compute a UC as an unsatisfiable subset of the set of top-level conjuncts of an LTL formula. Using resolution graphs to extract UCs is common in other domains such as SAT. In this article we construct and optimize resolution graphs for temporal resolution as implemented in the temporal resolution-based solver TRP++, and we use them to extract UCs for propositional LTL. The resulting UCs are more fine-grained than the UCs obtained from existing tools because UC extraction also simplifies top-level conjuncts instead of treating them as atomic entities. For example, given an unsatisfiable LTL formula of the form $$ existing tools return $phi$ as a UC irrespective of the complexity of $psi$ and $ps{i}^{\prime }$, whereas the approach presented in this article continues to remove parts not required for unsatisfiability inside $psi$ and $ps{i}^{\prime }$. Our approach also identifies groups of occurrences of a proposition that do not interact in a proof of unsatisfiability. We implement our approach in TRP++. Our experimental evaluation demonstrates that our approach (i) extracts UCs that are often significantly smaller than the input formula with an acceptable overhead and (ii) produces more fine-grained UCs than competing tools while remaining at least competitive in terms of run time and memory usage. The source code of our tool is publicly available.

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

Recommendations

• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Towards a notion of unsatisfiable cores for LTL
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Computing small unsatisfiable cores in satisfiability modulo theories

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• A structure-preserving clause form translation
• Minimal sets on propositional formulae. Problems and reductions
• Title not available (Why is that?)
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal resolution using a breadth-first search algorithm
• The complexity of propositional linear temporal logics in simple cases
• A transformation-based synthesis of temporal specification
• Extracting unsatisfiable cores for LTL via temporal resolution
• Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
• Resolution theorem proving
• 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
• Title not available (Why is that?)
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computing minimally unsatisfiable subformulas: state of the art and future directions
• Resolution proof transformation for compression and interpolation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• 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
• Enhanced vacuity detection in linear temporal logic.
• Software reliability methods. Foreword by Edmund M. Clarke
• Efficient detection of vacuity in temporal model checking
• The propositional dynamic logic of deterministic, well-structured programs

Cited In (5)

• 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
• Towards a notion of unsatisfiable cores for LTL
• Enhancing unsatisfiable cores for LTL with information on temporal relevance

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q266863)