Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach

TL;DR

The paper tackles verification of temporal specifications in interconnected discrete-time systems by introducing a resilience-based AGC framework that treats interconnections as structured disturbances. It defines a resilience metric to iteratively refine subsystem assumptions and guarantees, proving correctness and monotone refinement for two subsystems and extending to networks with L subsystems via weighted disturbance decomposition. The approach is instantiated for linear and nonlinear dynamics, with finite-horizon safety, exact-time reachability, and finite-horizon reachability, and validated through linear numerical examples and a nonlinear DC microgrid case study. The results demonstrate scalable, compositional verification of temporal logic properties in complex cyber-physical networks and provide a path toward future controller-synthesis extensions.

Abstract

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.

Figures (6)

• Figure 1: High-level representation of the proposed framework. Each subsystem $i$ receives internal inputs from neighbors and must meet a local specification $\psi_i$. The process starts by computing a resilience metric that indicates the maximum internal input each subsystem can handle while satisfying $\psi_i$. These metrics are used to iteratively refine AGCs across subsystems until convergence.
• Figure 2: Assumption sets calculated by Algorithm \ref{['Alg: AG FS 2']}, and 100 realizations of trajectories started from assumption sets while remaining in the safe set.
• Figure 3: Assumption sets calculated by Algorithm \ref{['Alg: AG ']}, and 15 trajectories starting from assumption sets and reaching the target set in step 3.
• Figure 4: Assumption sets calculated by Algorithm \ref{['Alg: AG ']}, and 15 trajectories starting from assumption sets and reaching the target set eventually in step 4.
• Figure 5: Five units architecture used for the simulations. Circles correspond to loads, and sources are denoted by double circles. Solid lines denote the transmission lines.

Theorems & Definitions (13)

• Definition II.1: Discrete-time subsystem
• Definition II.2: Discrete-time interconnected system
• Definition II.3: Resilience metric
• Definition II.4: AGCs
• Theorem III.1: Correctness
• Theorem III.2: Monotonicity
• Theorem III.3
• Remark 1
• Remark 2
• Example 1