Temporal Hierarchies of Regular Languages: How We Classified Languages

Table of Links

Abstract and 1 Introduction

2 Preliminaries

3 Temporal Hierarchies

4 Rating Maps

5 Optimal Imprints for TL(AT)

6 Conclusion and References

Appendix A. Appendix to Section 2

Appendix B. Appendix to Section 3

Appendix C. Appendix to Section 4

Appendix D. Appendix to Section 5

Abstract

We classify the regular languages using an operator C 7→ TL(C). For each input class of languages C, it builds a larger class TL(C) consisting of all languages definable in a variant of unary temporal logic whose future/past modalities depend on C. This defines the temporal hierarchy of basis C: level n is built by applying this operator n times to C. This hierarchy is closely related to another one, the concatenation hierarchy of basis C. In particular, the union of all levels in both hierarchies is the same.

We focus on bases G of group languages and natural extensions thereof, denoted G +. We prove that the temporal hierarchies of bases G and G + are strictly intertwined, and we compare them to the corresponding concatenation hierarchies. Furthermore, we look at two standard problems on classes of languages: membership (decide if an input language is in the class) and separation (decide, for two input regular 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 G, then so is membership for level two in the temporal hierarchies of bases G and G +. Moreover, we take a closer look at the case where G is the trivial class ST = {∅, A∗}. The levels one in the hierarchies of bases ST and ST+ are the standard variants of unary temporal logic while the levels two were considered recently using alternate definitions. We prove that for these two bases, level two has decidable separation. Combined with earlier results about the operator G 7→ TL(G), this implies that the levels three have decidable membership.

1. Introduction

Context. This paper addresses a fundamental question in automata theory: understanding the formalisms used to describe regular languages. A flagship example is the class of star-free languages. These are languages that can be defined by a regular expression without Kleene star, but where complement is allowed. A striking feature of this class is its robustness. McNaughton and Papert [19] proved that star-free languages are those that can be described in first-order logic FO(<) and Kamp [11] proved that FO(<) has the same expressiveness as linear time temporal logic LTL. Also, Sch¨utzenberger [35] proved that membership is decidable for the star-free languages: given as input a regular language, one can decide if it is star-free. This led Brzozowski and Cohen [4] to define a natural classification of the star-free languages according to the difficulty of expressing them: the dot-depth hierarchy.

This robustness justifies to investigate membership for individual levels. It is, however, a difficult problem. For example, in the dot-depth and Straubing-Therien hierarchies, it is known to be decidable only at levels one [37, 12] and two [27] despite decades of active research.