Partial-Order Reduction for Supervisory Controller Synthesis

• 成果类型: Article
• 署名作者: van der Sanden, Bram; Geilen, Marc; Reniers, Michel; Basten, Twan
• 署名单位: Eindhoven University of Technology
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2021.3129161
• 发表日期: 2022
• 页码: 870-885
• 关键词: automata; timing; performance analysis; scalability; Aerospace electronics; Throughput; redundancy; Control system analysis; control systems; system analysis and design; Systems engineering and theory; Supervisory control; system performance

摘要

A key challenge in the synthesis and subsequent analysis of supervisory controllers is the impact of state-space explosion caused by concurrency. The main bottleneck is often the memory needed to store the composition of plant and requirement automata and the resulting supervisor. Partial-order reduction (POR) is a well-established technique that alleviates this issue in the field of model checking. It does so by exploiting redundancy in the model with respect to the properties of interest. For controller synthesis, the functional properties of interest are nonblockingness, controllability, and least-restrictiveness, but also performance properties, such as throughput and latency are of interest. We propose an on-the-fly POR on the input model that preserves both functional and performance properties in the synthesized supervisory controller. This improves the scalability of the synthesis (and any subsequent performance analysis). Synthesis experiments show the effectiveness of the POR on a set of realistic manufacturing system models.