We consider the synthesis problem on timed automata with B\"uchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards.

翻译：我们考虑具有Büchi目标的时序自动机上的综合问题，其中控制器做出的延迟选择会受到微小扰动。通常，控制器需要避免准时守卫，例如测试时钟等于某个常数。在本工作中，我们推广到允许控制器在无扰动情况下执行自动机中准时转移的鲁棒性设定。为了表征能够抵抗扰动性的循环，我们在自动机接受循环的可达性关系上引入了一种新的结构性要求。该性质基于区域抽象进行表述，并推广了无准时守卫情况下获胜循环的现有表征。我们证明，尽管存在准时守卫，该问题仍然保持在PSPACE复杂度类内。