Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378): Difference between revisions

@@ Property / cites work @@
+Q4992524
@@ Property / cites work: Q4992524 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a notion of unsatisfiable and unrealizable cores for LTL
+Normal rank
@@ Property / cites work @@
+Locating Minimal Infeasible Constraint Sets in Linear Programs
+Normal rank
@@ Property / cites work @@
+Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Q4385542
@@ Property / cites work: Q4385542 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient detection of vacuity in temporal model checking
+Normal rank
@@ Property / cites work @@
+Sanity Checks in Formal Verification
@@ Property / cites work: Sanity Checks in Formal Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic Implementation of Alternating Automata
@@ Property / cites work: Symbolic Implementation of Alternating Automata / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Explaining Counterexamples Using Causality
@@ Property / cites work: Explaining Counterexamples Using Causality / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Extracting unsatisfiable cores for LTL via temporal resolution
+Normal rank
@@ Property / cites work @@
+Temporal logic can be more expressive
@@ Property / cites work: Temporal logic can be more expressive / rank @@
+Normal rank
@@ Property / cites work @@
+Clausal temporal resolution
@@ Property / cites work: Clausal temporal resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Temporal resolution using a breadth-first search algorithm
+Normal rank
@@ Property / cites work @@
+Q4012170
@@ Property / cites work: Q4012170 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804909
@@ Property / cites work: Q4804909 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Boolean Abstraction for Temporal Logic Satisfiability
+Normal rank
@@ Property / cites work @@
+A theory of diagnosis from first principles
@@ Property / cites work: A theory of diagnosis from first principles / rank @@
+Normal rank
@@ Property / cites work @@
+A correction to the algorithm in Reiter's theory of diagnosis
+Normal rank
@@ Property / cites work @@
+Vacuity Checking in the Modal Mu-Calculus*
@@ Property / cites work: Vacuity Checking in the Modal Mu-Calculus* / rank @@
+Normal rank
@@ Property / cites work @@
+Results on the propositional \(\mu\)-calculus
@@ Property / cites work: Results on the propositional \(\mu\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q2760241
@@ Property / cites work: Q2760241 / rank @@
+Normal rank
@@ Property / cites work @@
+The Description Logic Handbook
@@ Property / cites work: The Description Logic Handbook / rank @@
+Normal rank
@@ Property / cites work @@
+MUST: Provide a Finer-Grained Explanation of Unsatisfiability
+Normal rank
@@ Property / cites work @@
+Principles of Constraint Programming
@@ Property / cites work: Principles of Constraint Programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q2724150
@@ Property / cites work: Q2724150 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3490999
@@ Property / cites work: Q3490999 / rank @@
+Normal rank
@@ Property / cites work @@
+Reconstructing proofs at the assertion level
@@ Property / cites work: Reconstructing proofs at the assertion level / rank @@
+Normal rank
@@ Property / cites work @@
+Q4952309
@@ Property / cites work: Q4952309 / rank @@
+Normal rank
@@ Property / cites work @@
+Enhancing unsatisfiable cores for LTL with information on temporal relevance
+Normal rank
@@ Property / cites work @@
+On Context-Free Languages
@@ Property / cites work: On Context-Free Languages / rank @@
+Normal rank
@@ Property / cites work @@
+Q5678435
@@ Property / cites work: Q5678435 / rank @@
+Normal rank
@@ Property / cites work @@
+The complexity of propositional linear temporal logics
+Normal rank
@@ Property / cites work @@
+The propositional dynamic logic of deterministic, well-structured programs
+Normal rank
@@ Property / cites work @@
+The complementation problem for Büchi automata with applications to temporal logic
+Normal rank
@@ Property / cites work @@
+A structure-preserving clause form translation
@@ Property / cites work: A structure-preserving clause form translation / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic model checking: \(10^{20}\) states and beyond
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+A clausal resolution method for CTL branching-time temporal logic
+Normal rank
@@ Property / cites work @@
+Search strategies for resolution in temporal logics
+Normal rank
@@ Property / cites work @@
+Q3862379
@@ Property / cites work: Q3862379 / rank @@
+Normal rank
@@ Property / cites work @@
+Chrobak Normal Form Revisited, with Applications
@@ Property / cites work: Chrobak Normal Form Revisited, with Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Construction of Semilinear Representations of Languages Accepted by Unary Nondeterministic Finite Automata
+Normal rank
@@ Property / cites work @@
+Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
+Normal rank
@@ Property / cites work @@
+Deductive verification of simple foraging robotic behaviours
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4941841
@@ Property / cites work: Q4941841 / rank @@
+Normal rank
@@ Property / cites work @@
+A fully automatic theorem prover with human-style output
+Normal rank
@@ Property / cites work @@
+Q4583686
@@ Property / cites work: Q4583686 / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithms for computing minimal unsatisfiable subsets of constraints
+Normal rank
@@ Property / cites work @@
+Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Conjoining BDDs
@@ Property / cites work: Extended Resolution Proofs for Conjoining BDDs / rank @@
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Symbolic SAT Solving with Quantification
+Normal rank
@@ Property / cites work @@
+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.
+Normal rank
@@ Property / cites work @@
+Theory and applications of satisfiability testing -- SAT 2006. 9th international conference, Seattle, WA, USA, August 12--15, 2006. Proceedings.
+Normal rank