Solving parity games on integer vectors

DOI10.1007/978-3-642-40184-8_9MaRDI QIDQ2842100zbMATH OpenOpenAlexFDO

Authors Arnaud Sangnier, Jeremy Sproston, Parosh A. Abdulla, Richard M. Mayr

Publication date 12 August 2013

Published in CONCUR 2013 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.2806

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Games involving graphs (91A43) Applications of game theory (91A80)

Abstract: We consider parity games on infinite graphs where configurations are represented by control-states and integer vectors. This framework subsumes two classic game problems: parity games on vector addition systems with states (vass) and multidimensional energy parity games. We show that the multidimensional energy parity game problem is inter-reducible with a subclass of single-sided parity games on vass where just one player can modify the integer counters and the opponent can only change control-states. Our main result is that the minimal elements of the upward-closed winning set of these single-sided parity games on vass are computable. This implies that the Pareto frontier of the minimal initial credit needed to win multidimensional energy parity games is also computable, solving an open question from the literature. Moreover, our main result implies the decidability of weak simulation preorder/equivalence between finite-state systems and vass, and the decidability of model checking vass with a large fragment of the modal mu-calculus.

Recommendations

• On reachability-related games on vector addition systems with states
• Energy parity games
• Energy parity games
• Alternating vector addition systems with states
• Solving counter parity games

Cited in

(20)

• On reachability-related games on vector addition systems with states
• On decidability and complexity of low-dimensional robot games
• Simple stochastic games with almost-sure energy-parity objectives are in NP and conp
• Strategic reasoning with a bounded number of resources: the quest for tractability
• Qualitative analysis of VASS-induced MDPs
• Concurrent games on VASS with inhibition
• Alternating vector addition systems with states
• Fixed-dimensional energy games are in pseudo-polynomial time
• Solving parity games by a reduction to SAT
• scientific article; zbMATH DE number 7356850 (Why is no real title available?)
• State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems
• Solving Parity Games on the GPU
• A Multi-Core Solver for Parity Games
• Energy mean-payoff games
• On the complexity of resource-bounded logics
• Realizability problem for constraint LTL
• A matrix-based approach to parity games
• Process equivalence problems as energy games
• Round- and context-bounded control of dynamic pushdown systems
• Galois energy games: to solve all kinds of quantitative reachability problems

This page was built for publication: Solving parity games on integer vectors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2842100)