LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
l7 l7 l7: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l11 l11 l11: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l1 l1 l1: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l3 l3 l3: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l13 l13 l13: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l2 l2 l2: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l9 l9 l9: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l4 l4 l4: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l6 l6 l6: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l10 l10 l10: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l8 l8 l8: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l0 l0 l0: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
l12 l12 l12: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5
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 { l4, l7, l6, l10, l11, l8, l3, l0, l2, l9 }.

2.1.1 Transition Removal

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

l0: 4 − x1
l2: 3 − x1
l3: 4 − x1
l4: 3 − x1
l7: 3 − x1
l6: 3 − x1
l10: 3 − x1
l9: 3 − x1
l8: 3 − x1
l11: 3 − x1

2.1.2 Transition Removal

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

l3: −2
l0: −2
l4: 0
l2: 0
l7: 0
l6: 0
l10: 0
l9: 0
l8: 0
l11: 0

2.1.3 Transition Removal

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

l3: 1
l0: 0
l2: −1 + 2⋅x1x2 + 3⋅x5
l4: −2 + 2⋅x1x2 + 3⋅x5
l7: −2 + 2⋅x1x2 + 3⋅x5
l6: −2 + 2⋅x1x2 + 3⋅x5
l10: −2 + 2⋅x1x2 + 3⋅x5
l9: −2 + 2⋅x1x2 + 3⋅x5
l8: −2 + 2⋅x1x2 + 3⋅x5
l11: −2 + 2⋅x1x2 + 3⋅x5

2.1.4 Transition Removal

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

l2: 4 − x2
l4: 4 − x2
l7: 3 − x2
l6: 3 − x2
l10: 3 − x2
l9: 3 − x2
l8: 3 − x2
l11: 3 − x2

2.1.5 Transition Removal

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

l2: 4 − x3
l4: 4 − x3
l7: 4 − x3
l6: 4 − x3
l10: 3 − x3
l9: 3 − x3
l8: 3 − x3
l11: 3 − x3

2.1.6 Transition Removal

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

l2: −1 − x3x4
l4: −1 − x3x4
l7: −6 − x4
l6: 4 − x4
l10: 4 − x4
l9: 4 − x4
l8: 3 − x4
l11: 3 − x4

2.1.7 Transition Removal

We remove transitions 4, 13, 6, 11, 8, 7, 9 using the following ranking functions, which are bounded by −5.

l2: −5
l4: −6
l7: −4
l6: −3
l10: −2
l9: −1
l8: 0
l11: 1

2.1.8 Trivial Cooperation Program

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

Tool configuration

AProVE