Name
Abstract | ||
|---|---|---|
Unsatisfiable cores, i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, have important uses in debugging specifications, speeding up search in model checking or SMT, and generating certificates of unsatisfiability. While unsatisfiable cores have been well investigated for Boolean SAT and constraint programming, the notion of unsatisfiable cores for temporal logics such as LTL has not received much attention. In this paper we investigate notions of unsatisfiable cores for LTL that arise from the syntax tree of an LTL formula, from converting it into a conjunctive normal form, and from proofs of its unsatisfiability. The resulting notions are more fine-grained than existing ones. We illustrate the benefits of the more fine-grained notions on examples from the literature. We extend some of the notions to realizability and we discuss the relationship of unsatisfiable and unrealizable cores with the notion of vacuity. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.scico.2010.11.004 | Sci. Comput. Program. |
Keywords | Field | DocType |
unsatisfiable core,ltl,temporal logic,fine-grained notion,constraint programming,unsatisfiable formula,unrealizable core,important use,boolean sat,debugging specification,model checking,unrealizable cores,ltl formula,unsatisfiable cores,conjunctive normal form | Programming language,Model checking,Computer science,Constraint programming,Abstract syntax tree,Theoretical computer science,Conjunctive normal form,Mathematical proof,Temporal logic,Realizability,Debugging | Journal |
Volume | Issue | ISSN |
77 | 7-8 | Science of Computer Programming |
Citations | PageRank | References |
16 | 0.61 | 85 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Viktor Schuppan | 1 | 409 | 17.49 |