Navigational hierarchies of regular languages

TL;DR

This paper introduces alternative hierarchies for star-free languages using a temporal logic-based operator, explores their relationships with concatenation hierarchies, and proves decidability results for membership and separation problems.

Contribution

It develops new navigational hierarchies for star-free languages, analyzes their properties, and establishes decidability results for key language class problems.

Findings

Navigational hierarchies are strictly intertwined with concatenation hierarchies.

Decidability of separation implies decidability of membership at level two.

Level two for certain classes corresponds to variants of two-variable logic.

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.