Reachability Games on Extended Vector Addition Systems with States

TL;DR

This paper investigates reachability games on extended vector addition systems with states, identifying specific conditions under which the otherwise undecidable problem becomes decidable or tractable.

Contribution

The authors analyze the decidability of reachability games on extended vector addition systems with states, highlighting subcases with restricted counters or target sets that are computationally manageable.

Findings

Certain subcases are decidable and tractable

Decidability depends on restrictions on counters and target configurations

The general problem remains undecidable

Abstract

We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.