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

Journal article

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.

Authors: Haesaert, S; Van den Hof, P; Abate, A

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Automatica
• Volume: 79
• Pages: 115–126
• Publication date: 2017-03-02
• Acceptance date: 2016-10-15
• DOI: 10.1016/j.automatica.2017.01.037
• EISSN: 1873-2836
• ISSN: 0005-1098
• Keywords: temporal logic properties; reachability analysis; data-driven validation; model-based verification; statistical model checking; linear time-invariant models; Bayesian inference