TY - GEN
T1 - Compositional Safety Verification of Infinite Networks
T2 - 2024 European Control Conference, ECC 2024
AU - Aminzadeh, Ali
AU - Swikir, Abdalla
AU - Haddadin, Sami
AU - Lavaei, Abolfazl
N1 - Publisher Copyright:
© 2024 EUCA.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85200558309&partnerID=8YFLogxK
U2 - 10.23919/ECC64448.2024.10591289
DO - 10.23919/ECC64448.2024.10591289
M3 - Conference contribution
AN - SCOPUS:85200558309
T3 - 2024 European Control Conference, ECC 2024
SP - 545
EP - 551
BT - 2024 European Control Conference, ECC 2024
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 25 June 2024 through 28 June 2024
ER -