A set of graphs is "definable" in a logic if it is the set of models of a formula in that logic. These descriptive representations of sets of graphs by logical formulae constitute the basis of property specification in system design and is used to write proofs of correctness of the system (e.g. using Hoare logic). A "context-free" set of graphs is a component of the least solution of a system of recursive equations (written using a set of algebraic operations) whose unknowns denote sets. These constructive representations describe how the sets are built from basic building blocks and are used to model low-level implementation details. The verification problem “does the implementation satisfy a given property?” amounts to checking if a set built according to a context-free constructive representation is included in the descriptive specification set.

Motivated by verification problems that occur in the area of distributed computing, in particular proving the correctness of reconfigurable networks, we give an explicit characterisation of the sets of graphs that are (1) definable in Monadic-Second Order Logic (MSO) and (2) least solutions of Hyper-edge Replacement (HR) graph grammars. The inclusion problem is decidable for these sets, as a consequence of a celebrated theorem by Courcelle, stating the decidability of the satisfiability for MSO over graphs of bounded tree-width. We show that MSO-definable and HR sets are (3) recognizable (in the algebra of graph operation in which the HR grammar is written) and (4) have bounded tree-width. Moreover, these sets are the images of recognizable sets of trees (having arbitrarily many unordered children) under MSO-definable transductions. The latter condition is used to define MSO-definable HR sets from known ones, such as described by regular graph grammars or regular expressions for graphs of tree-width two.