有限与无限字上自动机的 FO2 量词交替层级的判定
形式语言与自动机理论
2021-09-02 v3 计算机科学中的逻辑
摘要
我们考虑二变量一阶逻辑 及其在有限字与无限字上的量词交替层级。我们的主要结果是针对确定性自动机（有限字）和 Carton-Michel 自动机（无限字）的禁戒模式。为了给出简洁的模式，我们允许在有限图的路径上使用子字。这一概念被形式化为子字模式（subword-patterns）。对于某些类型的子字模式，存在一个非确定性对数空间算法来判定其在给定自动机中的存在或缺失。特别地，这导出了用于判定 量词交替层级各层级的 算法。这适用于有限字与无限字上的完整层级与半层级。此外，我们证明这些问题是 -困难的，因此是 -完全的。
引用
@article{arxiv.2105.09291,
title = {Deciding FO2 Alternation for Automata over Finite and Infinite Words},
author = {Viktor Henriksson and Manfred Kufleitner},
journal= {arXiv preprint arXiv:2105.09291},
year = {2021}
}