Perfect Half-Space Games

• Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Main Authors: Colcombet, Thomas, Jurdzinski, Marcin, Lazić, Ranko, Schmitz, Sylvain
• Other Authors: Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Centre for Discrete Mathematics and its Applications Warwick (DIMAP), University of Warwick Coventry, Department of Computer Science Warwick, Laboratoire Spécification et Vérification Cachan (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), EPSRC grant EP/M011801/1, EPSRC grant EP/P020992/1, European Project: 259454,EC:FP7:ERC,ERC-2010-StG_20091028,GALE(2011)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT]; [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Iceland
• Online Access: https://hal.archives-ouvertes.fr/hal-01633355; https://doi.org/10.1109/LICS.2017.8005105

International audience We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi-dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2-EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary.