Data-driven and model-based verification via Bayesian identification and reachability analysis

Research output: Contribution to journalArticleAcademicpeer-review

6 Citations (Scopus)
4 Downloads (Pure)

Abstract

This work develops a measurement-driven and model-based formal verification approach, applicable to dynamical systems with partly unknown dynamics. We provide a new principled method, grounded on Bayesian inference and on reachability analysis respectively, to compute the confidence that a physical system driven by external inputs and accessed under noisy measurements verifies a given property expressed as a temporal logic formula. A case study discusses the bounded- and unbounded-time safety verification of a partly unknown system, encompassed within a class of linear, time-invariant dynamical models with inputs and output measurements.

Original languageEnglish
Pages (from-to)115-126
Number of pages12
JournalAutomatica
Volume79
DOIs
Publication statusPublished - 1 May 2017

Keywords

  • Bayesian inference
  • Data-driven validation
  • Linear time-invariant models
  • Model-based verification
  • Reachability analysis
  • Statistical model checking
  • Temporal logic properties

Fingerprint Dive into the research topics of 'Data-driven and model-based verification via Bayesian identification and reachability analysis'. Together they form a unique fingerprint.

Cite this