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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Decremental Algorithm for Fair Büchi Games

  • Irmak Sağlam,
  • Anne-Kathrin Schmuck,
  • Munko Tsyrempilon

摘要

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.