Model Checking Stochastic Automata for Dependability and Performance Measures

Model checking of Continuous Time Markov Chains (CTMCs) is a widely used approach in performance and dependability analysis and proves for which states of a CTMC a logical formula holds. This viewpoint might be too detailed in several practical situations, especially if the states of the CTMC do not correspond to physical states of the system since they are introduced for example to model non-exponential timing. The paper presents a general class of automata with stochastic timing realized by clocks. A state of an automaton is given by a logical state and by clock states. Clocks trigger transitions and are modeled by phase type distributions or more general state based stochastic processes. The class of stochastic processes underlying these automata contains CTMCs but also goes beyond Markov processes. The logic CSL is extended for model checking automata with clocks. A formula is then proved for an automata state and for the clock states that depend on the past behavior of the automaton. Basic algorithms to prove CSL formulas for logical automata states with complete or partial knowledge of the clock states are introduced. In some cases formulas can be proved efficiently by decomposing the model with respect to concurrently running clocks which is a way to avoid state space explosion.