  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 additional information about the time points at which the
subformulas of the UC are relevant for unsatisfiability. For example, in "(G p)
and (X not p)" the first occurrence of "p" is really only "relevant" for
unsatisfiability at time point 1 (time starts at time point 0). We present a
method to extract such information from the resolution graph of a temporal
resolution proof of unsatisfiability of an LTL formula. We implement our method
in TRP++, and we experimentally evaluate it. Source code of our tool is
available.

Logic in Computer Science;Software Engineering