Courcelle's theorem - A game-theoretic approach
Courcelle's theorem - A game-theoretic approach
复制标题
DOI：
10.1016/j.disopt.2011.06.001
复制
发表时间：
2011-04
期刊：
影响因子：
--
通讯作者：
Joachim Kneis;Alexander Langer;P. Rossmanith
中科院分区：
文献类型：
--
作者：
Joachim Kneis;Alexander Langer;P. Rossmanith
库塞勒定理指出，在一元二阶逻辑中可定义的每个问题都可以在线性时间内在有界树宽的结构上得到解决，例如，通过构造一个树自动机来识别或拒绝结构的树分解。现有的优化软件（如莫纳工具）可以用来构建相应的树自动机，对于有界树宽，树自动机的大小是恒定的。不幸的是，所涉及的常数可能会变得非常大-每个量词的交替都需要为自动机构造幂集。这里，所需的空间在实际应用中可能成为问题。在本文中，我们提出了一种新的，直接的方法基于模型检测游戏，它避免了昂贵的权力集的建设。实现的实验是有希望的，我们可以解决自动机理论方法在实践中失败的图上的问题。
Courcelle’s theorem states that every problem definable in Monadic Second-Order logic can be solved in linear time on structures of bounded treewidth, for example, by constructing a tree automaton that recognizes or rejects a tree decomposition of the structure. Existing, optimized software like the MONA tool can be used to build the corresponding tree automata, which for bounded treewidth are of constant size. Unfortunately, the constants involved can become extremely large—every quantifier alternation requires a power set construction for the automaton. Here, the required space can become a problem in practical applications. In this paper, we present a novel, direct approach based on model checking games, which avoids the expensive power set construction. Experiments with an implementation are promising, and we can solve problems on graphs where the automata-theoretic approach fails in practice.