Maximally permissive controlled system synthesis for non-determinism and modal logic

详细信息    查看全文

• 作者：A. C. van Hulst ; M. A. Reniers ; W. J. Fokkink
• 关键词：Controlled system synthesis ; Modal logic ; Non ; determinism ; Maximal permissiveness ; Controllability ; Partial bisimulation
• 刊名：Discrete Event Dynamic Systems
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：27
• 期：1
• 页码：109-142
• 全文大小：2398KB
• 刊物类别：Mathematics and Statistics
• 刊物主题：Systems Theory, Control; Operation Research/Decision Theory; Convex and Discrete Geometry; Electrical Engineering; Manufacturing, Machines, Tools;
• 出版者：Springer US
• ISSN：1573-7594
• 卷排序：27

文摘

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.