I would like to find a good reference detailing the mapping between Monadic Second-order Logic of two successors (MS2S) and infinite binary tree automata. In particular I'd like to see a well presented and easy to follow proof of decidability and an algorithm for the conversion.
I know this result is well-established, but there are many books on mathematical logic to choose from with varying foci. Most papers I've encountered cite earlier works I haven't been able to find copies of (at least not inexpensive copies). I've had trouble knowing where to even start. I don't want to buy an expensive book that only covers understanding how an algorithm transforming the language of MS2S to infinite binary tree automata is constructed and proven correct in a few of its chapters unless that's the only way to get access to the material.
Any solid references or explanations would be greatly appreciated. Work on efficient algorithms for model checking MS2S would be a bonus. The only software I'm aware of is MONA, which focuses on the weak form of MS2S on finite trees (WMS2S) as far as I'm aware.
One reference I've considered is "Graph Structure of Monadic Second-Order Logic" by Bruno Courcelle, but I'm not sure if that will cover the topic in the detail I'm looking for and is much more expensive than I would like.