A Decremental Algorithm for Fair Büchi Games
摘要
This paper provides the first decremental algorithm for fair Büchi games. It efficiently recalculates the winning region under the deletion of live edges in the underlying game graph. Our algorithm addresses the unique challenges posed by fair Büchi games such as exponential-memory strategies and the non-monotonicity of the winning region under edge deletion. This prevents a straight forward extension of dynamic algorithms from (normal) Büchi games, in particular Jurdziński’s small progress measures, on which these algorithms rely. The main contribution of this paper is the definition of a specialized (one-digit) progress measure for fair Büchi games and its correctness proof. We further derive a decremental algorithm for fair Büchi games using a fixed-point calculation entailed by this progress measure. We show that the (non-optimized) prototype implementation of our decremental algorithm outperforms an (optimized) fair Büchi game solver on a large class of benchmarks. By this, our work not only expands the scope of dynamic algorithms but also underscores the benefit of tailored solutions for specific game structures such as fair Büchi games.