Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance

This page contains additional material for the following paper:

V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: L. Bortolussi, H. Wiklicky (eds.): Proceedings of the Eleventh International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Rome, Italy, March 23-24, 2013. Volume 117 of Electronic Proceedings in Theoretical Computer Science, pp. 49-65. Open Publishing Association, 2013.

Download:

• (post-) proceedings: publisher, local (zipped), BibTeX,
• preliminary proceedings: preprint (zipped), BibTeX,
• full version: full (zipped), and
• slides: slides.

Source Code

The source code of our tool as used in the experimental evaluation of the paper is here: (post-) proceedings, preliminary proceedings.

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: (post-) proceedings, preliminary proceedings.

Examples

The examples used in the paper:

• simple example from abstract/introduction,
• example for temporal resolution and uc extraction from Sec. 4 and 6,
• more complex example from Sec. 5,
• lift example from Sec. 7,
• buffer specification from App. C, and
• business process specification from App. C.