A First-Order Complete Temporal Logic for Structured Context-Free Languages

TL;DR

This paper introduces POTL, a new FO-complete temporal logic for Operator Precedence Languages, enabling advanced reasoning about procedural programs with structured control flows and exceptions.

Contribution

The paper defines POTL, a novel FO-complete logic for OPLs, surpassing NWTL and OPTL in expressiveness for procedural program verification.

Findings

POTL is FO-complete, enabling precise formal reasoning.

POTL can express pre/post-conditions and stack inspection.

Experimental results demonstrate the practicality of the logic.

Abstract

The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPLs), more powerful than Nested Words. We define the new OPL-based logic POTL and prove its FO-completeness. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL too, which instead we show not to be FO-complete; it also allows to express more easily stack inspection and function-local properties. In a companion paper we report a model checking procedure for POTL and experimental results based on a prototype tool developed therefor. For completeness a short summary of this complementary result is provided in this paper too.