出版社:European Association of Software Science and Technology (EASST)
摘要: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.