Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.

Machine Learning Methods in Statistical Model Checking and System Design – Tutorial

BORTOLUSSI, LUCA;
2015

Abstract

Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.
9783319238197
9783319238203
http://link.springer.com/bookseries/558
http://www.springer.com/gp/book/9783319238197
File in questo prodotto:
File Dimensione Formato  
RV2015_tutorial-post.pdf

accesso aperto

Descrizione: pdf post-print
Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Digital Rights Management non definito
Dimensione 581.65 kB
Formato Adobe PDF
581.65 kB Adobe PDF Visualizza/Apri
RV2015-2.pdf

non disponibili

Descrizione: pdf editoriale
Tipologia: Documento in Versione Editoriale
Licenza: Digital Rights Management non definito
Dimensione 465.02 kB
Formato Adobe PDF
465.02 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/11368/2860877
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 3
social impact