The memory of $ω$-regular and BC($Σ_2^0$) objectives

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Casares, Antonio, Ohlmann, Pierre
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914622301274112
author Casares, Antonio
Ohlmann, Pierre
author_facet Casares, Antonio
Ohlmann, Pierre
contents In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.
format Preprint
id arxiv_https___arxiv_org_abs_2502_05840
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle The memory of $ω$-regular and BC($Σ_2^0$) objectives
Casares, Antonio
Ohlmann, Pierre
Logic in Computer Science
Formal Languages and Automata Theory
68Q45
F.4.3
In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.
title The memory of $ω$-regular and BC($Σ_2^0$) objectives
topic Logic in Computer Science
Formal Languages and Automata Theory
68Q45
F.4.3
url https://arxiv.org/abs/2502.05840