RAGTIMER 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS (extended version)

1 Introduction

• CTSVAS transient reachability analysis challenges current tools because PMC requires an explicit state space, while realistic CRNs can have infinite or intractably large spaces and rare events.In biochemical and synthetic biological models, even low species concentrations can have pathological consequences.Source: §1 · pp. 1–2
• Ragtimer builds a partial CTSVAS state space by enumerating traces to target states and expanding them to exploit concurrency and cycles.Its trace analysis yields a guaranteed lower bound on rare-event probability.Source: §1 · p. 2
• Ragtimer outperforms cutting-edge PMC tools in runtime and probability calculation and refutes rare-event simulation estimates on challenging CRN models.The paper presents it as an attractive alternative for transient probabilistic analysis of CTSVAS models.Source: §1 · p. 2
• Ragtimer 1.0 is developed and benchmarked for scalability, with a novel input format intended to improve accessibility for users who are not formal-methods experts.The paper also reports runtime and probability improvements over Ragtimer 0.1.Source: §1 · p. 2

2 Background Information

• A CTSVAS is a vector-state model with ordered nonnegative-integer variables, transitions carrying guards, updates, and rate functions, and an initial state.A transient target asks whether a CSL state formula is reached within a time bound; analyzing it requires an explicit state space.Source: §2 · pp. 2–3
• A partial state space assigns unexplored states to an absorbing state assumed not to satisfy the target, yielding a guaranteed probability lower bound; assuming it does satisfy the target gives an uninformative upper bound for Ragtimer’s rare-event-focused space.The paper notes that nearly all probability may be redirected to the absorbing state because the included traces lead to rare events.Source: §2 · p. 3

2.1 Motivating Example

• The Modified Yeast Polarization model targets a rise in Gbg from 0 to 50 within 20 seconds and has an infinite state space with a rare-event trace requiring at least 100 low-probability firings.Its highly concurrent and cyclical structure challenges cutting-edge PMC tools; an example trace uses 50 firings each of R8 and R5.Source: §2.1 · p. 4

2.2 Importance of Lower Probability Bounds

• A guaranteed lower bound can help biologists estimate the minimum cell population needed to observe a rare event with confidence.For a small per-cell lower bound x and 95% confidence, the text gives the approximation n ≥ 3/x; an upper bound alone could lead to under-provisioning.Source: §2.2 · pp. 4–5
• For biosensors, a guaranteed lower bound on early activation probability helps estimate how many independent cells are needed to observe at least one rapidly responding cell.An upper bound alone does not guarantee that early activation is sufficiently likely to be observed in a finite population.Source: §2.2 · p. 5

3.1 Probabilistic Model Checking

• PMC is the gold standard for tractable CTMC transient reachability, but its explicit-state requirement can exceed computational limits for infinite or intractably large CTSVAS models.The paper names Storm, PRISM, and Modest as cutting-edge PMC tools.Source: §3.1 · p. 5

3.2 Approximate Solutions

• Importance sampling and splitting, weighted simulation, and related rare-event methods provide approximate transient reachability results, whereas Ragtimer provides a guaranteed lower bound with minimal manual intervention.Importance sampling biases simulation toward rare events, while importance splitting uses levels ordered by reachability probability.Source: §3.2 · pp. 5–6

3.3 Abstraction Techniques

• Sliding-window abstractions focus computation on high-probability states and may discard low-probability transitions leading to rare events, making them poorly suited to these models.The paper says this limitation is empirically demonstrated by FAU benchmarking.Source: §3.3 · p. 6

3.4 Partial State Space Construction

• Partial-state-space tools can analyze models beyond exact PMC limits, and the Ragtimer 0.1 prototype with Cycle & Commute expanded trace-generated spaces through parallel traces and cycle exploration.Stamina instead produces upper and lower bounds by assigning unexplored transitions target probabilities of 1 or 0, respectively.Source: §3.4 · p. 6

4 Trace Generation and State Space Expansion

• Ragtimer generates traces, adds their states and transitions, expands the state space through commuting transitions and cycles, and exports it for PRISM.The workflow combines trace-based construction with deterministic parallel-trace and cycle expansion.Source: §4 · pp. 6–7

4.1 Dependency Analysis

• The dependency graph captures essential transition firings and guides trace generation, but naive shortest traces may exclude higher-probability interleavings.It is a directed acyclic graph of transition execution counts and enabling conditions; Ragtimer uses it as a heuristic.Source: §4.1 · pp. 8–9

4.2 Reinforcement Learning for Trace Generation

• Reinforcement learning weights enabled transitions, initially favoring dependency-graph transitions, then adjusts weights according to each trace’s probability relative to a rolling average.Weight changes scale with the number of times a transition fires in the trace.Source: §4.2 · p. 9

4.3 Random Dependency Graph for Trace Generation

• Random dependency-graph firing generates traces in Rust, avoiding Ragtimer 0.1’s IVy-to-C++ compilation and reducing duplicate traces.The approach is described as quickly and uniformly sampling a state space and improving accessibility through faster execution and less reliance on third-party tools.Source: §4.3 · p. 10

4.4 Cycle & Commute

• Cycle & Commute adds parallel traces when transitions remain enabled along a trace and adds bounded cycles to recapture probability otherwise directed to absorbing states.Cycle length and commuting depth are explicitly bounded because CRN state spaces may be infinite.Source: §4.4 · p. 10

5.1 CTSVAS Input Language

• The input format represents generic CTSVAS models and CRNs using notation designed to resemble typical CRN descriptions.The example specification describes two transitions over three variables and a probability query about increasing S3 from 300 to 400.Source: §5.1 · p. 11

5.2 Probabilistic Analysis

• Ragtimer exports its partial state space in PRISM explicit model format for checking with mainstream PMC tools such as PRISM and Storm.Source: §5.2 · p. 12

5.3 Efficiency Improvements over Ragtimer 0.1

• Custom prefix trees store explicit states and traces, supporting fast duplicate checks while improving memory efficiency and maintaining time complexity.The paper describes prefix-tree representation of explicit states and traces as novel to its knowledge.Source: §5.3 · p. 12

5.4 The Stamina Toolset

• Ragtimer 1.0 is included in the preliminary release of the cross-platform, open-source Stamina Toolset, designed to be modular, efficient, and accessible to non-technical users.The toolset is planned to feature a graphical interface.Source: §5.4 · p. 12

6.1 Rare-Event CRN Models

• The four realistic CRN benchmarks have large or infinite state spaces and rare-event targets; their unbounded species counts avoid potentially excluding rare events through tight manual bounds.The set includes MYP, EFC, SMR, and SSPD, with targets involving both species decreases and increases.Source: §6.1 · p. 13

6.2 Experiment Setup

• Experiments used one CPU per test on an AMD Ryzen Threadripper 12-Core 3.5 GHz processor with 132 GB RAM, running Ubuntu 22.04 LTS.Unless otherwise stated, models were unbounded.Source: §6.2 · p. 13

6.3 Results

• Adding cycles and parallel traces moves the lower bound toward the true probability; equal parameter values are a reasonable starting point, and RL typically yields higher results than RDG.For this benchmark set, parameter pair (5, 5) was sufficient to reach a plateau and approach the true probability; models benefited from different parameter changes.Source: §6.3 · pp. 14–15, Figure 4 · p. 14

6.4 Comparison to Existing Tools

• 1.67E-06 from 100 RL traces exceeded wSSA’s 1.24E-06 and WE’s 1.48E-6, and fell within Stamina’s reported [1.43E-06, 1.49E-05] range.The state space used 40 MB; Stamina took four hours to compute its range.Source: §6.4 · p. 15
• 1.72E-07 nearly matched EFC’s true 1.74E-07 in 3 ms; SMR reached 2.21E-07 versus wSSA’s 2.16E-07; SSPD matched wSSA at 2.95E-07 in 1 second.EFC benefited most from cycles, while SMR used RL trace generation plus Cycle & Commute.Source: §6.4 · p. 15
• Across four models, Ragtimer 1.0 offers the best balance of probability, runtime, and memory, though it does not lead every metric.It is competitive on less complex models and especially attractive on MYP and SMR when time and memory are limited.Source: §6.4 · p. 16, Table 1 · p. 17
• Storm timed out on MYP and exceeded the memory limit on SMR, while Ragtimer 1.0 computed highly accurate probabilities within limits on all four models.Ragtimer also produced significantly tighter lower bounds than Stamina on EFC and SSPD.Source: §6.4 · p. 16
• Within comparable runtimes and memory usage, Ragtimer 1.0 improved each probability result by several orders of magnitude over Ragtimer 0.1.The prototype’s traces were quick to generate but often had negligibly low cumulative probability.Source: §6.4 · p. 17

7 Conclusion

• Ragtimer 1.0 constructs streamlined partial state spaces that exploit concurrency and cycles to compute guaranteed lower bounds for properties of interest.Source: §7 · p. 18
• Evaluation on real-world CRN models found that Ragtimer 1.0 outperforms its prototype, competes with cutting-edge tools, and refutes rare-event simulation estimates.Source: §7 · p. 18
• As the first Stamina Toolset tool, Ragtimer enhances formal techniques' practicality and accessibility for industry professionals, particularly in synthetic biology.Source: §7 · pp. 18–19
• Future work includes broader custom rate-function support and proofs of correctness within Ragtimer's codebase.Source: §7 · p. 19

A.1 Modified Yeast Polarization

• The Modified Yeast Polarization model has eight reactions acting on species [R, L, RL, G, Ga, Gbg, Gd], with initial state [50, 2, 0, 50, 0, 0, 0].Source: §A.1 · p. 22
• The model represents a pheromone-induced G-protein cycle with a constant ligand population that keeps it away from equilibrium.Source: §A.1 · p. 22
• The rare-event query asks for the probability that Gbg rises from 0 to 50 molecules within 20 seconds.Source: §A.1 · p. 22

A.2 Enzymatic Futile Cycle

• The model has six reactions acting on six species, with initial state [1, 50, 0, 1, 50, 0].Source: §A.2 · p. 22
• The rare-event query asks for the probability that S5 decreases from 50 to 25 within 100 seconds.Source: §A.2 · p. 22
• The model is described as concurrent and cyclical, and reaction R1 is listed as S1 + S2.Source: §A.2 · p. 22

A.3 Simplified Motility Regulation

• The model represents the genetic mechanism regulating flagella formation in Bacillus subtilis and has nine species and twelve reactions.Source: §A.3 · p. 22
• Its initial state for [codY, flache, SigD_hag, CodY, CodY_flache, hag, CodY_hag, SigD, Hag] is [1, 1, 1, 10, 1, 1, 1, 10, 10].Source: §A.3 · p. 22
• The rare-event query asks for the probability that CodY increases from 10 to 20 within 10 seconds.Source: §A.3 · pp. 22–23
• The listed reactions include R7: SigD + hag, R9: CodY + flache, and R11: CodY + hag.Source: §A.3 · p. 23

• The CSL target queries whether S2 increases from 40 to 80 within 100 seconds from initial state [1, 40].The model describes a production-degradation interaction between two species.Source: §A.4 · p. 23

Appendix B Full Result Tables

• Tables 2–5 provide full results for MYP, EFC, SMR, and Single Species Production-Degradation, reporting approach, traces, cycle and commute limits, probability, time, and bytes.Approach distinguishes reinforcement-learning from random dependency-graph firing; probability is a lower bound, while time and bytes measure construction cost.Source: Appendix B · p. 24, Table 2 · p. 25, Table 3 · p. 26

Appendix C CRN & CTSVAS Input Format

• Ragtimer uses a custom input format intended to make CTSVAS specifications straightforward without requiring in-depth knowledge of CTMC modeling.Source: Appendix C · p. 29

C.1 Overview

• The overview describes a minimal, plain-English keyword format in which each line specifies a model property; its example includes variables, a target, transitions, updates, and rates.Source: §C.1 · p. 29

C.2 Syntax & Semantics

• Variables are ordered by declaration and initialized there; transition lines define updates and enabling bounds, rates may be constants or formulas, and exactly one target is specified.Source: Variables and Initial States · p. 30, Transitions · pp. 30–31, Property Specification · p. 31

C.3 Example: MYP Model

• The appendix provides an encoding of the Modified Yeast Polarization model in the custom input format.Source: §C.3 · p. 31