论文标题
与定性语义的交替树自动机
Alternating Tree Automata with Qualitative Semantics
论文作者
论文摘要
我们研究了无限二进制树上的定性语义交替的自动机：交替意味着两个相对的玩家构建了输入树的装饰，称为“奔跑”，而定性语义说，如果几乎所有运行的分支都接受了自动机的运行，则自动机的运行正在接受。在本文中，我们证明了与定性语义交替交替自动机的空虚问题的正面和负面结果。 积极的结果是对于Büchi接受条件而言，空虚问题的可决定性。我们方法的一个有趣的方面是，我们不会扩展经典的解决方案来解决交替自动机的空虚问题，该问题首先构建了等效的非确定性自动机。相反，我们直接构建了一个空虚的游戏，利用不完美的信息。 负面的结果是对于co-Büchi接受条件而言，空虚问题的不确定性。该结果有两个直接的后果：随着定性路径测量量量扩展了莫金二阶逻辑的不可证明性，以及对于非零语义的交流树自动机的空虚问题的不确定性，这是一种非零的语义，这是最近引入的交流树自动机的概率模型。
We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier, and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.
