HR* Graph Conditions Between Counting Monadic Second-Order and Second-Order Graph Formulas

Abstract

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.