Nicolas Markey

Abstract

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations.

We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in coNP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.

@inproceedings{gandalf2019-HMR,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
                         Raha, Ritam},
  title =               {Reachability games with relaxed energy constraints},
  editor =              {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c
                         c}ois},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {G}ames, {A}utomata, {L}ogics and
                         {F}ormal {V}erification ({GandALF}'19)},
  acronym =             {{GandALF}'19},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {305},
  pages =               {17-33},
  year =                {2019},
  month =               sep,
  doi =                 {10.4204/EPTCS.305.2},
  abstract =            {We study games with reachability objectives under
                         energy constraints. We first prove that under strict
                         energy constraints (either only lower-bound
                         constraint or interval constraint), those games are
                         \textsf{LOGSPACE}-equivalent to energy games with
                         the same energy constraints but without reachability
                         objective (i.e., for infinite runs). We then
                         consider two kinds of relaxations of the upper-bound
                         constraints (while keeping the lower-bound
                         constraint strict): in the first one, called
                         \emph{weak upper bound}, the upper bound is
                         \emph{absorbing}, in the sense that it allows
                         receiving more energy when the upper bound is
                         already reached, but the extra energy will not be
                         stored; in~the second~one, we~allow for
                         \emph{temporary violations} of the upper bound,
                         imposing limits on the number or on the amount of
                         violations.\par We prove that when considering weak
                         upper bound, reachability objectives require memory,
                         but can still be solved in polynomial-time for
                         one-player arenas; we prove that they are in
                         \textsf{coNP} in the two-player setting. Allowing
                         for bounded violations makes the problem
                         \textsf{PSPACE}-complete for one-player arenas and
                         \textsf{EXPTIME}-complete for two players.},
}