Diego Figueira ; Anirban Majumdar ; M. Praveen - Playing with Repetitions in Data Words Using Energy Games

lmcs:4898 - Logical Methods in Computer Science, July 3, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:1)2020
Playing with Repetitions in Data Words Using Energy GamesArticle

Authors: Diego Figueira ORCID; Anirban Majumdar ; M. Praveen

    We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating multi-attributed data words. The winner of the game is specified by formulas in the Logic of Repeating Values, which can reason about repetitions of data values in infinite data words. We prove that it is undecidable to check if one of the players has a winning strategy, even in very restrictive settings. However, we prove that if one of the players is restricted to choose valuations ranging over the Boolean domain, the games are effectively equivalent to single-sided games on vector addition systems with states (in which one of the players can change control states but cannot change counter values), known to be decidable and effectively equivalent to energy games. Previous works have shown that the satisfiability problem for various variants of the logic of repeating values is equivalent to the reachability and coverability problems in vector addition systems. Our results raise this connection to the level of games, augmenting further the associations between logics on data words and counter systems.


    Volume: Volume 16, Issue 3
    Published on: July 3, 2020
    Accepted on: May 12, 2020
    Submitted on: October 19, 2018
    Keywords: Computer Science - Logic in Computer Science,F.1.1,F.3.1
    Funding:
      Source : OpenAIRE Graph
    • IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS; Funder: French National Research Agency (ANR); Code: ANR-17-CE40-0028

    Consultation statistics

    This page has been seen 1335 times.
    This article's PDF has been downloaded 250 times.