CSRL Model Checking with Closed-Form Bounding Distributions

Continuous Stochastic Logic (CSL) which lets to express real time probabilistic properties on Continuous Time Markov Chains (CTMC) has been augmented by reward structures to check also performability measures. Thus Continuous Stochastic Reward Logic (CSRL) defined on Markov Reward Models (MRM) provides a framework to verify performance-related and as well as dependability-related measures. Probabilistic model checking can be provided through bounding transient, steady-state distributions of the underlying Markov chain, since models are checked to see if the considered measures are guaranteed or not. We propose to extend the model checking algorithm that we have proposed for CSL to the CSRL operators. This method is based on the construction of bounding models having closed-form transient and steady-state distributions by means of Stochastic Comparison technique. In the case when the model can be checked by this method we gain significantly in time and memory complexity. However in case when we can not conclude if the considered formula is satisfied or not, we may apply classical model checking algorithms.