Tobias Winkler ; Christina Gehnen ; Joost-Pieter Katoen - Model Checking Temporal Properties of Recursive Probabilistic Programs

lmcs:10029 - Logical Methods in Computer Science, December 15, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:24)2023
Model Checking Temporal Properties of Recursive Probabilistic ProgramsArticle

Authors: Tobias Winkler ORCID; Christina Gehnen ORCID; Joost-Pieter Katoen ORCID

    Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model checking pPDA against temporal properties have focused mostly on $\omega$-regular and LTL properties. In this paper, we give decidability and complexity results for the model checking problem of pPDA against $\omega$-visibly pushdown languages that can be described by specification logics such as CaRet. These logical formulae allow specifying properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties such as total and partial correctness.


    Volume: Volume 19, Issue 4
    Published on: December 15, 2023
    Accepted on: November 6, 2023
    Submitted on: September 12, 2022
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation; Funder: European Commission; Code: 787914

    Consultation statistics

    This page has been seen 939 times.
    This article's PDF has been downloaded 195 times.