Ehrenfeucht-Fraïssé games (Ajtai-Fagin in fact) for regular languages. Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127.  As $\exists$MSO on words is equivalent to regular languages, the game can be written as follows.

A language $L \subseteq \{a, b\}^*$ is regular if and only if Delilah has no winning strategy in the following game:
1. Samson chooses $c, m \in \mathbb{N}$,
2. Delilah chooses $w \in L$,
3. Samson chooses $c$ subsets $C_1^w, \ldots, C_c^w$ of the set of positions in $w$ (i.e. $\{0, \ldots, |w|-1\}$),
4. Delilah chosses $v \not\in L$ and $c$ subsets $C_1^v, \ldots, C_c^v$ of the set of positions in $v$,
5. Samson and Delilah play the $m$-turn EF game on $(\mathfrak{S}(w), C_1^w, \ldots, C_c^w)$ and $(\mathfrak{S}(v), C_1^v, \ldots, C_c^v)$,
where $\mathfrak{S}(w)$ is the structure associated with the word $w$, i.e. :
$$\mathfrak{S}(w) = \langle \{0, \ldots, |w|-1\}, SUCC, Q_a, Q_b \rangle$$
with $Q_l = \{p \;|\; w_p = l\}$, and $SUCC$ is the binary successor predicate.

I have two questions:
- How does one show that $\{a^nb^n \;|\; n \in \mathbb{N}\}$ is not regular, using an EF argument like this,
- Is it easier/harder to play those games (to show non-regularity) when one has an ordering rather than the successor relation? (Those are equivalent in existential MSO).
We will give a winning strategy for Delilah. Let Samson choose his $c$ and $m$. Then Delilah chooses $w = a^n b^n$ for a large $n$ to be determined later. Let Samson choose his subsets $C^w_1,\ldots,C^w_c$ which we view as a coloring of the positions of $w$ with $2^c$ colors. Let $w'$ denote this colored word. The goal of Delilah at this point is to find a segment $w'[i,\ldots,j]$ of $w'$ with the following properties for an $r$ and a $t$ to be chosen later:


$0 \leq i \leq j \leq n$ (thus the segment belongs to the first part of $w'$),
the $r$-neighborhoods (neighborhoods of radius $r$) of $i$ and $j$ in $w'$ are isomorphic,
for every $k \in [i,\ldots,j]$, the $r$-neighborhood of $k$ in $w'$ appears as $r$-neighborhood of at least $t$ other positions of $w'$.


If she manages to do that, then she will choose her colored word to be
$$
v' = w'[0,\ldots,i-1] w'[i,\ldots,j]^2 w'[j+1,\ldots,2n-1].
$$ 
If $v$ is the ${a,b}$-word underlying $v'$, it will follow that $v$ does not belong to $L$ (because we pumped a non-empty segment of $a$'s), and Delilah has a winning strategy in the $m$-turn EF game on $w'$ and $v'$ (this follows from Hanf's Theorem if $r$ and $t$ are sufficiently large with respect to $c$ and $m$; see Theorem 1.4.1 in Ebinghaus and Flum book "Finite Model Theory").

Thus, it remains to show that if $n$ is sufficiently large with respect to $c$, $m$, $r$ and $t$ we can find a segment $w'[i,\ldots,j]$ as above. But this follows from a standard pigeonhole argument using the fact that the number of ismorphism types of $r$-neighborhoods is finite.

This worked for successor structures. With a linear order it will be a bit harder but I didn't think much about it.

Note that, not surprisingly, this argument looks a bit like "pumping" argument in automata. However, it is not as silly as just translating the formula to an automaton. I think it counts as a model-theoretic argument.