More Like this

1. STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker

   https://doi.org/10.1007/978-3-031-43835-6_7  

   Jeppson, Josh; Volk, Matthias; Israelsen, Bryant; Roberts, Riley; Williams, Andrew; Buecherl, Lukas; Myers, Chris J; Zheng, Hao; Winstead, Chris; Zhang, Zhen (September 2023, Lecture notes in computer science)

   Jansen, N; Tribastone, M (Ed.)

   Improving the scalability of probabilistic model checking (PMC) tools is crucial to the verification of real-world system designs. The STAMINA infinite-state PMC tool achieves scalability by iteratively constructing a partial state space for an unbounded continuous-time Markov chain model, where a majority of the probability mass resides. It then performs time-bounded transient PMC. It can efficiently produce an accurate probability bound to the property under verification. We present a new software architecture design and the C++ implementation of the STAMINA 2.0 algorithm, integrated with the STORM model checker. This open-source STAMINA implementation offers a high degree of modularity and provides significant optimizations to the STAMINA 2.0 algorithm. Performance improvements are demonstrated on multiple challenging benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, over the previous STAMINA implementation. Additionally, its design allows for future customizations and optimizations to the STAMINA algorithm. 

   more » « less
2. STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis

   https://doi.org/https://doi.org/10.1007/978-3-030-25540-4_31  

   Neupane, Thakur; Myers, Chris; Madsen, Curtis; Zheng, Hao; Zhang, Zhen (January 2019, Lecture notes in computer science)

   Stochastic model checking is a technique for analyzing systems that possess probabilistic characteristics. However, its scalability is limited as probabilistic models of real-world applications typically have very large or infinite state space. This paper presents a new infinite state CTMC model checker, STAMINA, with improved scalability. It uses a novel state space approximation method to reduce large and possibly infinite state CTMC models to finite state representations that are amenable to existing stochastic model checkers. It is integrated with a new property-guided state expansion approach that improves the analysis accuracy. Demonstration of the tool on several benchmark examples shows promising results in terms of analysis efficiency and accuracy compared with a state-of-the-art CTMC model checker that deploys a similar approximation method. 

   more » « less
3. Stochastic Hazard Analysis of Genetic Circuits in iBioSim and STAMINA

   https://doi.org/10.1021/acssynbio.1c00159  

   Buecherl, Lukas; Roberts, Riley; Fontanarrosa, Pedro; Thomas, Payton J.; Mante, Jeanet; Zhang, Zhen; Myers, Chris J. (October 2021, ACS synthetic biology)

   In synthetic biology, combinational circuits are used to program cells for various new applications like biosensors, drug delivery systems, and biofuels. Similar to asynchronous electronic circuits, some combinational genetic circuits may show unwanted switching variations (glitches) caused by multiple input changes. Depending on the biological circuit, glitches can cause irreversible effects and jeopardize the circuit’s functionality. This paper presents a stochastic analysis to predict glitch propensities for three implementations of a genetic circuit with known glitching behavior. The analysis uses STochastic Approximate Model-checker for INfinite-state Analysis (STAMINA), a tool for stochastic verification. The STAMINA results were validated by comparison to stochastic simulation in iBioSim resulting in further improvements of STAMINA. This paper demonstrates that stochastic verification can be utilized by genetic designers to evaluate design choices and input restrictions to achieve a desired reliability of operation. 

   more » « less
4. Ragtimer 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS

   Taylor, Landon; Jeppson, Joshua; Hu, Bingqing; Buecherl, Lukas; Zhang, Zhen (December 2026, 24th International Symposium on Automated Technology for Verification and Analysis (ATVA))

   Bu, Lei; Kaminski, Benjamin Lucien (Ed.)

   Transient reachability analysis of rare events in Continuous- Time Stochastic Vector Addition Systems (CTSVAS) such as Chemical Reaction Networks (CRNs) has proven a formidable challenge to cutting- edge tools. Underlying a CTSVAS is a continuous-time Markov chain (CTMC), and CTMC transient reachability analysis calls for Probabilis- tic Model Checking (PMC). This analysis requires the explicit represen- tation of a model’s entire state space. Rare events occur with extremely low probability, compounding the challenge of probabilistic analysis. In CRNs, it is imperative to verify the probability of rare events; even a low concentration of a species can have pathological consequences. This paper presents the Ragtimer 1.0 tool, which efficiently builds a partial state space for a CTSVAS by enumerating traces to a rare event of in- terest and expanding them to exploit concurrency and cycles, providing a guaranteed lower bound on the probability of a rare event. Guaranteed lower bounds are particularly useful in synthetic biological applications because they indicate how and when a rare event can be experimen- tally observed. Ragtimer is an attractive alternative to existing rare event analysis methods for rare events in CTSVAS models. It outper- formsexistingPMCtoolsandrefutesmultipleprobabilityestimatesfrom rare-event stochastic simulation on multiple challenging CRN models. Ragtimer uses optimized data structures, a simple input format, and memory-safe Rust code to improve the scalability and accessibility of PMC for industry professionals. 

   more » « less
5. MFBO-SSM: Multi-Fidelity Bayesian Optimization for Fast Inference in State-Space Models

   Imani, M; Ghoreishi, S.F.; Allaire, D.; Braga-Neto, U (July 2019, Proceedings of the ... AAAI Conference on Artificial Intelligence)

   Nonlinear state-space models are ubiquitous in modeling real-world dynamical systems. Sequential Monte Carlo (SMC) techniques, also known as particle methods, are a well-known class of parameter estimation methods for this general class of state-space models. Existing SMC-based techniques rely on excessive sampling of the parameter space, which makes their computation intractable for large systems or tall data sets. Bayesian optimization techniques have been used for fast inference in state-space models with intractable likelihoods. These techniques aim to find the maximum of the likelihood function by sequential sampling of the parameter space through a single SMC approximator. Various SMC approximators with different fidelities and computational costs are often available for sample- based likelihood approximation. In this paper, we propose a multi-fidelity Bayesian optimization algorithm for the inference of general nonlinear state-space models (MFBO-SSM), which enables simultaneous sequential selection of parameters and approximators. The accuracy and speed of the algorithm are demonstrated by numerical experiments using synthetic gene expression data from a gene regulatory network model and real data from the VIX stock price index. 

   more » « less