Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata
arxiv(2024)
摘要
Our main technical contribution is a polynomial-time determinisation
procedure for history-deterministic Büchi automata, which settles an open
question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is
the lookahead game, which is a variant of Bagnol and Kuperberg's token game, in
which Adam is given a fixed lookahead. We prove that the lookahead game is
equivalent to the 1-token game. This allows us to show that the 1-token game
characterises history-determinism for semantically-deterministic Büchi
automata, which paves the way to our polynomial-time determinisation procedure.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要