Preprocessing

Eliminate variables [X₀] that do not contribute to the problem

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars:
Temp_Vars:
Locations: f, g, h, j, loopstop
Transitions:
g₀:f(X₀) -{0}> t₁:g(X₀) :|:
g₂:g(X₀) → [1/2]:t₃:h(0) :+: [1/2]:t₄:loopstop(1) :|:
g₅:h(X₀) -{2}> t₆:g(X₀) :|:
g₇:loopstop(X₀) → t₈:j(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₅: inf {Infinity}
g₇: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g; h]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [g; h]

Plrf for transition g₂:g(X₀) → [1/2]:t₃:h(0) :+: [1/2]:t₄:loopstop(1) :|: :

new bound:

2 {O(1)}

PLRF:

• g: 2
• h: 2
• loopstop: 0

Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₅:h(X₀) -{2}> t₆:g(X₀) :|: :

new bound:

1 {O(1)}

PLRF:

• g: 1
• h: 2
• loopstop: 0

Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Run classical analysis on SCC: [loopstop]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:5 {O(1)}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 1 {O(1)}
g₇: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [loopstop]

Run classical analysis on SCC: [j]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:5 {O(1)}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 1 {O(1)}
g₇: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [j]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:5 {O(1)}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 1 {O(1)}
g₇: 1 {O(1)}

Costbounds

Overall costbound: 7 {O(1)}
g₀: 0 {O(1)}
g₂: 4 {O(1)}
g₅: 2 {O(1)}
g₇: 1 {O(1)}

Sizebounds