Data-driven and model-based verification via Bayesian identification and reachability analysis. (May 2017)

• Record Type: Journal Article
• Authors: Haesaert, Sofie; Van den Hof, Paul M.J.; Abate, Alessandro
• Is Part Of: Automatica. Volume 79(2017)
• Page Start: 115
• Page End: 126
• Publication Date: 2017-05
• Subjects: Temporal logic properties -- Bayesian inference -- Linear time-invariant models -- Model-based verification -- Reachability analysis -- Data-driven validation -- Statistical model checking; Automatic control -- Periodicals; Automation -- Periodicals; 629.805
• DOI: 10.1016/j.automatica.2017.01.037
• Languages: English
• ISSNs: 0005-1098

Abstract

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.