Positionality in $Σ_0^2$ and a completeness result

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Ohlmann, Pierre, Skrzypczak, Michał
Format: Preprint
Published: 2023
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917461423554560
author Ohlmann, Pierre
Skrzypczak, Michał
author_facet Ohlmann, Pierre
Skrzypczak, Michał
contents We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in $Σ_0^2$ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Bchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective $W$ which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective $W'$ which is equivalent to $W$ over finite game graphs and positional over arbitrary game graphs.
format Preprint
id arxiv_https___arxiv_org_abs_2309_17022
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle Positionality in $Σ_0^2$ and a completeness result
Ohlmann, Pierre
Skrzypczak, Michał
Logic in Computer Science
We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in $Σ_0^2$ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Bchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective $W$ which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective $W'$ which is equivalent to $W$ over finite game graphs and positional over arbitrary game graphs.
title Positionality in $Σ_0^2$ and a completeness result
topic Logic in Computer Science
url https://arxiv.org/abs/2309.17022