Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation π_0 of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint K_0 on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the “inverse method”. The method presents the following advantages. First, since K_0 corresponds to a dense domain around π_0 on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to obtain a valuation satisfying K_0 which is as small as possible while preserving reachability probabilities, thus making the probabilistic analysis of the system easier and faster in practice. We provide examples of the application of our technique to models of randomized protocols, and introduce an extension of the method allowing the generation of a “probabilistic cartography” of a system.

An Extension of the Inverse Method to Probabilistic Timed Automata

SPROSTON, Jeremy James
2013-01-01

Abstract

Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation π_0 of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint K_0 on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the “inverse method”. The method presents the following advantages. First, since K_0 corresponds to a dense domain around π_0 on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to obtain a valuation satisfying K_0 which is as small as possible while preserving reachability probabilities, thus making the probabilistic analysis of the system easier and faster in practice. We provide examples of the application of our technique to models of randomized protocols, and introduce an extension of the method allowing the generation of a “probabilistic cartography” of a system.
2013
42
2
119
145
E. ANDRE; L. FRIBOURG; J. SPROSTON
File in questo prodotto:
File Dimensione Formato  
AFS-fmsd13_4aperto.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 553.56 kB
Formato Adobe PDF
553.56 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
art%3A10.1007%2Fs10703-012-0169-x.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 970.85 kB
Formato Adobe PDF
970.85 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/143906
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 7
social impact