efomega-stacs2014.final.pdf (531.04 kB)
Ehrenfeucht-Fraisse games on omega-terms
conference contribution
posted on 2018-02-23, 14:45 authored by Martin Huschenbett, Manfred Kufleitner© Martin Huschenbett and Manfred Kufleitner. 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-Fraïssé games on word instances of the omega-terms. The resulting proofs often require a significant amount of bookkeeping with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraïssé 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).
Funding
M.K. was supported by the German Research Foundation (DFG) under grant DI 435/5-1 and by the Technische Universitat Munchen, Germany.
History
School
- Science
Department
- Computer Science
Published in
Leibniz International Proceedings in Informatics, LIPIcsVolume
25Pages
374 - 385Citation
HUSCHENBETT, M. and KUFLEITNER, M., 2014. Ehrenfeucht-Fraisse games on omega-terms. Presented at the 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), Lyon, France, Mar 5-8th. pp. 374-385.Publisher
Schloss Dagstuhl – Leibniz Center for InformaticsVersion
- VoR (Version of Record)
Publisher statement
This work is made available according to the conditions of the Creative Commons Attribution 4.0 International (CC BY 4.0) licence. Full details of this licence are available at: http://creativecommons.org/licenses/ by/4.0/Publication date
2014Notes
This is an Open Access Article. It is published by Schloss Dagstuhl – Leibniz Center for Informatics under the Creative Commons Attribution 4.0 Unported Licence (CC BY). Full details of this licence are available at: http://creativecommons.org/licenses/by/4.0/ISBN
9783939897651ISSN
1868-8969Publisher version
Book series
Leibniz International Proceedings in Informatics, LIPIcs;25Language
- en