Playing with repetitions in data words using energy games.

*(English)*Zbl 07226003Summary: 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.

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.

##### References:

[1] | P. A. Abdulla, R. Mayr, A. Sangnier, and J. Sproston. Solving parity games on integer vectors. In CONCUR 2013, volume 8052 ofLNCS, pages 106-120. Springer Berlin Heidelberg, 2013. · Zbl 1390.68452 |

[2] | Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien D’orso. Monotonic and downward closed games. Journal of Logic and Computation, 18(1):153-169, 2008. · Zbl 1133.68042 |

[3] | S. Abriola, D. Figueira, and S. Figueira. Logics of repeating values on data trees and branching counter systems. InFOSSACS’17, volume 10203 ofLecture Notes in Computer Science, pages 196-212, 2017. · Zbl 06720991 |

[4] | B´eatrice B´erard, Serge Haddad, Mathieu Sassolas, and Nathalie Sznajder. Concurrent games on VASS with inhibition. In Maciej Koutny and Irek Ulidowski, editors,Proceedings of the 23rd International · Zbl 1364.68275 |

[5] | M. Boja´nczyk, C. David, A. Muscholl, Th. Schwentick, and L. Segoufin. Two-variable logic on data words.ACM Transactions on Computational Logic, 12(4):27, 2011. |

[6] | Tom´aˇs Br´azdil, Petr Janˇcar, and Anton´ın Kuˇcera.Reachability Games on Extended Vector Addition Systems with States, pages 478-489. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. |

[7] | Krishnendu Chatterjee, Mickael Randour, and Jean-Fran¸cois Raskin. Strategy synthesis for multidimensional quantitative objectives.Acta Informatica, 51(3):129-163, June 2014. · Zbl 1360.68208 |

[8] | A. Church. Logic, arithmetic and automata. InProceedings of the international congress of mathematicians, volume 1962, pages 23-35, 1962. |

[9] | T. Colcombet, M. Jurdzi´nski, R. Lazi´c, and S. Schmitz. Perfect half space games. InLICS 2017, pages 1-11, 2017. |

[10] | S. Demri, D. D’Souza, and R. Gascon. Temporal logics of repeating values.Journal of Logic and Computation, 22(5):1059-1096, 2012. · Zbl 1279.68203 |

[11] | S. Demri, D. Figueira, and M. Praveen. Reasoning about Data Repetitions with Counter Systems.Logical Methods in Computer Science, Volume 12, Issue 3:1-55, Aug 2016. · Zbl 1448.68339 |

[12] | S. Demri and R. Lazi´c. LTL with the freeze quantifier and register automata.ACM Transactions on Computational Logic, 10(3), 2009. · Zbl 1351.68158 |

[13] | D. Figueira. A decidable two-way logic on data words. InLICS’11, pages 365-374. IEEE, 2011. |

[14] | Diego Figueira and M. Praveen. Playing with repetitions in data words using energy games. InLICS’18, pages 404-413. ACM, 2018. |

[15] | A. Kara, Th. Schwentick, and Th. Zeume. Temporal logics on words with multiple data values. In FST&TCS’10, pages 481-492. LZI, 2010. · Zbl 1245.03021 |

[16] | Richard Mayr. Undecidable problems in unreliable computations.Theoretical Computer Science, 297(1):337 - 354, 2003. Latin American Theoretical Informatics. · Zbl 1044.68119 |

[17] | M. L. Minsky. Recursive unsolvability of post’s problem of ‘tag’ and other topics in the theory of turing machines.Annals of Mathematics, 74:437-455, 1961. · Zbl 0105.00802 |

[18] | F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets.ACM Transactions on Computational Logic, 5(3):403-435, 2004. · Zbl 1367.68175 |

[19] | A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module.Automata, Languages and Programming, pages 652-671, 1989. |

[20] | J.-F. Raskin, M. Samuelides, and L. Van Begin. Games for counting abstractions.Electronic Notes in Theoretical Computer Science, 128(6):69 - 85, 2005. Proceedings of the Fouth International Workshop · Zbl 1272.91014 |

[21] | L. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.