Termination is an important property of algorithms, ensuring that they will not run indefinitely. This property is often essential for correctness, yet proving termination can be challenging.
Under the SAPPORO project, we developed an automated technique called Subgraph Counting to prove termination for algorithms modeled as injective double-pushout (DPO) graph rewriting systems. DPO graph rewriting systems model data as graphs and algorithms as sets of rules representing operations that algorithms can perform. Each rule specifies conditions for replacing a subgraph with another.
In this presentation, we focus on the termination of algorithms representable as a single rule. The Subgraph Counting technique relies on the principle that if the number of occurrences of a specific subgraph strictly decreases with each rewriting step, then the rewriting rule will eventually terminates. The key challenge is to estimate the number of occurrences of the subgraph in the graph before and after a rewriting step in an implicit context. We are going to present a sufficient condition on the rewriting rule that makes this estimation possible.