Electronic Communications of the EASST
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.61.831
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.61.831.831
Hosted By Universitätsbibliothek TU Berlin.