2026-07-22T07:05:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6498 2024-03-06T10:38:14Z ddc:004 open_access

Stochastic Timed Games Revisited Akshay, S. Bouyer, Patricia Krishna, Shankara Narayanan Manasa, Lakshmi Trivedi, Ashutosh timed automata stochastic games two-counter machines Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players - 2, 1, or 0 - subclasses of stochastic timed games are often classified as 2 1/2-player, 1 1/2-player, and 1/2-player games where the 1/2 symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that 1 1/2-player one-clock STGs are decidable for qualitative objectives, and that 2 1/2-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for 1 1/2 player four-clock STGs, and even under the time-bounded restriction for 2 1/2-player five-clock STGs. We also obtain a class of 1 1/2, 2 1/2 player STGs for which the quantitative reachability problem is decidable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik S. Akshay and Patricia Bouyer and Shankara Narayanan Krishna and Lakshmi Manasa and Ashutosh Trivedi 2016 Is Part Of LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2016.8 urn:nbn:de:0030-drops-64985 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.8 eng https://creativecommons.org/licenses/by/3.0/legalcode