We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters under mild conditions. This enables us to devise a novel Bayesian statistical algorithm which performs model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and considerably faster than naive parameter exploration with standard statistical model checking methods. (C) 2016 Elsevier Inc. All rights reserved.

Smoothed model checking for uncertain Continuous-Time Markov Chains / Bortolussi, L.; Milios, D.; Sanguinetti, G.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 247:(2016), pp. 235-253. [10.1016/j.ic.2016.01.004]

Smoothed model checking for uncertain Continuous-Time Markov Chains

Sanguinetti, G.
2016-01-01

Abstract

We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters under mild conditions. This enables us to devise a novel Bayesian statistical algorithm which performs model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and considerably faster than naive parameter exploration with standard statistical model checking methods. (C) 2016 Elsevier Inc. All rights reserved.
2016
247
235
253
https://arxiv.org/abs/1402.1450
Bortolussi, L.; Milios, D.; Sanguinetti, G.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540116000055-main.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non specificato
Dimensione 873.37 kB
Formato Adobe PDF
873.37 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/20.500.11767/117341
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 54
  • ???jsp.display-item.citation.isi??? 37
social impact