Skip to main content
STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis
Lecture Notes in Computer Science
  • Thakur Neupane, Utah State University
  • Chris J. Myers, University of Utah
  • Curtis Madsen, Boston University
  • Hao Zheng, University of South Florida
  • Zhen Zhang, Utah State University
Document Type
Conference Paper
New York City, New York
Publication Date
Creative Commons License
Creative Commons Attribution 4.0

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.

Citation Information
Neupane T., Myers C.J., Madsen C., Zheng H., Zhang Z. (2019) STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis. In: Dillig I., Tasiran S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11561. Springer, Cham