Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908696221581312 |
|---|---|
| author | Monir, Negar Si, Youssef Ait Das, Ratnangshu Jagtap, Pushpak Saoud, Adnane Soudjani, Sadegh |
| author_facet | Monir, Negar Si, Youssef Ait Das, Ratnangshu Jagtap, Pushpak Saoud, Adnane Soudjani, Sadegh |
| contents | We propose a resilience-based framework for computing feasible assume-guarantee contracts that ensure the satisfaction of temporal specifications in interconnected discrete-time systems. Interconnection effects are modeled as structured disturbances. We use a resilience metric, the maximum disturbance under which local specifications hold, to refine assumptions and guarantees across subsystems iteratively. We first demonstrate correctness and monotone refinement of guarantees for two subsystems. Then, we extend our approach to general networks of L subsystems using weighted combinations of interconnection effects. We instantiate the framework on linear systems by meeting finite-horizon safety, exact-time reachability, and finite-horizon reachability specifications, and on nonlinear systems by fulfilling general finite-horizon specifications. Our approach is demonstrated through numerical linear examples and a nonlinear DC microgrid case study, showcasing the impact of our framework on verifying temporal logic specifications with compositional reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_01832 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach Monir, Negar Si, Youssef Ait Das, Ratnangshu Jagtap, Pushpak Saoud, Adnane Soudjani, Sadegh Systems and Control Logic in Computer Science Dynamical Systems We propose a resilience-based framework for computing feasible assume-guarantee contracts that ensure the satisfaction of temporal specifications in interconnected discrete-time systems. Interconnection effects are modeled as structured disturbances. We use a resilience metric, the maximum disturbance under which local specifications hold, to refine assumptions and guarantees across subsystems iteratively. We first demonstrate correctness and monotone refinement of guarantees for two subsystems. Then, we extend our approach to general networks of L subsystems using weighted combinations of interconnection effects. We instantiate the framework on linear systems by meeting finite-horizon safety, exact-time reachability, and finite-horizon reachability specifications, and on nonlinear systems by fulfilling general finite-horizon specifications. Our approach is demonstrated through numerical linear examples and a nonlinear DC microgrid case study, showcasing the impact of our framework on verifying temporal logic specifications with compositional reasoning. |
| title | Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach |
| topic | Systems and Control Logic in Computer Science Dynamical Systems |
| url | https://arxiv.org/abs/2509.01832 |