LARA Monadic Second-Order Logic over Trees Tree Automata Techniques and Applications (Tata book) The MONA Project Timbook for Reachability Analysis and Tree Automata Calculations