基于契约的网络化系统在任意划分下的时序逻辑规范分解
Contract-Based Decomposition of Temporal Logic Specifications for Networked Systems under Arbitrary Partitions
- Institute of Science Tokyo（东京科学大学）
- DENSO IT Laboratory（电装IT实验室）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出基于假设-保证契约的时序逻辑规范分解方法，使划分成为自由设计变量，并给出任意划分下分解正确的条件，通过管方法综合控制器，仿真验证权衡。
AI中文摘要：
计算复杂度是网络化系统形式化综合的固有局限，将全局规范分解为局部规范以保守性为代价缓解了这一局限。由于划分的粒度决定了这一权衡，将划分视为设计变量是合理的，这要求局部规范对每种划分都保持正确。为此，本文为每个智能体赋予一个局部规范，以假设-保证契约的形式书写，智能体可从局部信息中建立该契约。我们首先推导出这些契约在给定划分下分解全局规范的充要条件。在此基础上，我们进一步给出一个条件，使得分解对每种划分都正确，从而划分成为自由设计变量。对于线性动力学和具有仿射谓词的信号时序逻辑公式，我们进一步通过基于管的方法为每个联盟综合控制器。最后，在输入耦合水箱网络上的仿真展示了划分选择如何在计算成本与保守性之间进行权衡。
英文摘要：
Computational complexity is an inherent limitation of formal synthesis for networked systems, and decomposing the global specification into local ones relaxes this limitation at the cost of conservatism. Since the granularity of the partition governs this trade-off, it is reasonable to treat the partition as a design variable, which calls for local specifications that remain correct for every partition. To this end, this paper gives each agent a local specification, written as an assume-guarantee contract that the agent can establish from local information. We first derive a necessary and sufficient condition for these contracts to decompose the global specification under a given partition. Building on this, we then present a condition under which the decomposition is correct for every partition, so that the partition becomes a free design variable. For linear dynamics and signal temporal logic formulas with affine predicates, we further synthesize a controller for each coalition by a tube-based approach. Finally, simulations on a network of input-coupled tanks show how the choice of partition trades computational cost against conservatism.
