www.prismmodelchecker.org
[KNSS02] M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, 282, pages 101-150. June 2002. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (225 KB)  pdf pdf (474 KB)  bib bib
Links: [Google] [Google Scholar]
Abstract. We consider the timed automata model of Alur and Dill, which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, two approaches to model checking are introduced for this model. The first uses the algorithm of Baier and Kwiatkowska to provide a verification technique against temporal logic formulae which can refer both to timing properties and probabilities. The second, generally more efficient, technique concerns the verification of probabilistic, real-time reachability properties

Publications