Timed Alternating-Time Temporal Logic
Timed Alternating-Time Temporal Logic
复制标题
定时交替时间逻辑
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Vinayak S. Prabhu
中科院分区：
文献类型：
--
作者：
T. Henzinger;Vinayak S. Prabhu
我们将冻结量词添加到游戏逻辑 ATL 中，以便为在定时结构上玩的游戏指定实时目标。我们通过将玩家限制在物理上有意义的策略来定义所得逻辑 TATL 的语义，这不会阻止时间发散。我们证明 TATL 可以通过定时自动机游戏进行模型检查。我们还为物理上有意义的策略指定了定时优化问题，并且我们表明，对于定时自动机游戏，最佳答案可以在任何精度范围内近似。
We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.