HR* Graph Conditions Between Counting Monadic Second-Order and Second-Order Graph Formulas - Radke, Hendrik (Electronic Communications of the EASST, 2013)
Graph conditions are a means to express structural properties for graph transformation systems and graph programs in a large variety of application areas. With HR* graph conditions, non-local graph properties like “there exists a path of arbitrary length” or “the graph is circle-free” can be expressed. We show, by induction over the structure of formulas and conditions, that (1) any node-counting monadic second-order formula can be expressed by an HR∗ condition and (2) any HR* condition can be expressed by a second-order graph formula.