论文标题
离散事件系统的运行到完成控制器的合成
Synthesis of Run-To-Completion Controllers for Discrete Event Systems
论文作者
论文摘要
离散事件系统的控制器必须实现其目标,尽管其环境能够在受控事件和不受控制的事件之间解决种族条件。修理控制者失去所有种族有时是不现实的。在许多情况下,一个现实的假设是,控制器有时会赢得比赛,并且足够快,可以执行多个动作而不会中断。但是,要使用对DES控制的控制,为了对这种情况进行建模,这需要引入有关调度的外国假设,这些假设很难正确弄清楚。我们提出了一个更加平衡的控制问题,称为“运行式完成”(RTC),以减轻此问题。 RTC自然支持执行假设,在该假设中,控制器和环境都可以确保启动和执行动作序列,而无需无限期地互相泛滥或延迟。我们考虑以线性时间逻辑形式给出规格的上下文中的控制DES。我们正式化了RTC控制问题,并显示如何将其简化为标准控制问题。
A controller for a Discrete Event System must achieve its goals despite that its environment being capable of resolving race conditions between controlled and uncontrolled events.Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.