@inproceedings{14fdafd5794443969e0cdb12d6690a63,

title = "On Time with Minimal Expected Cost!",

abstract = "(Priced) timed games are two-player quantitative games involving an environment assumed to be completely antogonistic. Classical analysis consists in the synthesis of strategies ensuring safety, time-bounded or cost-bounded reachability objectives. Assuming a randomized environment, the (priced) timed game essentially defines an infinite-state Markov (reward) decision proces. In this setting the objective is classically to find a strategy that will minimize the expected reachability cost, but with no guarantees on worst-case behaviour. In this paper, we provide efficient methods for computing reachability strategies that will both ensure worst case time-bounds as well as provide (near-) minimal expected cost. Our method extends the synthesis algorithms of the synthesis tool Uppaal-Tiga with suitable adapted reinforcement learning techniques, that exhibits several orders of magnitude improvements w.r.t. previously known automated methods.",

author = "Alexandre David and Jensen, {Peter Gj{\o}l} and Larsen, {Kim Guldstrand} and Axel Legay and Didier Lime and S{\o}rensen, {Mathias Grund} and Taankvist, {Jakob Haahr}",

year = "2014",

doi = "10.1007/978-3-319-11936-6_10",

language = "English",

isbn = "978-3-319-11935-9",

volume = "8837",

series = "Lecture Notes in Computer Science",

publisher = "Springer Publishing Company",

pages = "129--145",

editor = "Franck Cassez and Jean-Fran{\c c}ois Raskin",

booktitle = "Automated Technology for Verification and Analysis",

address = "United States",

note = "null ; Conference date: 03-11-2012 Through 07-11-2014",

}