Extending PPTL for Verifying Heap Evolution Properties

TL;DR

This paper extends Propositional Projection Temporal Logic (PPTL) by integrating separation logic to verify heap evolution properties, enabling reasoning about linked lists within a decidable two-dimensional logic framework.

Contribution

It introduces PPTL$^{\tiny\mbox{SL}}$, a novel two-dimensional logic combining separation logic and PPTL, with a translation method to leverage existing PPTL decision procedures.

Findings

PPTL$^{\tiny\mbox{SL}}$ can describe linked list properties.

Existing PPTL tools can be reused for PPTL$^{\tiny\mbox{SL}}$.

A translation method links PPTL$^{\tiny\mbox{SL}}$ to PPTL formulas.

Abstract

In this paper, we integrate separation logic with Propositional Projection Temporal Logic (PPTL) to obtain a two-dimensional logic, namely PPTL$^{\tiny\mbox{SL}}$. The spatial dimension is realized by a decidable fragment of separation logic which can be used to describe linked lists, and the temporal dimension is expressed by PPTL. We show that PPTL and PPTL$^{\tiny\mbox{SL}}$ are closely related in their syntax structures. That is, for any PPTL$^{\tiny\mbox{SL}}$ formula in a restricted form, there exists an "isomorphic" PPTL formula. The "isomorphic" PPTL formulas can be obtained by first an equisatisfiable translation and then an isomorphic mapping. As a result, existing theory of PPTL, such as decision procedure for satisfiability and model checking algorithm, can be reused for PPTL$^{\tiny\mbox{SL}}$.