自动机带有MSO图存储的Büchi-Elgot-Trakhtenbrot定理
摘要：介绍了MSO图存储类型，并称存储类型为MSO可表达的，如果它同构于某个MSO图存储类型。MSO图存储类型具有MSO可定义的图集合作为存储配置和存储转换。考虑具有MSO图存储的顺序自动机，并与每个这样的自动机相关联一个字符串语言（按照常规方式）和图语言；如果图表示给定输入字符串的正确存储配置序列，则该图被自动机接受。对于每个MSO图存储类型，定义了一个MSO逻辑，它是图上常规MSO逻辑的子集。证明了Büchi-Elgot-Trakhtenbrot定理，分别针对字符串情况和图情况。此外，证明了（i）每个MSO图传递可以用作MSO图存储类型中的存储转换，（ii）每个自动存储类型都是MSO可表达的，以及（iii）存储类型上的下推操作保持MSO可表达性的属性。因此，迭代下推存储类型是MSO可表达的。
作者：Joost Engelfriet and Heiko Vogler
论文ID：1905.00559
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22