Automatic verification of real-time systems with discrete probability distributions

We consider the timed automata model of [3], which allows the analysis of realtime 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 [6] 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.

• Type: Journal
• Year: 2002
• Where: TCS
• Authors: Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston
• Keywords: Model, Quantitative Timing Constraints, TCS 2002, Theoretical Computer Science, Timed Automata Model