Proving Termination of Linear DPO Graph Rewriting Systems using Weighted Type Graphs Anonymous
Qi Qiu · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
We improve a termination technique initially developed by Zantema et al. for cycle rewriting, later extended to graph rewriting by Bruggink et al., and generalized by Endrullis et al., which uses weighted type graphs, to prove the uniform termination of arrow-labeled multigraph rewriting systems with the double pushout approach.We establish a machine-checkable condition that considers the number of morphisms from graphs with multiple edges under specific conditions, a factor previously overlooked.Our enhancement resolves cases that prior methods could not and simplifies termination proofs for certain systems.