On labeled birooted tree languages: Algebras, automata and logic

With an aim to developing expressive language theoretical tools applicable to inverse semigroup languages, that is, subsets of inverse semigroups, this paper explores the language theory of finite labeled birooted trees: Munn's birooted trees extended with vertex labeling. To this purpose, we define a notion of finite state birooted tree automata that simply extends finite state word automata semantics. This notion is shown to capture the class of languages that are definable in Monadic Second Order Logic and upward closed with respect to the natural order. Then, we derive from these automata the notion of quasi-recognizable languages, that is, languages recognizable by means of (adequate) premorphisms into finite (adequately) ordered monoids. This notion is shown to capture finite Boolean combinations of languages as above, a class that contains classical regular languages of finite (mono-rooted) trees. This contrasts with the known collapse of classical algebraic tools when applied to inverse semigroups.