Robust Timed Automata
Robust Timed Automata
复制标题
鲁棒定时自动机
作者：
Vineet Gupta;T. Henzinger;R. Jagadeesan
我们定义了鲁棒的时间自动机，它是接受所有轨迹的时间自动机“鲁棒”：如果一个鲁棒的时间自动机接受一个轨迹，那么它必须接受相邻的轨迹也;如果一个鲁棒的时间自动机拒绝一个轨迹，那么它必须拒绝相邻的轨迹也。通过修改时间自动机的区域构造，我们证明了鲁棒时间自动机的空性问题仍然是可判定的。然后，我们表明，像时间自动机，强大的时间自动机不能确定。这个结果有点出乎意料，因为在时态逻辑中，去除实时等式约束会导致一个在所有布尔运算下都是封闭的可判定理论。
We define robust timed automata, which are timed automata that accept all trajectories “robustly”: if a robust timed automaton accepts a trajectory, then it must accept neighboring trajectories also; and if a robust timed automaton rejects a trajectory, then it must reject neighboring trajectories also. We show that the emptiness problem for robust timed automata is still decidable, by modifying the region construction for timed automata. We then show that, like timed automata, robust timed automata cannot be determinized. This result is somewhat unexpected, given that in temporal logic, the removal of realtime equality constraints is known to lead to a decidable theory that is closed under all boolean operations.