Reachset-Conformant System Identification

TL;DR

This paper introduces a generalized framework for automatically identifying reachset-conformant models, including nonlinear and input-output models, to enhance formal verification of complex cyber-physical systems.

Contribution

It extends existing linear methods to nonlinear and various input-output models, accommodating different prior knowledge levels for system identification.

Findings

Successfully identified reachset-conformant models from data

Demonstrated robustness on simulated and real-world data

Extended applicability to nonlinear and black-box models

Abstract

Formal verification techniques play a pivotal role in ensuring the safety of complex cyber-physical systems. To transfer model-based verification results to the real world, we require that the measurements of the target system lie in the set of reachable outputs of the corresponding model, a property we refer to as reachset conformance. This paper is on automatically identifying those reachset-conformant models. While state-of-the-art reachset-conformant identification methods focus on linear state-space models, we generalize these methods to nonlinear state-space models and linear and nonlinear input-output models. Furthermore, our identification framework adapts to different levels of prior knowledge on the system dynamics. In particular, we identify the set of model uncertainties for white-box models, the parameters and the set of model uncertainties for gray-box models, and entire reachset-conformant black-box models from data. The robustness and efficacy of our framework are demonstrated in extensive numerical experiments using simulated and real-world data.