用于检查 MSO2 图属性的 Fly 自动机
计算机科学中的逻辑
2015-12-23 v2
摘要
一个更具描述性但过长的标题将是：构造fly自动机以检查由带边量词的单子二阶公式表达的、有界树宽的图的性质。此类性质简称为MSO2。Fly自动机(FA)在表示图的项上自底向上运行，并“即时(on the fly)”计算必要的状态和转移，而非查阅巨大且实际上不可实现的表。在先前工作中，我们构造了处理表示有界团宽图的项的FA，以检查其单子二阶(MSO)性质（由无量词边公式表达）。此处，我们调整这些FA以适用于关联图，从而能检查有界树宽图的MSO2性质。这是可能的，因为：(1)图的MSO2性质无非是其关联图的MSO性质；(2)图的关联图的团宽在其树宽方面呈线性有界。我们的构造实际上是可实现且可用的。我们在此视角下详述自动机的具体构造。
引用
@article{arxiv.1511.08605,
title = {Fly-automata for checking MSO 2 graph properties},
author = {Bruno Courcelle},
journal= {arXiv preprint arXiv:1511.08605},
year = {2015}
}
备注
Submitted for publication in December 2015