论文标题
非终止过程的监管控制器合成是一个义务的游戏
Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game
论文作者
论文摘要
我们提出了一种新算法，以解决模型为$ω$ regratular Automata的非终止过程中的监督控制问题。 Thistle在1995年获得了一种解决此问题的解决方案，该解决方案使用了自动机的复杂操作。我们通过减少对游戏的减少来展示问题的新解决方案，而该游戏又可以将其简化为$ω$的反应性合成。因此，我们的还原导致了使用反应性合成工具基于操纵状态集的符号算法。
We present a new algorithm to solve the supervisory control problem over non-terminating processes modeled as $ω$-regular automata. A solution to this problem was obtained by Thistle in 1995 which uses complex manipulations of automata. We show a new solution to the problem through a reduction to obliging games, which, in turn, can be reduced to $ω$-regular reactive synthesis. Therefore, our reduction results in a symbolic algorithm based on manipulating sets of states using tools from reactive synthesis.
