Logic and games on automatic structures. Playing with quantifiers and decompositions (Q555655)

Omega-automatic structures are used for the storage and algorithmic manipulation of infinite structures in a finite way, with elements represented by infinite words over a finite alphabet and relations represented by synchronous omega-regular automata on tuples of such words, and enjoy desirable algorithmic properties, such as having a decidable first-order theory. The author extends the game-based algorithmic approach to first-order logic by extending FOL by a regular game quantifier on automatic presentations, corresponding to the step-by-step construction of the word for an element by two players, and which is shown to preserve regularity. The model checking problem for FOL with the regular game quantifier is then reduced to solving a multiplayer game with the players forming two coalitions and with hierarchical imperfect information. Furthermore it is shown that the cardinality and modulo counting generalized quantifiers preserve regularity on all automatic structures. Then, several classes of games with winning conditions with infinitely many priorities and the memory sufficient for winning strategies are considered using variants of latest appearance records and Zielonka trees. Finally, the second-order cardinality quantifiers in monadic second-order logic over countable linear orders and over trees are investigated and it is shown that they may be effectively eliminated.