一句话：提出基于算子优先语言（OPL）的时序逻辑 POTL，证明其一阶完备性，表达力优于 NWTL 与 OPTL。
过程式程序的模型检测推动了对上下文无关结构时序逻辑的研究，已有工作包括嵌套字上的 CaRet 与 NWTL，以及基于算子优先语言（OPL）的 OPTL。本文定义新的 OPL 时序逻辑 POTL，并证明其相对一阶逻辑是完备的（FO-complete），即其表达能力与相应一阶逻辑吻合。POTL 相比 NWTL 的改进在于：在存在异常类构造的情况下仍能刻画前/后条件、栈检查等需求；相比 OPTL，本文证明 OPTL 并不 FO-完备，而 POTL 不仅能达到 FO-完备，还更易表达栈检查与函数局部性质。作者在姊妹论文中给出 POTL 的模型检测过程及原型工具的实验结果，本文对该互补结果作了简要总结。
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.
@article{paperbot1678,
title = {A First-Order Complete Temporal Logic for Structured Context-Free Languages},
author = {Michele Chiari and Dino Mandrioli and Matteo Pradella},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:11)2022}
}