基于半环上加权类型图证明图变换系统的终止性
计算机科学中的逻辑
2023-10-12 v3 形式语言与自动机理论
摘要
我们介绍了基于字符串重写的矩阵解释来证明图变换系统一致终止的技术。我们通过将该技术适用于图重写而非字符串重写，并将其推广到有序半环，从而推广了该技术。以此方式，我们获得了一个受[5]中热带和极地类型图启发并引入了算术类型图新变体的框架。这些类型图可用于为图分配权重，并证明这些权重在每次重写步骤中递减，以证明终止性。我们给出一个涉及计数器的示例，并讨论了在工具Grez中的实现。
引用
@article{arxiv.1505.01695,
title = {Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings},
author = {H. J. Sander Bruggink and Barbara König and Dennis Nolte and Hans Zantema},
journal= {arXiv preprint arXiv:1505.01695},
year = {2023}
}