Enhancing unsatisfiable cores for LTL with information on temporal relevance

LTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specifications unsatisfiable cores (UCs), i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, are a well established means for debugging. However, little work has been done to help understanding a UC of an unsatisfiable LTL formula. In this paper we suggest to enhance a UC of an unsatisfiable LTL formula with information about the time points at which the subformulas of the UC are relevant for unsatisfiability. In previous work we showed how to obtain a UC in LTL by translating the LTL formula into a clausal normal form, applying temporal resolution, extracting a clausal UC from the resolution proof, and mapping the clausal UC back to a UC in LTL. In this paper we extend that method by extracting information at which time points the clauses of a clausal UC are relevant for unsatisfiability from a resolution proof and by transferring that information to a UC in LTL. We implement our method in TRP++, and we experimentally evaluate it.