Using logic to prove non-regularity of a language

Question

A language $L$ is regular if and only if it is definiable by a sentence in monadic second order logic (MSO) over strings (J.R. Buchi, Weak second-order arithmetic and Finite automata; Z. Math. Logik Grundlagen Math. 6 (1960) 66-92).

1. Are there proofs of non-regularity of a language $L$ (e.g. $L = \{ a^n b^n \}$) that are based on the non expressibility in MSO of $L$?
   
2. What are the (logic) techniques (if any) that can be used?

I googled a little bit, but didn't find anything relevant (but I'm not an expert, so I'm probably using the wrong terms).

• Luke Mathieson: Everything I've found (in a non-exhaustive search) goes the other way - using non-regularity to show inexpressibility in MSO. Even Ebbinghaus & Flum's "Finite Model Theory" only has examples in that direction (if you have it handy, Chapter 7, pp. 112-113, 2nd Ed.).
• J.-E. Pin: I agree with @luke-mathieson . All examples I know go the other way. If that helps, note that, over strings, MSO = $\exists$MSO. Thus it would suffice to prove non expressibility in $\exists$MSO.
• Kaveh: The usual way to directly show something is not expressible in descriptive complexity/finite model theory is to use some variation of Ehrenfeucht-Fraisse games.
• Hendrik Jan: But in a way also Büchi was working the other way. Not per sé interested in the regualr languages, but in applying their decidability to MSO logic?
• Caleb Stanford: This essay defines EF games for MSO definable formulas. While it shows only that the class of finite structures is not MSO-definable (which doesn't correspond to a non-regular language), perhaps an argument can be made to show that $\{ 0^n 1^n \mid n \in \mathbb{N}\}$ is not MSO-definable, just by showing the duplicator wins the $n$-turn game on strings 0ドル^n 1^n$ and 0ドル^{n+1} 1^{n+1}$.