Oxford logo
[KNSS99] M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-Time Systems with Discrete Probability Distributions. In J.-P. Katoen (editor), Proc. 5th International AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), volume 1601 of LNCS, pages 75--95, Springer. March 1999. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (120 KB)  pdf pdf (308 KB)  bib bib
Notes: The original publication is available at link.springer.com.
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, we may wish 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, using the algorithm of Baier and Kwiatkowska with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, ``with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2''.