TRP++UC is a satisfiability solver for Linear Temporal Logic (LTL) that can extract fine-grained unsatisfiable cores for LTL. In particular, it annotates the subformulas of an unsatisfiable core with the time points at which they are relevant for unsatisfiability or it identifies groups of occurrences of a proposition that do not interact in a proof of unsatisfiability. TRP++UC extends TRP++ by Boris Konev and Ullrich Hustadt, which is based on temporal resolution.
TRP++UC is described in two papers: This Acta Informatica 2015 paper explains extraction of unsatisfiable cores via temporal resolution and grouping of occurrences of propositions in unsatisfiable cores, and this Theoretical Computer Science 2016 paper covers the annotation with sets of time points. For more information see the README. For information on TRP++ see its webpage. A general discussion of unsatisfiable cores for LTL can be found in this paper.
| Current version released on 28 June 2015 | download |
| Version used to obtain the experimental results in the Theoretical Computer Science 2016 paper | download |
| Version used to obtain the experimental results in the Acta Informatica 2015 paper | download |
| Version used to obtain the experimental results in the TIME 2013 paper | download |
| Version used to obtain the experimental results in the (post-) proceedings version of the QAPL 2013 paper | download |
| Version used to obtain the experimental results in the arXiv and the preliminary proceedings version of the QAPL 2013 paper | download |
| Examples used in the experiments of the Theoretical Computer Science 2016 paper | download |
| Examples used in the experiments of the Acta Informatica 2015 paper | download |
| Examples used in the experiments of the TIME 2013 paper | download |
| Examples used in the experiments of the (post-) proceedings version of the QAPL 2013 paper | download |
| Examples used in the experiments of the the arXiv and the preliminary proceedings version of the QAPL 2013 paper | download |
More examples (in particular, also satisfiable ones) can be obtained from an evaluation of LTL satisfiability solvers. For examples in SNF see a page by Boris Konev.
TRP++UC was written by Viktor Schuppan. Please send bug reports, comments, questions, etc to
|
© Viktor Schuppan Last modified 29 January 2016 |