Title: Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach Show Chinese title

Title: 可行假设-保证契约的计算：一种基于弹性的方法

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. For two subsystems, we demonstrate correctness, monotone refinement of guarantees, and that the resulting assumptions are maximal within ball-shaped sets. Additionally, 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-time 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 in verifying temporal logic specifications with compositional reasoning. Show Chinese abstract

Abstract: 我们提出了一种基于弹性性的框架，用于计算可行的假设-保证契约，以确保互连离散时间系统中时间规范的满足。互连效应被建模为结构化扰动。我们使用一个弹性度量，即在局部规范保持有效的最大扰动，来迭代地精炼子系统的假设和保证。对于两个子系统，我们证明了正确性、保证的单调精炼性，并且得出的假设在球形集合内是最大的。此外，我们通过互连效应的加权组合将方法扩展到一般的L个子系统的网络。我们通过满足有限时间范围内的安全、精确时间可达性和有限时间可达性规范，在线性系统上实例化了该框架；并通过满足一般有限时间范围规范，在非线性系统上实例化了该框架。我们的方法通过数值线性例子和一个非线性直流微电网案例研究进行了演示，展示了我们的框架在使用组合推理验证时间逻辑规范中的影响。