基于SAT的分布式反应控制协议综合方法用于布尔网络
SAT-based Distributed Reactive Control Protocol Synthesis for Boolean Networks
AI总结：
本文提出了一种基于SAT的分布式反应控制协议综合方法，用于布尔网络。通过有向无环图表示布尔子系统的网络，并基于部分序结构递归计算每个子系统的局部合同和控制协议，从而保证全局合同的满足。
摘要：
本文考虑了在分布式方式下对布尔网络的分布式反应控制协议的综合。我们从一个有向无环图表示的布尔子系统网络和一个给定的全局合同（即假设-保证对）开始。假设捕捉环境行为，保证是系统需要满足的要求。基于有向无环图诱导的部分序结构，每个子系统递归地计算局部假设-保证合同以及确保这些局部合同的局部控制协议。通过构造，实施这些局部控制协议将保证满足全局假设-保证合同。此外，在这种情况下，局部控制协议的综合归结为量化可满足性（QSAT）问题。我们还讨论了影响所提出算法完整性的网络结构特性。作为应用，我们展示了如何将飞机电力系统表示为布尔网络，并从全局假设-保证合同中综合出分布式控制协议。假设捕捉系统组件的可能故障，保证捕捉与电力分配相关的安全要求。
英文摘要：
This paper considers the synthesis of distributed reactive control protocols for a Boolean network in a distributed manner. We start with a directed acyclic graph representing a network of Boolean subsystems and a global contract, given as an assumption-guarantee pair. Assumption captures the environment behavior, and guarantee is the requirements to be satisfied by the system. Local assumption-guarantee contracts, together with local control protocols ensuring these local contracts, are computed recursively for each subsystem based on the partial order structure induced by the directed acyclic graph. By construction, implementing these local control protocols together guarantees the satisfaction of the global assumption-guarantee contract. Moreover, local control protocol synthesis reduces to quantified satisfiability (QSAT) problems in this setting. We also discuss structural properties of the network that affect the completeness of the proposed algorithm. As an application, we show how an aircraft electric power system can be represented as a Boolean network, and we synthesize distributed control protocols from a global assumption-guarantee contract. The assumptions capture possible failures of the system components, and the guarantees capture safety requirements related to power distribution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
