Expressiveness of graph conditions with variables

摘要

Graph conditions are very important for graph transformation systems and graph programs in a large variety of application areas. Nevertheless, non-local graph properties like ``there exists a path'', ``the graph is connected'', and ``the graph is cycle-free'' are not expressible by finite graph conditions. In this paper, we generalize the notion of finite graph conditions, expressively equivalent to first-order formulas on graphs, to finite $HR^+$ graph conditions, i.e., finite graph conditions with variables where the variables are place-holders for graphs generated by a hyperedge replacement system. We show that graphs with variables and replacement morphisms form a weak adhesive HLR category. We investigate the expressive power of $HR^+$ graph conditions and show that finite $HR^+$ graph conditions are more expressive than monadic second-order graph formulas.