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