Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTG has attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).
翻译:加权计时游戏(简称WTG)是用来描述涉及实时问题的控制器合成问题的最广泛使用的模式。 不幸的是,这些问题非常困难,而且一般而言是不可估量的。 因此,1小时的WTG引起了很大的注意,特别是因为当只允许非负权重时,人们知道它们是可以分化的。然而,在考虑任意权重时,尽管最近做了几项工作,它们的变分性状况仍然不明。在本文件中,我们积极解决这一问题,并表明其价值函数可以用指数时间(如果重量在单数中编码的话)计算。