Extracting Unsatisfiable Cores for LTL via Temporal Resolution

This page contains additional material for the following paper:

V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. In: C. Sanchez, B. Venable, E. Zimanyi (eds.): Proceedings of the 20th International Symposium on Temporal Representation and Reasoning, TIME 2013, Pensacola, FL, USA, September 26-28, 2013, pp. 54-61. IEEE Computer Society, 2013.

Download:

• proceedings: publisher, preprint (zipped), BibTeX,
• full version: full (zipped),
• slides: slides.

Source Code

The source code of our tool as used in the experimental evaluation of the paper is here.

For updated versions see the web page of the tool.

The original version of TRP++ is available from Boris Konev's TRP++ page.

Experimental Evaluation

The benchmarks and data from our experimental evaluation are here.

Examples

The examples used in the paper:

• toy example from Sec. VII,
• lift example from Sec. VII,
• example for temporal resolution and uc extraction from Sec. VII, and
• complete example from App. E ltl, snf.