LTS Termination Proof
by AProVE
Input
Integer Transition System
-
Initial Location:
l1, l3, l0, l2
-
Transitions: (pre-variables and post-variables)
| l0 |
1 |
l1:
|
|
1 ≤ 0 |
| l1 |
2 |
l0:
|
|
0 ≤ 0 |
| l2 |
3 |
l0:
|
|
0 ≤ 0 |
| l3 |
4 |
l2:
|
|
0 ≤ 0 |
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpoint-transitions:
| l1 |
l1 |
l1: |
TRUE
|
| l3 |
l3 |
l3: |
TRUE
|
| l0 |
l0 |
l0: |
TRUE
|
| l2 |
l2 |
l2: |
TRUE
|
and for every transition t,
a duplicate t is considered.
2 SCC Decomposition
We consider subproblems for each of the 1 SCC(s) of the program graph.
2.1 SCC Subproblem 1/1
Here we consider the SCC
{ l1, l0 }.
2.1.1 Transition Removal
We remove transitions 1, 2
using the following ranking functions, which are bounded by
−1.
2.1.2 Trivial Cooperation Program
There are no more "sharp" transitions in the cooperation program.
Hence the cooperation termination is proved.
Tool configuration
AProVE
- version: AProVE Commit ID: unknown
- strategy:
Statistics for single proof: 100.00 % (4 real / 0 unknown / 0 assumptions / 4 total proof steps)