时间自动机上的平均时间对策
Average-Time Games on Timed Automata
摘要：
在有限时间自动机的无限图上进行平均时间博弈。两个玩家，Min和Max，通过轮流执行定时转换来构建自动机的无限运行。最小博弈者希望最小化每次转移的平均时间，而最大博弈者希望最大化每次转移的平均时间。一个直接的结果是平均时间博弈的决定性的一个初等证明。这补充了我们对可达时间博弈的研究结果，并部分解决了Bouyer等人提出的问题，在定价时间自动机上设计求解平均价格博弈的算法。本文还建立了求解平均时间对策的精确计算复杂性：对于至少有两个时钟的时间自动机，该问题是EXPTIME完全的。
英文摘要：
An average-time game is played on the infinite graph of configurations of a finite timed automaton. The two players, Min and Max, construct an infinite run of the automaton by taking turns to perform a timed transition. Player Min wants to minimise the average time per transition and player Max wants to maximise it. A solution of average-time games is presented using a reduction to average-price game on a finite graph. A direct consequence is an elementary proof of determinacy for average-time games. This complements our results for reachability-time games and partially solves a problem posed by Bouyer et al., to design an algorithm for solving average-price games on priced timed automata. The paper also establishes the exact computational complexity of solving average-time games: the problem is EXPTIME-complete for timed automata with at least two clocks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
