On Time with Minimal Expected Cost!

Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, Jakob Haahr Taankvist

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

34 Citationer (Scopus)

Abstrakt

(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.
OriginalsprogEngelsk
TitelAutomated Technology for Verification and Analysis
RedaktørerFranck Cassez, Jean-François Raskin
Antal sider16
Vol/bind8837
ForlagSpringer Publishing Company
Publikationsdato2014
Sider129-145
ISBN (Trykt)978-3-319-11935-9
ISBN (Elektronisk)978-3-319-11936-6
DOI
StatusUdgivet - 2014
BegivenhedAutomated Technology for Verification and Analysis - Sydney, NSW, Australien
Varighed: 3 nov. 20127 nov. 2014

Konference

KonferenceAutomated Technology for Verification and Analysis
LandAustralien
BySydney, NSW
Periode03/11/201207/11/2014
NavnLecture Notes in Computer Science
ISSN0302-9743

Citationsformater