Omega-项上的 Ehrenfeucht-Fraisse 博弈
形式语言与自动机理论
2013-10-14 v1 计算机科学中的逻辑
群论
摘要
词上的一阶逻辑片段通常可以用有限幺半群或有限半群来刻画。通常，这些代数描述能够判定给定的正则语言是否可在特定片段中定义的问题。有效的代数刻画可以从所谓的 omega-项的恒等式中获得。为了证明给定片段满足某个 omega-项恒等式，可以在 omega-项的词实例上使用 Ehrenfeucht-Fraisse 博弈。由此产生的证明通常需要对涉及的常数进行大量的记录工作。在本文中，我们引入了 omega-项上的 Ehrenfeucht-Fraisse 博弈。为此，我们为每个 omega-项分配一个带标号的线性序。我们的主要定理表明，给定片段满足某个 omega-项恒等式，当且仅当 Duplicator 在所得线性序的博弈中具有获胜策略。这使得可以避免记录工作。作为我们主要结果的一个应用，我们证明了可以在指数时间内判定所有非周期幺半群是否满足某个给定的 omega-项恒等式，从而改进了 McCammond (Int. J. Algebra Comput., 2001) 的结果。
引用
@article{arxiv.1310.3195,
title = {Ehrenfeucht-Fraisse Games on Omega-Terms},
author = {Martin Huschenbett and Manfred Kufleitner},
journal= {arXiv preprint arXiv:1310.3195},
year = {2013}
}