# LTS Termination Proof

by manual

## Input

Integer Transition System
• Initial Location: l0
• Transitions: (pre-variables and post-variables)  l0 t1 l1: x = x ∧ y = y ∧ z = −1 l1 t2 l2: −5 ≤ x ∧ x = x + z ∧ y = 0 ∧ z = z − 1 l2 t3 l2: y < x ∧ x = x ∧ y = y + 1 ∧ z = z l2 t4 l1: x ≤ y ∧ x = x ∧ y = y ∧ z = z

## Proof

The following invariants are asserted.

 l0: TRUE l1: z < 0 l2: z < −1

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (l0) TRUE 1 (l1) z < 0 2 (l2) z < −1 3 (l2) z < −1 4 (l1) z < −1
• initial node: 0
• cover edges:  3 → 2 4 → 1
• transition edges:  0 t1 1 1 t2 2 2 t3 3 2 t4 4

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 l2 e l2: x = x ∧ y = y ∧ z = z
and for every transition t, a duplicate t is considered.

### 3 SCC Decomposition

We consider subproblems for each of the 1 SCC(s) of the program graph.

### 3.1 SCC Subproblem 1/1

Here we consider the SCC { l1, l2 }.

### 3.1.1 Transition Removal

We remove transition t2 using the following ranking functions, which are bounded by −5.

 l1: x l2: x
Hints:

### 3.1.2 SCC Decomposition

We consider subproblems for each of the 1 SCC(s) of the program graph.

### 3.1.2.1 SCC Subproblem 1/1

Here we consider the SCC { l2 }.

### 3.1.2.1.1 Transition Removal

We remove transition t3 using the following ranking functions, which are bounded by 0.

 l2: x − y
Hints:

### 3.1.2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

manual

• version: -