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: N. Bertrand, L. Bortolussi and H. Wiklicky (eds.): Quantitative Aspects of Programming Languages and Systems (2013-14), Theoretical Computer Science 655, Part B: pp. 155-192. Elsevier, 2016. doi:10.1016/j.tcs.2016.01.014. Substantially extended version of [Sch13b].
Download:
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:
- example from Sec. 1
- "every second time point" example from Sec. 2
- lift example from Sec. 2
- buffer example from Sec. 2
- running example 1 from Sec. 3, 4, and 6
- running example 2 from Sec. 4 and 6
- source: SNF
- command line to obtain resolution graph before pruning: trp++uc -s BFS -u -g snf --write-rg-before-pruning=running2_notpruned.dot running2.snf
- command line to obtain resolution graph after pruning: trp++uc -s BFS -u -g snf --write-rg-after-pruning=running2_pruned.dot running2.snf
- command line to obtain UC in SNF with sets of time points: trp++uc -s BFS -u -g snf --sets-of-time-points-uc running2.snf
- running example 3 from Sec. 4 and 6
- source: SNF
- command line to obtain resolution graph before pruning: trp++uc -s BFS -u -g snf --no-prune-failed-loop-search-its --write-rg-before-pruning=running3_notpruned.dot running3.snf
- command line to obtain resolution graph after pruning: trp++uc -s BFS -u -g snf --write-rg-after-pruning=running3_pruned.dot running3.snf
- command line to obtain UC in SNF with sets of time points: trp++uc -s BFS -u -g snf --sets-of-time-points-uc running3.snf
- business process example from Appendix B