<p>This work presents a comprehensive investigation into the robust supervisory control of metric discrete event systems, which are modeled as finite state automata and incorporate metric functions to measure state distances. While existing studies on supervisory control primarily focus on qualitative analysis and provide a binary answer regarding whether the controlled system satisfies the given specifications, our work introduces Metric Discrete Event Systems to quantitatively investigate robust supervisory control. Specifications are defined using a fragment of Linear Temporal Logic (LTL), specifically syntactically co-safe LTL (scLTL). Environmental disturbances can cause deviations from the system’s nominal behaviors, thereby hindering the successful accomplishment of the original tasks. To mitigate this issue, we design supervisors to ensure that the controlled system degrades gracefully under adverse conditions. We formally define the robustness of supervisors in a topological context and formulate two key problems: verification of the existence of robust supervisors and synthesis of optimal robust supervisors. We propose a two-player game framework to address both problems. First, we introduce a bipartite structure called distance bipartite transition system (DBTS) as the arena of the game between the supervisor and the environment. The verification problem is then reformulated and solved as a reachability game on a special DBTS, where the set of target states is properly defined. For the synthesis problem, we define a sequence of vectors to track the shortest distance to the accepting states under disturbances and compute their fixed-point using dynamic programming techniques. Then we synthesize the optimal winning strategy of the supervisor, which eventually yields the optimal robust supervisor. Finally, we provide a case study of robot task planning to validate the performance of our proposed methods that demonstrates persuasive results in real-world scenarios.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On Robust Supervisory Control of Metric Discrete Event Systems for scLTL Specifications

  • Peiran Liu,
  • Shaowen Miao,
  • Yiding Ji,
  • Xiang Yin

摘要

This work presents a comprehensive investigation into the robust supervisory control of metric discrete event systems, which are modeled as finite state automata and incorporate metric functions to measure state distances. While existing studies on supervisory control primarily focus on qualitative analysis and provide a binary answer regarding whether the controlled system satisfies the given specifications, our work introduces Metric Discrete Event Systems to quantitatively investigate robust supervisory control. Specifications are defined using a fragment of Linear Temporal Logic (LTL), specifically syntactically co-safe LTL (scLTL). Environmental disturbances can cause deviations from the system’s nominal behaviors, thereby hindering the successful accomplishment of the original tasks. To mitigate this issue, we design supervisors to ensure that the controlled system degrades gracefully under adverse conditions. We formally define the robustness of supervisors in a topological context and formulate two key problems: verification of the existence of robust supervisors and synthesis of optimal robust supervisors. We propose a two-player game framework to address both problems. First, we introduce a bipartite structure called distance bipartite transition system (DBTS) as the arena of the game between the supervisor and the environment. The verification problem is then reformulated and solved as a reachability game on a special DBTS, where the set of target states is properly defined. For the synthesis problem, we define a sequence of vectors to track the shortest distance to the accepting states under disturbances and compute their fixed-point using dynamic programming techniques. Then we synthesize the optimal winning strategy of the supervisor, which eventually yields the optimal robust supervisor. Finally, we provide a case study of robot task planning to validate the performance of our proposed methods that demonstrates persuasive results in real-world scenarios.