More Like this

1. STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking

   https://doi.org/https://doi.org/10.1007/978-3-030-94583-1_16  

   Roberts, R.; Neupane, T.; Buecherl, L.; Myers, C.J.; Zhang, Z. (June 2022, Lecture notes in computer science)

   Finkbeiner, B.; Wies, T. (Ed.)

   Stochastic model checking (SMC) is a formal verification technique for the analysis of systems with probabilistic behavior. Scalability has been a major limiting factor for SMC tools to analyze real-world systems with large or infinite state spaces. The infinite-state Continuous-time Markov Chain (CTMC) model checker, STAMINA, tackles this problem by selectively exploring only a portion of a model’s state space, where a majority of the probability mass resides, to efficiently give an accurate probability bound to properties under verification. In this paper, we present two major improvements to STAMINA, namely, a method of calculating and distributing estimated state reachability probabilities that improves state space truncation efficiency and combination of the previous two CTMC analyses into one for generating the probability bound. Demonstration of the improvements on several benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, yield significant savings in both run-time and state space size (and hence memory), compared to both the previous version of STAMINA and the infinite-state CTMC model checker INFAMY. The improved STAMINA demonstrates significant scalability to allow for the verification of complex real-world infinite-state systems. 

   more » « less
2. 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
3. On the surprising effectiveness of a simple matrix exponential derivative approximation, with application to global SARS-CoV-2

   https://doi.org/10.1073/pnas.2318989121  

   Didier, Gustavo; Glatt-Holtz, Nathan E.; Holbrook, Andrew J.; Magee, Andrew F.; Suchard, Marc A. (January 2024, Proceedings of the National Academy of Sciences)

   The continuous-time Markov chain (CTMC) is the mathematical workhorse of evolutionary biology. Learning CTMC model parameters using modern, gradient-based methods requires the derivative of the matrix exponential evaluated at the CTMC’s infinitesimal generator (rate) matrix. Motivated by the derivative’s extreme computational complexity as a function of state space cardinality, recent work demonstrates the surprising effectiveness of a naive, first-order approximation for a host of problems in computational biology. In response to this empirical success, we obtain rigorous deterministic and probabilistic bounds for the error accrued by the naive approximation and establish a “blessing of dimensionality” result that is universal for a large class of rate matrices with random entries. Finally, we apply the first-order approximation within surrogate-trajectory Hamiltonian Monte Carlo for the analysis of the early spread of Severe acute respiratory syndrome coronavirus 2 (SARS-CoV-2) across 44 geographic regions that comprise a state space of unprecedented dimensionality for unstructured (flexible) CTMC models within evolutionary biology. 

   more » « less
4. Infinity Learning: Learning Markov Chains from Aggregate Steady-State Observations

   https://doi.org/10.1609/aaai.v34i04.5806  

   Gao, Jianfei; Zahran, Mohamed A.; Sheoran, Amit; Fahmy, Sonia; Ribeiro, Bruno (June 2020, Proceedings of the AAAI Conference on Artificial Intelligence)

   We consider the task of learning a parametric Continuous Time Markov Chain (CTMC) sequence model without examples of sequences, where the training data consists entirely of aggregate steady-state statistics. Making the problem harder, we assume that the states we wish to predict are unobserved in the training data. Specifically, given a parametric model over the transition rates of a CTMC and some known transition rates, we wish to extrapolate its steady state distribution to states that are unobserved. A technical roadblock to learn a CTMC from its steady state has been that the chain rule to compute gradients will not work over the arbitrarily long sequences necessary to reach steady state —from where the aggregate statistics are sampled. To overcome this optimization challenge, we propose ∞-SGD, a principled stochastic gradient descent method that uses randomly-stopped estimators to avoid infinite sums required by the steady state computation, while learning even when only a subset of the CTMC states can be observed. We apply ∞-SGD to a real-world testbed and synthetic experiments showcasing its accuracy, ability to extrapolate the steady state distribution to unobserved states under unobserved conditions (heavy loads, when training under light loads), and succeeding in difficult scenarios where even a tailor-made extension of existing methods fails. 

   more » « less
5. A simple but powerful simulated certainty equivalent approximation method for dynamic stochastic problems

   Cai, Yongyang; Judd, Kenneth (January 2023, Quantitative economics)

   We introduce a novel simulated certainty equivalent approximation (SCEQ) method for solving dynamic stochastic problems. Our examples show that SCEQ can quickly solve high-dimensional finite- or infinite-horizon, stationary or nonstationary dynamic stochastic problems with hundreds of state variables, a wide state space, and occasionally binding constraints. With the SCEQ method, a desktop computer will suffice for large problems, but it can also use parallel tools efficiently. The SCEQ method is simple, stable, and can utilize any solver, making it suitable for solving complex economic problems that cannot be solved by other algorithms. 

   more » « less