Navigational hierarchies of regular languages

We study a celebrated class of regular languages: 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 (and extensions thereof). They are built with an operator ${\mathcal{C}} \mapsto {\text{TL}}\left({\mathcal{C}}\right)$. It takes a class of languages ${\mathcal{C}}$ as input, and produces a larger one ${\text{TL}}\left({\mathcal{C}}\right)$, consisting of all languages definable in a variant of unary temporal logic, where the future/past modalities depend on ${\mathcal{C}}$. Level n in the navigational hierarchy of basis ${\mathcal{C}}$ is then constructed by applying this operator n times to ${\mathcal{C}}$.As bases ${\mathcal{G}}$, we focus on group languages and natural extensions thereof, denoted ${{\mathcal{G}}^ + }$. We prove that the navigational hierarchies of bases ${\mathcal{G}}$ and ${{\mathcal{G}}^ + }$ are strictly intertwined and we conduct a thorough investigation of their relationships with their concatenation hierarchy counterparts. We also look at two standard problems on classes of languages: membership (decide if a language is in the class) and separation (decide, for two languages L1,L2, if there is a language K in the class with L1⊆ K and L2∩K = ∅). We prove that if separation is decidable for ${\mathcal{G}}$, then so is membership for level two in the navigational hierarchies of bases ${\mathcal{G}}$ and ${{\mathcal{G}}^ + }$.We take a closer look at the trivial class ST = ∅,A*. For the bases ST and ST+, the levels one are the standard variants of unary temporal logic. The levels 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 two has decidable separation. Combined with earlier results on the operator ${\mathcal{C}} \mapsto {\text{TL}}\left({\mathcal{C}}\right)$, this implies that level three has decidable membership.