Aperiodicity, Star-freeness, and First-order Logic Definability of Structured Context-Free Languages

A classic result in formal language theory is the equivalence among noncounting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Together with first-order completeness of linear temporal logic these results constitute a theoretical foundation for model-checking algorithms. Extending these results to structured subclasses of context-free languages, such as tree-languages did not work as smoothly: for instance W. Thomas showed that there are star-free tree languages that are counting. We show, instead, that investigating the same properties within the family of operator precedence languages leads to equivalences that perfectly match those on regular languages. The study of this old family of context-free languages has been recently resumed to enhance not only parsing (the original motivation of its inventor R. Floyd) but also to exploit their algebraic and logic properties. We have been able to reproduce the classic results of regular languages for this much larger class by going back to string languages rather than tree languages. Since operator precedence languages strictly include other classes of structured languages such as visibly pushdown languages, the same results given in this paper hold as trivial corollary for that family too.