  We describe two formalisms for defining graph languages, and prove that they
are equivalent:
  1. Separator logic. This is first-order logic on graphs which is allowed to
use the edge relation, and for every $n \in \{0,1,\ldots \}$ a relation of
arity $n+2$ which says that "vertex $s$ can be connected to vertex $t$ by a
path that avoids vertices $v_1,\ldots,v_n$".
  2. Star-free graph expressions. These are expressions that describe graphs
with distinguished vertices called ports, and which are built from finite
languages via Boolean combinations and the operations on graphs with ports used
to construct tree decompositions.
  Furthermore, we prove a variant of Sch\"utzenberger's theorem (about
star-free languages being those recognized by a periodic monoids) for graphs of
bounded pathwidth. A corollary is that, given $k$ and a graph language
represented by an \mso formula, one can decide if the language can be defined
in either of two equivalent formalisms on graphs of pathwidth at most $k$.
