Research: Reachability in Stochastic Timed Games

Advisor: S. Akshay and Krishna S.

Stochastic Timed Games (STG) naturally generalize both continuous-time Markov chains and timed automata. In Spring ‘18, We extended a known undecidability result on two player STGs to single player STGs. We proved that the quantitative reachability problem - the problem of existence of a strategy reaching a given target with probability at least r, is undecidable, by reducing from the non-halting problem of two counter machines. We worked on proving decidability of qualitative reachability for two players - reachability with probability 1.