Automatic Verification of Real-Time Systems With Discrete Probability Distributions
Author: M. Kwiatkowska, G. Normann, R. Segala, J. Sproston
Appears: in Theoretical Computer Science, vol. 282, pages 101--150, 2002.
Also: An extended abstract appears in Proceedings of the 5th International AMAST Workshop on Real Time and Probabilistic Systems, LNCS 1601, pages 79-95, May 1999.
Abstract: We consider the timed automata model of [AD94], 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 [BKm96] 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.
Download the full paper from the publisher.
Download the extended abstract from the publisher.