On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems
On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems
复制标题
离散和密集时间系统的动态控制器综合
DOI：
10.1007/3-540-48119-2_15
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
K. Altisen
中科院分区：
文献类型：
--
作者：
S. Tripakis;K. Altisen
我们提出了新的技术，有效的控制器综合不定时和定时系统的不变性和可达性。在不定时的情况下，我们给出的控制器合成算法的背景下，有限的图形与ticontrollable和不可控的边缘，区分系统的行动和它的环境，分别。该算法是即时的，因为他们返回一个控制器，只要一个被发现，这避免了整个状态空间的生成。在定时的情况下，我们使用的时间定时自动机模型扩展可控和不可控的离散转换。我们的合成方法在这里只有一半的飞行，因为它依赖于一个先验生成的有限模型（图）的时间自动机，作为商的时间抽象互模拟。商图本质上是一个不定时的图，我们可以在其上应用不定时的实时算法来计算定时控制器。
We present novel techniques for eficient controller synthesis for untimed and timed systems with respect to invariance and reachability properties. In the untimed case, we give algorithms for controller synthesis in the context of finite graphs with ticontrollable and uncontrollable edges, distinguishing between the actions of the system and its environment, respectively. The algorithms are tion-the-fly, since they return a controller as soon as one is found, which avoids the generation of the whole state space.In the timed case, we use the model of titimed automata extended with controllable and uncontrollable discrete transitions. Our controller-synthesis method here is only half on-the-fly, since it relies on the a-priori generation of a finite model (graph) of the timed automaton, as quotient of the titime-abstracting bisimulation. The quotient graph is essentially an untimed graph, upon which we can apply the untimed on-the-fly algorithms to compute a timed controller.