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

Automatic Verification of Real-time Systems with Discrete Probability Distributions

SPROSTON, Jeremy James
1999-01-01

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''.
1999
1601
75
95
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/114807
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact