@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 = "Automated Technology for Verification and Analysis ; Conference date: 03-11-2012 Through 07-11-2014",
}