Game Characterizations of Timed Relations for Timed Automata Processes

In this work, we design the game semantics for timed equivalences and preorders of timed processes. The timed games corresponding to the various timed relations form a hierarchy. These games are similar to Stirling’s bisimulation games. If it is the case that the existence of a winning strategy for the defender in a game ${\mathcal{G}}_1$ implies that there exists a winning strategy for the defender in another game ${\mathcal{G}}_2$, then the relation that corresponds to ${\mathcal{G}}_1$ is stronger than the relation corresponding to ${\mathcal{G}}_2$. The game hierarchy also throws light into several timed relations that are not considered in this paper.