Regular Tree Languages Definable in FO and in FOmod

We consider regular languages of labeled trees. We give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of the locally threshold testable languages on strings. We...

Full description

Bibliographic Details
Main Authors: Benedikt, M, Segoufin, L
Format: Journal article
Language:English
Published: 2009
Description
Summary:We consider regular languages of labeled trees. We give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of the locally threshold testable languages on strings. We show that this characterization yields a decision procedure for determining whether a regular tree language is first-order definable: The procedure is polynomial time in the minimal automaton presenting the regular language. We also provide an algorithm for deciding whether a regular language is definable in first-order logic supplemented with modular quantifiers. © 2009 ACM.