Expected Reachability-Time Games

TL;DR

This paper investigates two-player zero-sum games on probabilistic timed automata with the goal of analyzing expected reachability times, revealing their non-determined nature and establishing decidability within NEXPTIME complexity.

Contribution

It introduces a novel class of reachability-time games on probabilistic timed automata, analyzing their properties and decision problems, including non-determinacy and complexity bounds.

Findings

Games are not determined.

Decidable in NEXPTIME ∩ co-NEXPTIME.

Decision problems for upper and lower values are solvable.

Abstract

Probabilistic timed automata are a suitable formalism to model systems with real-time, nondeterministic and probabilistic behaviour. We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. The two players---called player Min and player Max---compete by proposing timed moves simultaneously and the move with a shorter delay is performed. The first player attempts to minimise the given objective while the second tries to maximise the objective. We observe that these games are not determined, and study decision problems related to computing the upper and lower values, showing that the problems are decidable and lie in the complexity class NEXPTIME $\cap$ co-NEXPTIME.