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.

翻译：我们提出了一种基于弹性度量的框架，用于计算可行的假设-保证契约，以确保互连离散时间系统中时序规范的满足。互连效应被建模为结构化扰动。我们采用弹性度量——即局部规范得以维持的最大扰动——来迭代地精化各子系统间的假设与保证。首先，我们针对两个子系统证明了保证的正确性与单调精化性质。随后，通过引入互连效应的加权组合，我们将方法推广至包含L个子系统的一般网络。在线性系统上，我们通过满足有限时域安全性、精确时间可达性与有限时域可达性规范来实例化该框架；在非线性系统上，则通过实现一般有限时域规范来实例化。通过数值线性示例及一个非线性直流微电网案例研究，我们展示了该方法在利用组合推理验证时序逻辑规范方面的实际影响。