zbMATH — the first resource for mathematics

Faster and symbolic CTMC model checking. (English) Zbl 1007.68517
De Alfaro, Luca (ed.) et al., Process algebra and probabilistic methods. Performance modelling and verification. Joint international workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2165, 23-38 (2001).
Summary: This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of $$\mathcal{ O}(N)$$ in the time complexity of checking time-bounded until-formulas, where $$N$$ is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.
For the entire collection see [Zbl 0971.00028].

MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68Q60 Specification and verification (program logics, model checking, etc.)
CUDD
Full Text: