Data-driven verification of stochastic linear systems with signal temporal logic constraints

Cyber-physical systems usually have complex dynamics and are required to fulfill complex tasks. In recent years, formal methods from Computer Science have been used by control theorists for both describing the required tasks and ensuring that they are fulfilled by the systems. The crucial drawback of formal methods is that a complete model of the system often needs to be available. The main goal of this paper is to study formal verification of linear time-invariant systems with respect to a fragment of temporal logic specifications when only a partial knowledge of the model is available, i.e., a parameterized model of the system is known but the exact values of the parameters are unknown. We provide a probabilistic measure for the satisfaction of the specification by trajectories of the system under the influence of uncertainty. We assume these specifications are expressed as signal temporal logic formulae and provide an approach that relies on gathering input-output data from the system and employs Bayesian inference on the collected data to associate a notion of confidence to the satisfaction of the specification. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system. The inner layer is with respect to the uncertainties in dynamics and observed data while the outer layer is with respect to the distribution over the parameter space. The latter is updated using Bayesian inference on the collected data. The proposed approach is demonstrated in two case studies. (C) 2021 The Authors. Published by Elsevier Ltd.

Automated summary

This paper investigates the formal verification of linear time-invariant systems with a partial knowledge of the model, using probabilistic measures, Bayesian inference, and signal temporal logic formulae. The approach combines data-driven and model-based techniques to have a two-layer probabilistic reasoning over the behavior of the system, considering uncertainties in dynamics and observed data in the inner layer, and parameter space distribution in the outer layer. The proposed approach is demonstrated in two case studies.