Resource-Bound Quantification for Graph Transformation

TL;DR

This paper introduces resource-bound quantification in linear logic to reason about graph transformation systems, providing an algebraic and logical framework for modeling concurrent systems across various scientific domains.

Contribution

It extends intuitionistic linear logic with resource-bound quantification to implicitly handle double-pushout conditions in graph transformations.

Findings

Resource logic can effectively reason about graph transformation systems.

The approach simplifies the algebraic characterization of DPO conditions.

The framework applies to modeling concurrent systems in software and life sciences.

Abstract

Graph transformation has been used to model concurrent systems in software engineering, as well as in biochemistry and life sciences. The application of a transformation rule can be characterised algebraically as construction of a double-pushout (DPO) diagram in the category of graphs. We show how intuitionistic linear logic can be extended with resource-bound quantification, allowing for an implicit handling of the DPO conditions, and how resource logic can be used to reason about graph transformation systems.