Maximally permissive controlled system synthesis for non-determinism and modal logic
Maximally permissive controlled system synthesis for non-determinism and modal logic
复制标题
非确定性和模态逻辑的最大许可受控系统综合
DOI：
10.1007/s10626-016-0231-8
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
W. Fokkink
中科院分区：
文献类型：
--
作者：
Allan van Hulst;M. Reniers;W. Fokkink
针对模态逻辑的要求，提出了一种基于非确定性自动机的受控系统综合新技术。综合，如本文所定义的，限制不受控制系统的行为规范，使其满足给定的逻辑表达式，同时遵守监督控制所规定的规则，如最大许可性和可控性。应用的需求形式主义用Gödel-Löb逻辑的不变和可达模式扩展了Hennessy-Milner逻辑，因此能够表达广泛的控制需求，例如标记状态可达性和死锁自由。本文通过在模态逻辑的不确定性环境中实现控制要求的最大许可性，以及通过部分双仿真处理可控性，为控制综合领域做出了贡献。我们给出了一个定义良好的完整的合成结果的推导，并进一步支持使用Coq证明助手创建的计算机验证证明。本文还以算法的形式给出了该综合方法，并对其计算复杂度进行了分析。我们证明了所提出的综合理论允许Ramadge-Wonham监督控制理论的完全可表达性，并在两个小型工业案例研究中说明了其适用性，包括关于可扩展性的分析。
We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.