  We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting
with strong matching. Our approach, called PBPO+, allows more control over the
embedding of the pattern in the host graph, which is important for a large
class of rewrite systems. We argue that PBPO+ can be considered a unifying
theory in the general setting of quasitoposes, by demonstrating that PBPO+ can
define a strict superset of the rewrite relations definable by PBPO, AGREE and
DPO. Additionally, we show that PBPO+ is well suited for rewriting labeled
graphs and some classes of attributed graphs, by introducing a lattice
structure on the label set and requiring graph morphisms to be
order-preserving.

Logic in Computer Science