Compositional Safety Verification of Infinite Networks: A Data-Driven Approach

Ali Aminzadeh, Abdalla Swikir, Sami Haddadin, Abolfazl Lavaei

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This paper develops a compositional framework for formal safety verification of an interconnected network comprised of a countably infinite number of discrete-time nonlinear subsystems with unknown mathematical models. Our proposed scheme involved subdividing the infinite network problem into individual subsystems, wherein the safety concept is modelled through a robust optimization program (ROP) via a notion of local-barrier certificates (L-BC). To address the difficulties associated with solving the ROP directly, primarily due to the absence of a mathematical model, we gather finite data from subsystem trajectories and leverage them to provide a scenario optimization program (SOP). We proceed with solving the resulted SOP and construct a local-barrier certificate for each unknown subsystem with a guarantee of correctness. Finally, in accordance with some small-gain conditions, we construct a global-barrier certificate (G-BC) derived from individual local certificates of subsystems, thus guaranteeing the safety of the infinite network within infinite time horizons. The practicality of our compositional findings becomes evident through a vehicle platooning scenario, characterized by a countably infinite number of vehicles with a single leader and an unlimited number of followers.

Original languageEnglish
Title of host publication2024 European Control Conference, ECC 2024
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages545-551
Number of pages7
ISBN (Electronic)9783907144107
DOIs
StatePublished - 2024
Event2024 European Control Conference, ECC 2024 - Stockholm, Sweden
Duration: 25 Jun 202428 Jun 2024

Publication series

Name2024 European Control Conference, ECC 2024

Conference

Conference2024 European Control Conference, ECC 2024
Country/TerritorySweden
CityStockholm
Period25/06/2428/06/24

Fingerprint

Dive into the research topics of 'Compositional Safety Verification of Infinite Networks: A Data-Driven Approach'. Together they form a unique fingerprint.

Cite this