2016/07/19 by S. Akshay, Akshay, S, Patricia Bouyer +7
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Reliability and Analysis Research
paper · pdf · doi:10.48550/arxiv.1607.05671
openalex publication_date 2016/07/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.