Competative optimisation on timed automata
Competative optimisation on timed automata
复制标题
时间自动机的竞争优化
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Hartford
中科院分区：
文献类型：
--
作者：
E. Bondestam;Andrejs Breikss;M. Hartford
时间自动机是伴随着一组有限的实值变量（称为时钟）的有限自动机。时间自动机的优化问题是验证建模为时间自动机的实时系统的属性的基础，而这种系统的控制程序合成问题可以建模为一个两人游戏。本论文在时间自动机竞争最佳化的大标题下，研究时间自动机上的最佳化问题与二人对策。
本论文将时间自动机上的竞争性最佳化视为一个多阶段的决策过程，其中一个或两个玩家面临选择一系列时间动作的问题-一个时间延迟和一个动作-以优化他们的目标。这类问题的解决方案由目标的“最优”值和每个参与者的“最优”策略组成。本文介绍了一种新的策略，称为边界策略，它建议玩家采取一种形式为（B，c，a）的符号定时移动-“等到时钟c的值非常接近整数B，然后执行一个标记为动作a的转换”。本文所讨论的竞争最优化问题的一个显著特点是存在最优边界策略。也许令人惊讶的是，许多竞争性的优化问题的时间自动机的实际利益承认最佳的边界策略。例如，具有可达性价格、折扣价格和平均价格目标的优化问题，以及具有可达性时间和平均时间目标的双人回合制游戏。
最优边界策略的存在允许人们使用一种新的时间自动机抽象，称为边界区域图，其中玩家只能使用边界策略。边界区域图的一个有趣的性质是，对于每个状态，可达状态的集合是有限的。因此，最优边界策略的存在允许我们将时间自动机上的竞争优化问题简化为有限图上的相应竞争优化问题。
Timed automata are finite automata accompanied by a finite set of real-valued variables called clocks. Optimisation problems on timed automata are fundamental to the verification of properties of real-time systems modelled as timed automata, while the control-program synthesis problem of such systems can be modelled as a two-player game. This thesis presents a study of optimisation problems and two-player games on timed automata under a general heading of competitive optimisation on timed automata.
This thesis views competitive optimisation on timed automata as a multi-stage decision process, where one or two players are confronted with the problem of choosing a sequence of timed moves—a time delay and an action—in order to optimise their objectives. A solution of such problems consists of the “optimal” value of the objective and an “optimal” strategy for each player. This thesis introduces a novel class of strategies, called boundary strategies, that suggest to a player a symbolic timed move of the form (b, c, a)— “wait until the value of the clock c is in very close proximity of the integer b, and then execute a transition labelled with the action a”. A distinctive feature of the competitive optimisation problems discussed in this thesis is the existence of optimal boundary strategies. Surprisingly perhaps, many competitive optimisation problems on timed automata of practical interest admit optimal boundary strategies. For example, optimisation problems with reachability price, discounted price, and average-price objectives, and two-player turn-based games with reachability time and average time objectives.
The existence of optimal boundary strategies allows one to work with a novel abstraction of timed automata, called a boundary region graph, where players can use only boundary strategies. An interesting property of a boundary region graph is that, for every state, the set of reachable states is finite. Hence, the existence of optimal boundary strategies permits us to reduce competitive optimisation problem on a timed automaton to the corresponding competitive optimisation problem on a finite graph.