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

我们提出了一种基于弹性的框架，用于计算可行的假设-保证契约，以确保互联离散时间系统中时间规范的满足。互联效应被建模为结构化扰动。我们使用一种弹性指标，即保持局部规范成立的最大扰动，来迭代地细化各子系统间的假设与保证。我们首先证明了两个子系统情形下保证的正确性与单调细化。然后，我们使用互联效应的加权组合，将我们的方法扩展到 $L$ 个子系统的一般网络。我们通过满足有限时域安全性、精确时间可达性和有限时域可达性规范，将该框架应用于线性系统；并通过满足一般有限时域规范，将其应用于非线性系统。我们的方法通过线性数值算例和非线性直流微电网案例研究进行了演示，展示了我们的框架对基于组合推理验证时序逻辑规范的影响。