Michele Chiari ; Dino Mandrioli ; Matteo Pradella - A First-Order Complete Temporal Logic for Structured Context-Free Languages

lmcs:8355 - Logical Methods in Computer Science, July 29, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:11)2022
A First-Order Complete Temporal Logic for Structured Context-Free LanguagesArticle

Authors: Michele Chiari ; Dino Mandrioli ; Matteo Pradella

    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.


    Volume: Volume 18, Issue 3
    Published on: July 29, 2022
    Accepted on: May 10, 2022
    Submitted on: August 13, 2021
    Keywords: Computer Science - Logic in Computer Science

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1992 times.
    This article's PDF has been downloaded 642 times.