Parity Games on Temporal Graphs

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Austin, Pete, Bose, Sougata, Totzke, Patrick
Format: Preprint
Published: 2023
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866913212233940992
author Austin, Pete
Bose, Sougata
Totzke, Patrick
author_facet Austin, Pete
Bose, Sougata
Totzke, Patrick
contents Temporal graphs are a popular modelling mechanism for dynamic complex systems that extend ordinary graphs with discrete time. Simply put, time progresses one unit per step and the availability of edges can change with time. We consider the complexity of solving $ω$-regular games played on temporal graphs where the edge availability is ultimately periodic and fixed a priori. We show that solving parity games on temporal graphs is decidable in PSPACE, only assuming the edge predicate itself is in PSPACE. A matching lower bound already holds for what we call punctual reachability games on static graphs, where one player wants to reach the target at a given, binary encoded, point in time. We further study syntactic restrictions that imply more efficient procedures. In particular, if the edge predicate is in $P$ and is monotonically increasing for one player and decreasing for the other, then the complexity of solving games is only polynomially increased compared to static graphs.
format Preprint
id arxiv_https___arxiv_org_abs_2310_12701
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle Parity Games on Temporal Graphs
Austin, Pete
Bose, Sougata
Totzke, Patrick
Logic in Computer Science
Formal Languages and Automata Theory
Temporal graphs are a popular modelling mechanism for dynamic complex systems that extend ordinary graphs with discrete time. Simply put, time progresses one unit per step and the availability of edges can change with time. We consider the complexity of solving $ω$-regular games played on temporal graphs where the edge availability is ultimately periodic and fixed a priori. We show that solving parity games on temporal graphs is decidable in PSPACE, only assuming the edge predicate itself is in PSPACE. A matching lower bound already holds for what we call punctual reachability games on static graphs, where one player wants to reach the target at a given, binary encoded, point in time. We further study syntactic restrictions that imply more efficient procedures. In particular, if the edge predicate is in $P$ and is monotonically increasing for one player and decreasing for the other, then the complexity of solving games is only polynomially increased compared to static graphs.
title Parity Games on Temporal Graphs
topic Logic in Computer Science
Formal Languages and Automata Theory
url https://arxiv.org/abs/2310.12701