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-granular than existing ones. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-11623-0_7 | FSEN |
Keywords | Field | DocType |
unsatisfiable core,important use,boolean sat,syntax tree,model checking,debugging specification,constraint programming,unsatisfiable formula,ltl formula,conjunctive normal form,temporal logic | Model checking,Parse tree,Programming language,Computer science,Constraint programming,Abstract syntax tree,Theoretical computer science,Linear temporal logic,Conjunctive normal form,Temporal logic,Debugging | Conference |
Volume | ISSN | ISBN |
5961 | 0302-9743 | 3-642-11622-1 |
Citations | PageRank | References |
14 | 0.69 | 60 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Viktor Schuppan | 1 | 409 | 17.49 |