In this section, we consider a number of automatic verification methods for probabilistic timed automata. The underlying semantics of a probabilistic timed automaton is generally presented with respect to the time domain of the real numbers, and hence the resulting semantic timed Markov decision process generally has an uncountable number of states and transitions. Therefore, the methods that we present are based on the construction of finite-state Markov decision processes, which are defined so that their analysis can be used to infer reachability probabilities and other performance measures of probabilistic timed automata. We present a different finite-state construction in each of the following four sections.

Verification of Real-time Probabilistic Systems

SPROSTON, Jeremy James
2008-01-01

Abstract

In this section, we consider a number of automatic verification methods for probabilistic timed automata. The underlying semantics of a probabilistic timed automaton is generally presented with respect to the time domain of the real numbers, and hence the resulting semantic timed Markov decision process generally has an uncountable number of states and transitions. Therefore, the methods that we present are based on the construction of finite-state Markov decision processes, which are defined so that their analysis can be used to infer reachability probabilities and other performance measures of probabilistic timed automata. We present a different finite-state construction in each of the following four sections.
2008
Modeling and Verification of Real-time Systems
ISTE - John Wiley & Sons
257
297
9781848210134
M. KWIATKOWSKA; G. NORMAN; D. PARKER; 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/133218
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact