Star-free picture expressions are strictly weaker than first-order logic

Abstract

We exhibit a first-order definable picture language which we prove is not expressible by any star-free picture expression, i. e., it is not star-free. Thus first-order logic over pictures is strictly more powerful than star-free picture expressions are. This is in sharp contrast with the situation with words: the well-known McNaughton-Papert theorem states that a word language is expressible by a first-order formula if and only if it is expressible by a star-free (word) expression. The main ingredients of the non-expressibility result are a Fraïssé-style algebraic characterization of star freeness for picture languages and combinatorics on words.