Playing with Repetitions in Data Words Using Energy Games

摘要

We introduce two-player games which build words over infinite alphabets, andwe study the problem of checking the existence of winning strategies. Thesegames are played by two players, who take turns in choosing valuations forvariables ranging over an infinite data domain, thus generatingmulti-attributed data words. The winner of the game is specified by formulas inthe Logic of Repeating Values, which can reason about repetitions of datavalues in infinite data words. We prove that it is undecidable to check if oneof the players has a winning strategy, even in very restrictive settings.However, we prove that if one of the players is restricted to choose valuationsranging over the Boolean domain, the games are effectively equivalent tosingle-sided games on vector addition systems with states (in which one of theplayers can change control states but cannot change counter values), known tobe decidable and effectively equivalent to energy games. Previous works have shown that the satisfiability problem for variousvariants of the logic of repeating values is equivalent to the reachability andcoverability problems in vector addition systems. Our results raise thisconnection to the level of games, augmenting further the associations betweenlogics on data words and counter systems.