Competitive Optimisation on Timed Automata.
Ashutosh Trivedi
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.
PhD thesis, Deaprtment of Computer Science, The University of Warwick, 2009.
PDF © 2009 University of Warwick.