论文标题
通过假设合同的凸参数化的组成合成
Compositional Synthesis via a Convex Parameterization of Assume-Guarantee Contracts
论文作者
论文摘要
我们开发了一个假设保证框架，用于控制有限的时间范围和避免或无限时间不变性规格的大规模线性（时变）系统。合同描述了单个子系统的一组国家和控制。如果相互的假设和保证以我们形式化的方式匹配，则一组合同正确组成。我们提出了合同的丰富参数化，使得正确组成的参数集为凸。此外，我们设计了参数的潜在功能，该功能描述了合同与正确组成的距离。因此，汇总系统的验证和合成被打破以求解单个子系统的小型凸程序，其中最终以组成方式实现了正确性。说明性示例证明了我们方法的可扩展性。
We develop an assume-guarantee framework for control of large scale linear (time-varying) systems from finite-time reach and avoid or infinite-time invariance specifications. The contracts describe the admissible set of states and controls for individual subsystems. A set of contracts compose correctly if mutual assumptions and guarantees match in a way that we formalize. We propose a rich parameterization of contracts such that the set of parameters that compose correctly is convex. Moreover, we design a potential function of parameters that describes the distance of contracts from a correct composition. Thus, the verification and synthesis for the aggregate system are broken to solving small convex programs for individual subsystems, where correctness is ultimately achieved in a compositional way. Illustrative examples demonstrate the scalability of our method.
