5 papers
RAGTIMER 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS (extended version)
Landon Taylor, Joshua Jeppson, Bingqing Hu +2
Transient reachability analysis of rare events in Continuous-Time Stochastic Vector Addition Systems (CTSVAS) such as Chemical Reaction Networks (CRNs) has proven a formidable chal…
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic s…
Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models
Landon Taylor, Joshua Jeppson, Ahmed Irfan +3
Highly-concurrent system models with vast state spaces like Chemical Reaction Networks (CRNs) that model biological and chemical systems pose a formidable challenge to cutting-edge…
Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces
Joshua Jeppson, Landon Taylor, Bingqing Hu +1
Rare events in Stochastic Vector Addition System (VAS) are of significant interest because, while extremely unlikely, they may represent undesirable behavior that can have adverse…
Tools at the Frontiers of Quantitative Verification
Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool suppo…