A Modal Logic for Termgraph Rewriting

TL;DR

This paper introduces a modal logic designed to accurately describe and analyze graph transformations, specifically for termgraphs that model complex data structures with sharing and cycles, enabling formal reasoning about rewriting and normal forms.

Contribution

It presents a novel modal logic that can represent termgraph transformations, including matching, rewriting, and normal form computation, surpassing propositional dynamic logic in expressiveness.

Findings

Logic can describe termgraphs with sharing and cycles

It faithfully models rewriting and normal form computation

Enables specification of classical data-structure shapes

Abstract

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.).