具有MSO图存储的自动机的Büchi-Elgot-Trakhtenbrot定理
形式语言与自动机理论
2023-06-22 v4
摘要
我们引入MSO图存储类型，并称一个存储类型为MSO可表达的，如果它同构于某个MSO图存储类型。MSO图存储类型以MSO可定义的图集合作为存储构型与存储变换。我们考虑具有MSO图存储的时序自动机，并为每个这样的自动机关联一个字符串语言（以通常方式）和一个图语言；若图表示给定输入字符串的正确存储构型序列，则该图被自动机接受。对每个MSO图存储类型，我们定义一种MSO逻辑，它是通常图上MSO逻辑的一个子集。我们证明了Büchi-Elgot-Trakhtenbrot定理，分别针对字符串情形与图情形。此外，我们证明：(i) 每个MSO图转导都可用作MSO图存储类型中的存储变换，(ii) 每个自动存储类型都是MSO可表达的，以及 (iii) 存储类型上的下推算子保持MSO可表达性。因此，迭代下推存储类型是MSO可表达的。
引用
@article{arxiv.1905.00559,
title = {A B\"uchi-Elgot-Trakhtenbrot theorem for automata with MSO graph storage},
author = {Joost Engelfriet and Heiko Vogler},
journal= {arXiv preprint arXiv:1905.00559},
year = {2023}
}