Star-free expressions for graphs, and an appropriate first-order logic

In the study of word languages, first-order logic is more frequently used with the order predicate x > y, and not the successor predicate x=y+1. (For MSO, there is no difference.) For example, the celebrated equivalence of star-free regular languages with first-order logic uses the first-order logic with order. With successor only, first-order logic for words is a less appealing logic. In contrast to words, the graph variant of first-order logic is usually studied with the edge relation E(x,y), which seems to be more in spirit of successor than order. It would be nice to define a variant of first-order logic for graphs, so that the standard notion of first-order logic for words becomes a special case for those graphs which are words. This is the topic of my talk. I will discuss a variant of star-free expressions for graphs, and a variant of first-order logic that is equivalent to these expressions. The variant is first-order logic with separator predicates of the form: “there is a path from vertex s to vertex t, which does not use vertices x1,…,xk”. (This is an infinite family of predicates, with one predicate of arity k+2 for every k.)