论文标题
在无环时机中计算最大允许的策略
Computing maximally-permissive strategies in acyclic timed automata
论文作者
论文摘要
定时自动机是用于实时系统建模和推理的方便数学模型。虽然它们提供了表示此类系统定时方面的有力方法，但定时自动机采用任意精度和零延迟操作。特别是，可以在定时的自动机中声明一个状态，但无法在IT模型的物理系统中到达。在本文中，我们将允许的策略视为克服这个问题的一种方式：此类策略提出了延迟的间隔，而不是单个延误，旨在达到目标状态，无论实际发生哪种延迟。我们开发了一种用于计算无环时自动机和游戏中最佳允许性（以及相关的最大允许策略）的算法。
Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.
