Navigational hierarchies of regular languages

TL;DR

This work studies star-free languages through navigational hierarchies formed by the TL operator, providing a parallel to classical concatenation hierarchies. It defines TL(C) as a unary-temporal-logic based expansion of a basis C and shows that for any C, the levels TL_n(C) contain the levels BPol_n(C) and together they exhaust the star-free closure SF(C). The paper gives deep results for group-based bases G and G+, establishing strictness and intertwining between navigational and concatenation hierarchies, and develops a comprehensive framework of rating maps and optimal imprints to decide covering and, via transfer theorems, membership and separation for key bases such as ST and DD. It also proves decidability results for TL_2(ST) and, via enrichment, TL_3(ST) membership, with consequences for related bases like MOD, AMT, GR, and TL_2(DD). The combination of algebraic and logical methods yields new decidability results and tight comparisons between hierarchies, with optimal imprint techniques enabling systematic treatment of covering problems.

Abstract

We study the class of star-free languages. A long-standing goal is to classify them by the complexity of their descriptions. The most influential research effort involves concatenation hierarchies, which measure alternations between ``complement'' and ``union plus concatenation''. We explore alternative hierarchies that also stratify star-free languages. They are built with an operator $C\mapsto TL(C)$. From an input class $C$, it produces a larger one $TL(C)$, consisting of all languages definable in a variant of unary temporal logic, where temporal modalities depend on $C$. Level $n$ in the navigational hierarchy of basis $C$ is constructed by applying this operator $n$ times to $C$. As bases $G$, we focus on group languages and natural extensions thereof, denoted $G^+$. We prove that the navigational hierarchies of bases $G$ and $G^+$ are strictly intertwined and conduct a thorough investigation of their relationships with concatenation hierarchies. We also look at two problems on classes of languages: membership (decide if a language is in the class) and separation (decide, for two languages $L_1,L_2$, if there is a language $K$ in the class with $L_1\subseteq K$ and $L_2\cap K=\emptyset$). We prove that if separation is decidable for $G$, then so is membership for level \emph{two} in the navigational hierarchies of bases $G$ and $G^+$. We take a look at the trivial class $ST=\{\emptyset,A^*\}$. For the bases $ST$ and $ST^+$, the levels \emph{one} are standard variants of unary temporal logic. The levels \emph{two} correspond to variants of two-variable logic, investigated recently by Krebs, Lodaya, Pandya and Straubing. We solve one of their conjectures. We also prove that for these two bases, level \emph{two} has decidable \emph{separation}. Combined with earlier results on the operator $C\mapsto TL(C)$, this implies that level \emph{three} has decidable membership.

Figures (3)

• Figure 1: Comparison of the two hierarchies (bases $\mathcal{G}$ or $\mathcal{G}\xspace^{+}$)
• Figure 2: The four kinds of levels in a concatenation hierarchy.
• Figure 3: Level 2 (filled) in a navigational hierarchy (bases $\mathcal{G}$/$\mathcal{G}\xspace^{+}$)

Theorems & Definitions (107)

• remark 1
• remark 2
• Lemma 0
• Proposition 0
• Lemma 0
• Lemma 0
• Theorem 1
• remark 3
• Theorem 2
• Corollary 2