The atnext/atprevious Hierarchy on the Starfree Languages
Bernd Borchert, Pascal Tesson · 2004
The temporal logic operators atnext and atprevious are alternatives for the operators until and since. P atnext Q has the meaning: at the next position in the future where Q holds it holds P. We define an asymmetric but natural notion of depth for the expressions of this linear temporal logic. The sequence of classes atn of languages expressible via such depth-n expressions gives a parametrization of the starfree regular languages which we call the atnext/atprevious ierarchy, or simply the at hierarchy. It turns out that the at hierarchy equals the hierarchy given by the n-fold weakly iterated block product of DA. It is shown that the at hierarchy is situated properly between the until/since and the dot-depth hierarchy.