Game Characterizations of Timed Relations for Timed Automata Processes

TL;DR

This paper develops game semantics for timed equivalences and preorders in timed automata, establishing a hierarchy of timed games similar to Stirling's bisimulation games, to analyze process relations.

Contribution

It introduces a hierarchy of timed game semantics for timed automata processes, providing a new framework to compare timed relations through game strategies.

Findings

Hierarchy of timed games for process relations

Relation strength inferred from defender's winning strategies

Insight into unconsidered timed relations

Abstract

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 ${\cal G}_1$ implies that there exists a winning strategy for the defender in another game ${\cal G}_2$, then the relation that corresponds to ${\cal G}_1$ is stronger than the relation corresponding to ${\cal G}_2$. The game hierarchy also throws light into several timed relations that are not considered in this paper.