Preprocessing

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁
Temp_Vars:
Locations: f, g, h
Transitions:
g₁:f(X₀,X₁) -{0}> t₂:g(X₀,X₁) :|:
g₃:g(X₀,X₁) -{3}> t₄:g(X₀,X₁+UNIFORM(1, 3)) :|: 3+X₁ ≤ X₀ ∧ 0 ≤ 1
g₅:g(X₀,X₁) -{0}> t₆:h(X₀,X₁) :|: X₀ ≤ 2+X₁
g₇:h(X₀,X₁) → [2/3]:t₈:h(X₀,X₁-10) :+: [1/3]:t₉:h(X₀,X₁) :|: 10 ≤ X₁

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: inf {Infinity}
g₅: 1 {O(1)}
g₇: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g]

MPRF for transition t₄: g(X₀,X₁) -{3}> g(X₀,Temp_Int₂₆) :|: 0 ≤ 1 ∧ 1+X₁ ≤ Temp_Int₂₆ ∧ Temp_Int₁ ≤ 3+X₁ ∧ 1+X₁ ≤ Temp_Int₁ ∧ Temp_Int₂₆ ≤ 3+X₁ ∧ 3+X₁ ≤ X₀ ∧ Temp_Int₂+X₁ ≤ Temp_Int₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₁ ∧ Temp_Int₂+X₁ ≤ Temp_Int₁ ∧ 1 ≤ Temp_Int₂ ∧ Temp_Int₂ ≤ 3 ∧ 3+X₁ ≤ X₀ of depth 1:

new bound:

X₀+X₁ {O(n)}

MPRF:

• g: [X₀-X₁]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}

Run probabilistic analysis on SCC: [g]

Run classical analysis on SCC: [h]

MPRF for transition t₈: h(X₀,X₁) → h(X₀,X₁-10) :|: 10 ≤ X₁ of depth 1:

new bound:

3⋅X₀+5⋅X₁ {O(n)}

MPRF:

• h: [X₁]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}
(g₇,h), X₀: 4⋅X₀ {O(n)}
(g₇,h), X₁: 10⋅X₁+6⋅X₀ {O(n)}

Run probabilistic analysis on SCC: [h]

Plrf for transition g₇:h(X₀,X₁) → [2/3]:t₈:h(X₀,X₁-10) :+: [1/3]:t₉:h(X₀,X₁) :|: 10 ≤ X₁:

new bound:

3/4⋅X₁+9/20⋅X₀ {O(n)}

PLRF:

• h: 3/20⋅X₁

Use expected size bounds for entry point (g₅:g→[t₆:1:h],h)
Use classical time bound for entry point (g₅:g→[t₆:1:h],h)

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:29/20⋅X₀+7/4⋅X₁+2 {O(n)}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: 3/4⋅X₁+9/20⋅X₀ {O(n)}

Costbounds

Overall costbound: 39/10⋅X₀+9/2⋅X₁ {O(n)}
g₁: 0 {O(1)}
g₃: 3⋅X₀+3⋅X₁ {O(n)}
g₅: 0 {O(1)}
g₇: 3/2⋅X₁+9/10⋅X₀ {O(n)}

Sizebounds

(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}
(g₇,h), X₀: 4⋅X₀ {O(n)}
(g₇,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}