Non-deterministic asynchronous automata games and their undecidability

TL;DR

This paper introduces ATS games, a new model of distributed games on asynchronous systems, and proves their undecidability, highlighting fundamental limits in automated strategy synthesis for such systems.

Contribution

The paper defines ATS games on non-deterministic asynchronous transition systems and proves their undecidability, establishing a key theoretical limitation in distributed game analysis.

Findings

ATS games are equivalent to asynchronous games.

Deciding the existence of a winning strategy is undecidable.

The model captures distributed systems working on Mazurkiewicz traces.

Abstract

We propose a new model of a distributed game, called an ATS game, which is played on a non-deterministic asynchronous transition system -- a natural distributed finite-state device working on Mazurkiewicz traces. This new partial-information game is played between an environment and a distributed system comprising multiple processes. A distributed strategy uses causal past to make the next move. The key algorithmic question is to solve the game, that is, to decide the existence of a distributed winning strategy. It turns out ATS games are equivalent to asynchronous games, which are known to be undecidable. We prove that ATS games are undecidable in this article.