Weighted automata on infinite words in the context of Attacker-Defender games

TL;DR

This paper introduces a new language-theoretic result for weighted automata on infinite words and applies it to prove undecidability in various Attacker-Defender games and related mathematical games.

Contribution

It presents a novel encoding of weighted automata results into Attacker-Defender games and establishes undecidability for several low-dimensional game problems.

Findings

New language-theoretic result for weighted automata on infinite words

Encoding of automata results into Attacker-Defender game framework

Undecidability results for vector reachability, word, and braid games

Abstract

We consider infinite-state Attacker-Defender games with reachability objectives. The results of the paper are twofold. Firstly we prove a new language-theoretic result for weighted automata on infinite words and show its encoding into the framework of Attacker-Defender games. Secondly we use this novel concept to prove undecidability for checking existence of a winning strategy in several low-dimensional mathematical games including vector reachability games, word games and braid games.