LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
l5 l5 l5: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l7 l7 l7: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l11 l11 l11: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l1 l1 l1: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l3 l3 l3: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l13 l13 l13: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l18 l18 l18: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l17 l17 l17: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l9 l9 l9: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l14 l14 l14: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l4 l4 l4: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l10 l10 l10: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l6 l6 l6: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l8 l8 l8: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l15 l15 l15: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l16 l16 l16: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l0 l0 l0: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
l12 l12 l12: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18
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 { l5, l7, l11, l3, l13, l9, l14, l4, l10, l6, l8, l15, l16, l12 }.

2.1.1 Transition Removal

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

l4: x5 + x6
l6: x5 + x6
l3: −1 − x5 + x6
l5: −1 − x5 + x6
l9: −1 − x5 + x6
l10: −1 − x5 + x6
l11: −1 − x5 + x6
l14: −1 − x5 + x6
l13: −1 − x5 + x6
l12: −1 − x5 + x6
l15: −1 − x5 + x6
l16: −1 − x5 + x6
l8: −1 − x5 + x6
l7: −1 − x5 + x6

2.1.2 Transition Removal

We remove transitions 6, 4, 8, 10, 13, 12, 15, 17, 21, 20, 19, 22 using the following ranking functions, which are bounded by 0.

l4: 0
l6: −1
l3: 1
l5: 1
l9: 2
l10: 2
l11: 3
l14: 4
l13: 5
l12: 5
l15: 6
l16: 7
l8: 8
l7: 8

2.1.3 Transition Removal

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

l5: x1 + x4
l3: x1 + x4
l10: −1 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x13 + 13⋅x17 + 14⋅x18
l9: −1 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x13 + 13⋅x17 + 14⋅x18
l12: −1 − 2⋅x1 + 15⋅x2 + 16⋅x3 + 17⋅x4 + x5 + 18⋅x6 + 19⋅x7 + 20⋅x8 + 21⋅x9 + 22⋅x10 + 23⋅x11 + 24⋅x12 + 25⋅x13 + 26⋅x14 + 27⋅x15 + 28⋅x16 + 29⋅x17 + 30⋅x18
l13: −1 − 2⋅x1 + 15⋅x2 + 16⋅x3 + 17⋅x4 + x5 + 18⋅x6 + 19⋅x7 + 20⋅x8 + 21⋅x9 + 22⋅x10 + 23⋅x11 + 24⋅x12 + 25⋅x13 + 26⋅x14 + 27⋅x15 + 28⋅x16 + 29⋅x17 + 30⋅x18
l7: −1 − 2⋅x1 + 31⋅x2 + 32⋅x3 + 33⋅x4 + x5 + 34⋅x6 + 35⋅x7 + 36⋅x8 + 37⋅x9 + 38⋅x10 + 39⋅x11 + 40⋅x12 + 41⋅x14 + 42⋅x15 + 43⋅x16 + 44⋅x18
l8: −3 − 2⋅x1 + 31⋅x2 + 32⋅x3 + 33⋅x4 + x5 + 34⋅x6 + 35⋅x7 + 36⋅x8 + 37⋅x9 + 38⋅x10 + 39⋅x11 + 40⋅x12 + 41⋅x14 + 42⋅x15 + 43⋅x16 + 44⋅x18

2.1.4 Transition Removal

We remove transitions 24, 9 using the following ranking functions, which are bounded by 0.

l5: 1
l3: 0
l10: x1 + x5
l9: x1 + x5
l12: −1 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x13 + 13⋅x14 + 14⋅x15 + 15⋅x16 + 16⋅x17 + 17⋅x18
l13: −1 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x13 + 13⋅x14 + 14⋅x15 + 15⋅x16 + 16⋅x17 + 17⋅x18
l7: −1 − 2⋅x1 + 18⋅x2 + 19⋅x3 + 20⋅x4 + x5 + 21⋅x6 + 22⋅x7 + 23⋅x8 + 24⋅x9 + 25⋅x10 + 26⋅x11 + 27⋅x12 + 28⋅x14 + 29⋅x15 + 30⋅x16 + 31⋅x18
l8: −1 − 2⋅x1 + 18⋅x2 + 19⋅x3 + 20⋅x4 + x5 + 21⋅x6 + 22⋅x7 + 23⋅x8 + 24⋅x9 + 25⋅x10 + 26⋅x11 + 27⋅x12 + 28⋅x14 + 29⋅x15 + 30⋅x16 + 31⋅x18

2.1.5 Transition Removal

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

l10: 1
l9: 0
l12: x1 + x5
l13: x1 + x5
l7: −1 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x14 + 13⋅x15 + 14⋅x16 + 15⋅x18
l8: −3 − 2⋅x1 + 2⋅x2 + 3⋅x3 + 4⋅x4 + x5 + 5⋅x6 + 6⋅x7 + 7⋅x8 + 8⋅x9 + 9⋅x10 + 10⋅x11 + 11⋅x12 + 12⋅x14 + 13⋅x15 + 14⋅x16 + 15⋅x18

2.1.6 Transition Removal

We remove transitions 11, 23 using the following ranking functions, which are bounded by 0.

l12: 1
l13: 0
l7: x1 + x5
l8: x1 + x5

2.1.7 Transition Removal

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

l7: 0
l8: −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