STAMINA is designed to work with large or infinite state space models and truncate them so that the probability of a CSL path property holding given an initial state is bounded within a window. It is developed within Dr. Zhen Zhang's research group at Utah State University and maintained by the following people:

Current Maintainer:

Josh Jeppson, B.Sc.
PhD Student - Utah State University
Email: [Click To See Email]

Past Maintainers and Code Contributors:

• Riley Roberts*
• Andrew Williams
• Bret Jepsen
• Thakur Neupane**
• Lukas Buecherl^†
• Andrew Gerber

Introduction to STAMINA

STAMINA is an infinite state-space model truncation tool compatible with both PRISM and STORM. STAMINA is a tool within the FLUENT toolchain. It deploys a state truncation-based approach, estimating path probabilities of reaching each state on-the-fly and terminates exploration of a path when the cumulative estimated probability along such a path drops below a predefined threshold. Each terminated path is routed to an absorbing state, in order to estimate the error probability in subsequent CTMC analysis.

After all paths have been explored or truncated, transient Markov chain analysis is applied to determine the probability of a transient property of interest specified using Continuous Stochastic Logic (CSL). The calculated probability forms a lower bound on the probability, while the upper bound also includes the probability of the absorbing state. The actual probability of the CSL property is guaranteed to be within this range. If the probability bound is still too large compared to a user-provided probability precision value (default is 10^-3), the PRISM version of STAMINA employs a property property-guided refinement technique to expand the state space to tighten the reported probability range incrementally.

Frequently Asked Questions

What model checking engines does STAMINA support?

STAMINA supports the STORM and PRISM model checking engines, and it supports models written in the PRISM language. Future work includes making STAMINA compatible with JANI and other model formats.

What types of models does STAMINA support?

Currently, STAMINA/PRISM supports only CTMCs, whereas STAMINA/STORM supports both CTMCs, and has alpha support for DTMCs through the STORM API.

Why would we want to check an infinite (or very large) model?

STAMINA was developed primarily to check models representative of chemical reaction networks in synthetic biology. Because each combination of molecules is a state, even a bounded reaction network could have an infinite or extremely large number of states, making the resulting model non-trivial for a traditional model checker such as STORM or PRISM. In order to actually extract useful information from these models, and to test them against CSL properties, STAMINA was developed.

The STAMINA Algorithm(s)

STAMINA makes use of multiple variations on a smart breadth-first search algorithm to estimate reachability probability on-the-fly. It does not explore paths whose reachability is below a certain user-defined threshold, κ, which automatically decrements until the probability window is within a certain bound. Currently there are several variations on the STAMINA algorithm. To learn more about the STAMINA algorithms, please visit the wiki page.