POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages

TL;DR

This paper introduces POTL, a new first-order complete temporal logic for Operator Precedence Languages, enabling advanced reasoning about procedural programs with complex control structures.

Contribution

The paper defines POTL, proves its FO-completeness, and provides a model checking procedure, advancing temporal logic capabilities for OPLs over previous logics.

Findings

POTL is FO-complete.

POTL enables expressing pre/post-conditions and stack inspection.

Model checking for POTL is feasible.

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 (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, prove its FO-completeness, and provide a model checking procedure for it. 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 by being FO-complete, and by expressing more easily stack inspection and function-local properties.