Rankers over Infinite Words

TL;DR

This paper characterizes four fragments of first-order logic over finite and infinite words using generalized rankers, providing new insights into their expressive power and logical structure.

Contribution

It introduces two natural extensions of rankers for infinite words, characterizing complex logical fragments and connecting them with temporal logics.

Findings

Characterizations of FO2, Sigma2∩FO2, Pi2∩FO2, and Delta2 using rankers.

Extension of rankers to infinite words with full expressive power.

Connections between rankers and unambiguous temporal logics.

Abstract

We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite words, they coincide with classical rankers and over infinite words, they both have the full expressive power of FO2. Moreover, the first extension of rankers admits a characterization of the intersection of Sigma2 and FO2 while the other leads to a characterization of the intersection of Pi2 and FO2. Both versions of rankers yield characterizations of the fragment Delta2. As a byproduct, we also obtain characterizations based on unambiguous temporal logic and unambiguous interval temporal logic.