Ehrenfeucht-Fraisse Games on Omega-Terms
Ehrenfeucht-Fraisse Games on Omega-Terms
复制标题
欧米茄条款上的 Ehrenfeucht-Fraisse Games
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Manfred Kufleitner
中科院分区：
文献类型：
--
作者：
Martin Huschenbett;Manfred Kufleitner
词上的一阶逻辑片段通常可以用有限幺半群或有限半群来刻画。通常，这些代数描述产生的问题，是否一个给定的正则语言是在一个特定的片段可定义的可判定性。一个有效的代数特征可以从所谓的Ω项的恒等式中得到。为了证明一个给定的片段满足某些Ω项的恒等式，我们可以对Ω项的词实例使用Escherichfeucht-Fraisse游戏。由此产生的证明往往需要大量的簿记有关的常数。在本文中，我们介绍了Escherichfeucht-Fraisse对策的ω-条款。为此，我们为每个omega项分配一个标记的线性顺序。我们的主要定理表明，一个给定的片段满足一些单位的欧米茄条款，当且仅当复制者有一个获胜的策略，为游戏的线性订单。这样可以避免记账。作为我们主要结果的一个应用，我们证明了在指数时间内可以判定所有非周期幺半群是否满足某个给定的Ω项恒等式，从而改进了McCammond（Int. J. Algebra Comput.，2001年）。
Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment satisfies some identity of omega-terms, one can use Ehrenfeucht-Fraisse games on word instances of the omega-terms. The resulting proofs often require a significant amount of book-keeping with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraisse games on omega-terms. To this end we assign a labeled linear order to every omega-term. Our main theorem shows that a given fragment satisfies some identity of omega-terms if and only if Duplicator has a winning strategy for the game on the resulting linear orders. This allows to avoid the book-keeping. As an application of our main result, we show that one can decide in exponential time whether all aperiodic monoids satisfy some given identity of omega-terms, thereby improving a result of McCammond (Int. J. Algebra Comput., 2001).