Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
For researchers and practitioners in dependable systems, this work addresses the lack of scalable model checking techniques for general stochastic automata, which are important for modeling faults and repairs.
The paper presents the first general and effective model checking approach for stochastic automata (SA) that works for nontrivial examples, providing upper/lower bounds on reachability probabilities. The approach combines interval abstraction with big time steps semantics and is implemented in a prototype tool.
Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularly useful to faithfully model and analyse dependable systems involving faults, maintenance, and repairs. Effective SA analysis approaches have so far been limited to statistical model checking and thus deterministic SA, while previously proposed model-checking techniques apply to limited subclasses of SA only, or do not scale. In this paper, we present the first dedicated SA model checking approach that is general and effective: It puts few restrictions on the input SA, and we show in our experimental evaluation that it works well for nontrivial examples. It combines a refinable interval abstraction of the continuous distributions with a direct application of the "big time steps" semantics of SA, providing upper/lower bounds on maximum/minimum reachability probabilities. We extend the Modest and Jani modelling formalisms with support for SA, and provide a prototype implementation of our approach in Rust.