Data-driven Abstractions for Verification of Linear Systems

Data-driven Abstractions for Verification of Linear Systems

Coppola, R. (TU Delft Team Manuel Mazo Jr)
Peruffo, A. (TU Delft Team Manuel Mazo Jr)
Mazo, M. (TU Delft Team Manuel Mazo Jr)

2023

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.

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

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

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

2023-12-22

2475-1456

IEEE Control Systems Letters, 7, 2737-2742

Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.

Institutional Repository

journal article

© 2023 R. Coppola, A. Peruffo, M. Mazo