STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking

on YouTube ↗26m

" summary

STAMINA 2.0 implements a combined CTMC transient analysis with PRISM to produce min/max probability bounds in one pass, replaces predecessor-sum reachability with a forward-pass reachability propagation that resets passed mass to avoid trapped reachability, and dynamically lowers kappa from 1 instead of requiring manual tuning. Benchmarks (including a glitching hazard genetic circuit) show up to ~90% reduction in runtime and state count versus STAMINA 1.0 and large wins versus INFAMY, enabling previously intractable infinite-state CTMC checks.

AI-written summary · about

" chapters (10)

1. 0:00Start
2. 3:12Guided Early Path Termination
3. 5:08General Architecture of Stamina
4. 7:01Estimated Reachability
5. 7:53Combined Ctmc Analysis
6. 9:43The Trapped Reachability Problem
7. 13:25Algorithm Changes
8. 16:29Results
9. 17:02The Hazard Circuit
10. 22:33Conclusion