[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]
|
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''.
|