The monadic second-order logic of graphs,II: Infinite graphs of bounded width

A countable graph can be considered as the value of a certain infinite expression, represented itself by an infinite tree. We establish that the set of finite or infinite (expression) trees constructed with a finite number of operators, the value of which is a graph satisfying a property expressed in monadic second-order logic, is itself definable in monadic second-order logic. From Rabin's theorem, the emptiness of this set of (expression) trees is decidable. It follows that the monadic second-order theory of an equational graph, or of the set of countable graphs of width less than an integerm, is decidable. This work has been supported by the “Programme de Recherches Coordonnées: Mathématiques et Informatique.” Reprints can be requested by electronic mail at mcvax!inria!geocub!courcell (on UUCP network) or courcell@geocub.greco-prog.fr. Unité de Recherche associée au C.N.R.S. no. 726.