The Library
Competitive optimisation on timed automata
Tools
Trivedi, Ashutosh (2009) Competitive optimisation on timed automata. PhD thesis, University of Warwick.

PDF
WRAP_THESIS_Trivedi_2009.pdf  Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader Download (967Kb)  Preview 

PDF
WRAP_THESIS_Trivedi_2009.pdf Restricted to Repository staff only  Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader Download (1073Kb) 
Official URL: http://webcat.warwick.ac.uk/record=b2283114~S15
Abstract
Timed automata are finite automata accompanied by a finite set of realvalued variables called clocks. Optimisation problems on timed automata are fundamental to the verification of properties of realtime systems modelled as timed automata, while the controlprogram synthesis problem of such systems can be modelled as a twoplayer game. This thesis presents a study of optimisation problems and twoplayer games on timed automata under a general heading of competitive optimisation on timed automata.
This thesis views competitive optimisation on timed automata as a multistage 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 averageprice objectives, and twoplayer turnbased 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.
Item Type:  Thesis or Dissertation (PhD) 

Subjects:  Q Science > QA Mathematics 
Library of Congress Subject Headings (LCSH):  Temporal automata, Mathematical optimization, Decision making  Mathematical models, Game theory 
Official Date:  April 2009 
Institution:  University of Warwick 
Theses Department:  Department of Computer Science 
Thesis Type:  PhD 
Publication Status:  Unpublished 
Supervisor(s)/Advisor:  Jurdziński, Marcin ; Lazić, Ranko 
Format of File:  
Extent:  162 leaves 
Language:  eng 
URI:  http://wrap.warwick.ac.uk/id/eprint/2243 
Request changes or add full text files to a record
Actions (login required)
View Item 