Skip to main content

MSO Automata


Suitable for

MSc in Mathematics and Foundations of Computer Science
MSc in Computer Science


The Automata, Logic, and Games course presents automata that run on infinite binary trees. However, in certain applications, it is natural to consider trees with unbounded or even infinite branching degree. The automata that run on trees like this are sometimes called MSO automata, since the transition function is described by a monadic second-order logic (MSO) formula, rather than by explicitly giving the state for each successor.

Although these MSO automata have been considered in the literature, the complexity of various operations on these automata is not well studied. The goal in this project is to fill this gap.

Prerequisites: Automata, Logic, and Games