一种用于项图重写的模态逻辑
A Modal Logic for Termgraph Rewriting
摘要：
我们提出了一个模态逻辑量身定制的描述图变换，并讨论了它的一些属性。我们专注于一类特殊的图，称为termgraphs。它们是一阶项，增加了共享和循环。Termgraphs允许一个描述经典的数据结构（可能与指针），如双向链表，循环列表等，我们展示了如何建议的逻辑可以忠实地描述（一）termgraphs以及（二）应用termgraphs重写规则（即匹配和替换）和（iii）计算范式相对于一个给定的重写系统。我们还展示了如何建议的逻辑，这是更具表现力的命题动态逻辑，可以用来指定形状的经典数据结构（如二叉树，循环列表等）。
英文摘要：
We propose a modal logic tailored to describe graph transformations and discuss some of its properties. We focus on a particular class of graphs called termgraphs. They are first-order terms augmented with sharing and cycles. Termgraphs allow one to describe classical data-structures (possibly with pointers) such as doubly-linked lists, circular lists etc. We show how the proposed logic can faithfully describe (i) termgraphs as well as (ii) the application of a termgraph rewrite rule (i.e. matching and replacement) and (iii) the computation of normal forms with respect to a given rewrite system. We also show how the proposed logic, which is more expressive than propositional dynamic logic, can be used to specify shapes of classical data-structures (e.g. binary trees, circular lists etc.).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
