Tackling Scalability for Transient Reachability Analysis of Chemical Reaction Networks (Poster)

Appears in FMCAD 2025 Student Forum
Landon Taylor, Zhen Zhang

Abstract. Probabilistic notions of correctness are absolutely essential for stochastic systems operating in safety- and mission-critical settings. Among these noisy, stochastic systems are Chemical Reaction Networks (CRNs), which model the interactions within biochemical systems. A CRN induces a Continuous-Time Markov Chain (CTMC), in which a model's state changes based on a transition rate function. Probabilistic Model Checking (PMC) is a crucial tool for making guarantees for CTMCs. However, these systems often involve rare events that can lead to critical failures. Currently, PMC faces state explosion in models with rare events, making quantitative analysis computationally prohibitive. Our work addresses this challenge by focusing on three key objectives: (1) scaling CTMC transient reachability analysis through innovative pre-processing techniques that reduce the explicit state space; (2) extending symbolic verification methods to CTMCs to provide regional probability estimates without the need for exhaustive state enumeration; and (3) developing a provably-correct probabilistic verification tool in Rust. Preliminary results in these objectives show the viability of our approach.

  Description

Stochastic Modeling and Experimental Validation of Cannabinoid Biosynthesis in Saccharomyces cerevisae

Appears in IBE 2025
Bingqing Hu, Ammar Mussaji, Joshua Jeppson, Landon Taylor, Jixun Zhan, Zhen Zhang

Abstract. Cannabinoid biosynthesis in engineered microbial systems is frequently constrained by uncertainties in enzyme behavior and competing metabolic pathways. Experimental methods alone can struggle to fully understand and optimize these complex biosynthetic routes. To address this, we built computational models of the cannabigerolic acid (CBGA) biosynthetic pathway using Continuous-Time Markov Chains (CTMC). Our models included experimentally measured Michaelis-Menten kinetic parameters and enzyme reaction data. By combining modeling with experimental results in our stochastic analysis, we identified key steps that limit CBGA production in Saccharomyces cerevisae. For example, our simulations showed that adjusting branching ratios—especially in the two-step conversion of hexanoyl-CoA to olivetolic acid—can significantly improve yields. Moreover, the stochastic (probabilistic) nature of our model allowed us to study variability and transient enzyme behavior that are difficult to capture experimentally, providing insights into the probabilistic distribution of fluxes through alternative branches within the CBGA biosynthesis pathway. Our model's predictions matched experimentally measured CBGA concentrations, demonstrating their accuracy. Overall, this approach underscores the power of combining computational modeling with experimental validation, utilizing stochastic analysis to robustly explore and optimize complex cannabinoid biosynthesis pathways.

Degradation-Driven Failure Minimization in Genetic Circuits Through Model Checking

Appears in IWBDA 2025
Landon Taylor, Lukas Buecherl, Zhen Zhang

Abstract. The genetic toggle switch is a foundational motif in synthetic biology, enabling bistable behavior in which a cell can maintain one of two distinct stable states in response to transient inputs. In a common implementation, the toggle switch is composed of two transcriptional units: one in which TetR represses LacI expression, and another in which LacI represses the expression of TetR and YFP. The states are toggled by aTc and IPTG, which bind TetR and LacI, respectively, effectively removing the repressors. Once the toggle switch reaches a given state, its long-term stability depends on various system parameters, including protein production and degradation rates, which govern the dynamics of state maintenance and transitions. In this work, we focus on how the degradation rates of the toggle switch proteins, namely LacI, TetR, and YFP, influence the probability of unintended state reversal after the system reaches a steady state. Degradation is a particularly attractive design parameter because it can be modulated through engineered degradation tags, offering a practical route for tuning circuit performance.

  Slides

Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces (Preprint)

Appears in preprint at arXiv
Joshua Jeppson, Landon Taylor, Bingqing Hu, Zhen Zhang

Abstract. 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 effects. Their low probabilities and potentially extremely large state spaces challenge existing probabilistic model checking and stochastic rare-event simulation techniques. In particular, in Chemical Reaction Networks (CRNs), a chemical kinetic language often represented as VAS, rare event effects may be pathological. We present two novel heuristics for priority-first partial state space expansion and trace generation tuned to the transient analysis of rare-event probability in VAS: Iterative Subspace Reduction (ISR) and Single Distance Priority (SDP). Both methods construct a closed vector space containing all solution states. SDP then simply prioritizes shorter distances to this ``solution space'', while ISR constructs a set of nested subspaces, where short and highly-probable satisfying traces are likely to pass through in sequence. The resulting partial state graph from each method contains likely traces to rare-event states, allowing efficient probabilistic model checking to compute a lower-bound probability of a rare event of interest. These methods are deterministic, fast, and demonstrate marked performance on challenging CRN models.

 DOI   arXiv

Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report

Appears in TOOLympics
Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. KÖhl, Bettina KÖnighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang

Abstract. 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 support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification.

 DOI   Open-Access Paper   Springer

Enhancing Property-Directed Reachability for Chemical Reaction Networks (Poster)

Appears in FMCAD 2023 Student Forum
Landon Taylor, Zhen Zhang

Abstract. Property-Directed Reachability (PDR) is a scalable method for inductively checking reachability of system models. PDR is specialized for Boolean and integer systems, but it is currently unable to provide probability information for continuous-time systems like Chemical Reaction Networks (CRNs). This research advances PDR to bound variables in infinite-state CRNs and to estimate a target state's reachability probability.

  Poster   Description

Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks

Appears in FMCAD 2023
Landon Taylor, Bryant Israelsen, Zhen Zhang

Abstract. In synthetic biological systems, rare events can cause undesirable behavior leading to pathological effects. Due to their low observability, rare events are challenging to analyze using existing stochastic simulation methods. Chemical Reaction Networks (CRNs) are a general-purpose formal language for modeling chemical kinetics. This paper presents a fully automated approach to efficiently construct a large number of concurrent traces by expanding a sample of known traces. These traces constitute a partial state space containing only traces leading to a rare event of interest. This state space is then used to compute a lower bound for the rare event’s probability. We propose a novel approach for the analysis of highly concurrent CRNs, including a CRN reaction independence analysis and an algorithm that exploits CRN concurrency to rapidly enumerate parallel traces. We then present a novel algorithm to add cycles to a partial state space to further increase the rare event’s probability lower bound to its actual value. The resulting prototype tool, RAGTIMER, demonstrates improvement over stochastic simulation and probabilistic model checking.

 DOI   IEEE   reposiTUm   NSF Public Access

Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks

Appears in SPIN 2023
Bryant Israelsen, Landon Taylor, Zhen Zhang

Abstract. Rare events are known to potentially cause pathological behavior in biochemical reaction systems. It is important to understand the cause. However, rare events are challenging to analyze due to their extremely low observability. This paper presents a fully automated approach that rapidly generates a large number of execution traces guaranteed to reach user-specified rare-event states for Chemical Reaction Network (CRN) models. It is enabled by a unique combination of a multi-layered and service-oriented CRN formal modeling approach, a dependency graph method to aid the shortest rare-event trace generation, and randomized compositional testing. The resulting prototype tool shows marked improvement over stochastic simulation and probabilistic model checking and it offers insights into a CRN.

 DOI   Springer   NSF Public Access

Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms

Appears in VMCAI 2022
Landon Taylor, Zhen Zhang

Abstract. As an efficient interconnection network, Network-on-Chip (NoC) provides significant flexibility for increasingly prevalent many-core systems. It is desirable to deploy fault-tolerance in a dependable safety-critical NoC design. However, this process can easily introduce deeply buried flaws that traditional simulation-based NoC design approaches may miss. This paper presents a case study on applying scalable formal verification that detects, corrects, and proves livelock in a dependable fault-tolerant NoC using the IVy verification tool. We formally verify correctness at the routing algorithm level. We first present livelock verification using refutation-based simulation scaled to a 15-by-15 two-dimensional NoC. We then present a novel zone-based approach to livelock verification in which finite coordinate-based routing conditions are abstracted as positional zones relative to a packet’s destination. This abstraction allows us to detect and remove livelock patterns on an arbitrarily large network. The resultant improved routing algorithm is free of livelock and maintains a high level of fault tolerance.

 DOI   Springer   ResearchGate   Talk Recording