# STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

## TL;DR

STAMINA is a new stochastic model checker that efficiently analyzes infinite-state continuous-time Markov chains by approximating large models to finite ones, enhancing scalability and accuracy.

## Contribution

It introduces a novel state space approximation and property-guided expansion, improving scalability and precision in infinite-state stochastic model checking.

## Key findings

- Demonstrates improved analysis efficiency over existing tools.
- Shows promising accuracy in benchmark tests.
- Effectively handles large and infinite state models.

## Abstract

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.