Data-driven Abstractions for Verification of Linear Systems

Journal article (2023)

Authors

R. Coppola Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering

A. Peruffo Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering

M. Mazo Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering

Research Group

Team Manuel Mazo Jr (Mechanical, Maritime and Materials Engineering) (TU Delft)

DOI: https://doi.org/10.1109/LCSYS.2023.3288731

Optimization Modeling Uncertainty Trajectory Automata Computational modeling Symbols Picture archiving and communication systems Statistical learning Extraterrestrial measurements

More Info

expand_more

To reference this document use:

http://resolver.tudelft.nl/uuid:21cdc4f3-0abc-423b-b715-4ecdab2ba11c

Published Date

2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Mechanical, Maritime and Materials Engineering

Department

Delft Center for Systems and Control

Research Group

Team Manuel Mazo Jr

Abstract

We introduce a novel approach for the construction of symbolic abstractions - simpler, finite-state models - which mimic the behaviour of a system of interest, and are commonly utilized to verify complex logic specifications. Such abstractions require an exhaustive knowledge of the concrete model, which can be difficult to obtain in real-world applications. To overcome this, we propose to sample finite length trajectories of an unknown system and build an abstraction based on the concept of ℓ -completeness. To this end, we introduce the notion of probabilistic behavioural inclusion. We provide probably approximately correct (PAC) guarantees that such an abstraction, constructed from experimental symbolic trajectories of finite length, includes all behaviours of the concrete system, for both finite and infinite time horizon. Finally, our method is displayed with numerical examples.

Files

Data_Driven_Abstractions_for_V... (.pdf)

(.pdf | 0.578 Mb)

- Embargo expired in 22-12-2023