Extending PPTL for Verifying Heap Evolution Properties

Original · EN

In this paper, we integrate separation logic with Propositional Projection Temporal Logic (PPTL) to obtain a two-dimensional logic, namely PPTL. 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 are closely related in their syntax structures. That is, for any PPTL 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.