Title
Quantitative Games on Probabilistic Timed Automata
Abstract
Two-player zero-sum games are a well-established model for syn- thesising controllers that optimise some performance criterion. In such games one player represents the controller, while the other describes the (adversarial) environment, and controller synthesis corresponds to computing the optimal strategies of the controller for a given criterion. Asarin and Maler initiated the study of quantitative games on (non-probabilistic) timed automata by synthesis- ing controllers which optimise the time to reach a final state. The correctness and termination of their approach was dependent on exploiting the properties of a special class of functions, called simple functions, that can be finitely represented. In this paper we consider quantitative games over probabilistic timed automata. Since the concept of simple functions is not sufficient to solve games in this setting, we generalise simple functions to so-called quasi-simple functions. Then, using this class of functions, we demonstrate that the problem of solving games with either expected reachability-time or expected discounted-time criteria on probabilistic timed automata are in NEXPTIME \ co-NEXPTIME. As a side result, we also show that the problem of solving discounted-time games on timed automata is EXPTIME-complete.
Year
Venue
Keywords
2010
Clinical Orthopaedics and Related Research
zero sum game,game theory
Field
DocType
Volume
NEXPTIME,Combinatorial game theory,Mathematical optimization,Control theory,Correctness,Automaton,Simple function,Theoretical computer science,Timed automaton,Probabilistic logic,Mathematics
Journal
abs/1001.1
Citations 
PageRank 
References 
1
0.35
20
Authors
3
Name
Order
Citations
PageRank
Marta Z. Kwiatkowska16118322.21
Gethin Norman24163193.68
Ashutosh Trivedi314928.08