模式-目标游戏:用于控制应用的反应合成
Mode-Target Games: Reactive Synthesis for Control Applications
AI总结:
本文提出了一类线性时序逻辑(LTL)规范,可在多项式时间内合成控制器。该规范称为模式-目标(MT),受控制应用中多种模式及其对应目标的启发。将合成 enforcing MT 规范的控制器问题建模为游戏,并提供一个需要 O(∑i ti n²) 符号步骤的算法。
摘要:
在本文中,我们介绍了一类线性时序逻辑(LTL)规范,其中控制器合成问题可以在多项式时间内解决。新的规范类是LTL的一个片段,我们称之为模式-目标(MT),受众多控制应用的启发,其中存在模式和对应(可能多个)目标。我们将合成 enforcing MT 规范的控制器问题建模为游戏,并提供一个需要 O(∑i ti n²) 符号步骤的算法,其中 n 是游戏图中的状态数,ti 是对应模式 i 的目标数。
英文摘要:
In this paper we introduce a class of Linear Temporal Logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The new class of specifications is an LTL fragment that we term Mode-Target (MT) and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide an algorithm that requires $O(\sum_i t_i n^2)$ symbolic steps, where $n$ is the number of states in the game graph, and $t_i$ is the number of targets corresponding to mode $i$.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。