We consider the timed automata model of Alur and Dill (Theoret. Comput. Sci. 126 (1994) 183–235), 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 (Distributed Comput. 11 (1998) 125–155) 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.

Automatic Verification of Real-time Systems with Discrete Probability Distributions

SPROSTON, Jeremy James
2002-01-01

Abstract

We consider the timed automata model of Alur and Dill (Theoret. Comput. Sci. 126 (1994) 183–235), 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 (Distributed Comput. 11 (1998) 125–155) 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.
2002
282
101
150
M. KWIATKOWSKA; G. NORMAN; R. SEGALA; J. SPROSTON
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/125250
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 246
  • ???jsp.display-item.citation.isi??? 167
social impact