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.): Special Issue: Temporal Representation and Reasoning (TIME'13) - Part 2, Acta Informatica 53 (3) 2016: pp. 247-299. Springer, 2015. doi:10.1007/s00236-015-0242-1. Invited, substantially extended version of [Sch13c].
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:
- toy example from Sec. 2.1
- source: LTL
- command line: trp++uc -s BFS -f ltl -u -g ltl --no-nnf --no-ltl-simplification req_gnt.trp
- lift example from Sec. 2.2
- source: LTL
- command line: trp++uc -s BFS -f ltl -u -g ltl --no-nnf --no-ltl-simplification lift.trp
- running example for the translation from LTL into SNF, for temporal resolution, and for uc extraction from Sec. 3, 4
- source: LTL
- command line: trp++uc -s BFS -f ltl -u -g ltl --no-ltl-simplification running.trp
- source: SNF
- command line: trp++uc -s BFS -u -g snf running.snf
- first grouped propositions example from Sec. 5.2
- source: LTL
- command line: trp++uc -s BFS -f ltl -u --partitioned-propositions-uc -g ltl --no-ltl-simplification groupedpropositions1.trp
- second grouped propositions example from Sec. 5.2
- source: SNF
- command line: trp++uc -s BFS -u --partitioned-propositions-uc -g snf groupedpropositions2.snf
- grouped propositions example from Sec. 7.7
- source: LTL
- command line: trp++uc -s BFS -f ltl -u --partitioned-propositions-uc -g ltl --no-nnf liftf_b_l3_3.trp
- comparison with related approaches example from Sec. 7.8
- trp++uc source: LTL
- trp++uc command line: trp++uc -s BFS -f ltl -u -a proofdeletion -g ltl --sharing=none --no-nnf --no-ltl-simplification liftf_l1_2.trp
- PLTL-MUP tool: here
- PLTL-MUP source: LTL
- PLTL-MUP command line: cat liftf_l1_2.pltl|pltlmup
- procmine tool: here
- procmine source: LTL, DomainKnowledge.txt
- procmine command line: rm -f constraints.pltl; cp liftf_l1_2.procmine constraints.pltl; inconanalysis 2 1