LTS Termination Proof
by AProVE
Input
Integer Transition System

Initial Location:
l1, l3, l0, l2

Transitions: (prevariables and postvariables)
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 cutpointtransitions:
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)