We prove that every monadic second-order property of the unfolding of a transition system is a monadic second-order property of the system itself. An unfolding is an instance of the general notion of graph covering. We consider two more instances of this notion. A similar result is possible for one of them but not for the other.

In every undirected graph or, more generally, in every undirected hypergraph of bounded rank, one can specify an orientation of the edges or hyperedges by monadic second-order formulas using quantifications on sets of edges or hyperedges. The proof uses an extension to hypergraphs of the classical notion of a depth-first spanning tree. Applications are given to the characterization of the classes of graphs and hypergraphs having decidable monadic theories.