efomega-stacs2014.final.pdf (531.04 kB)
Download file

Ehrenfeucht-Fraisse games on omega-terms

Download (531.04 kB)
conference contribution
posted on 23.02.2018, 14:45 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, LIPIcs

Volume

25

Pages

374 - 385

Citation

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 Informatics

Version

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

2014

Notes

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

9783939897651

ISSN

1868-8969

Book series

Leibniz International Proceedings in Informatics, LIPIcs;25

Language

en