Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into 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 study the model checking problem of pPDA against $\omega$-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than $\omega$-regular properties. 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.

翻译：概率下推自动机（pPDA）是涉及离散随机选择、过程和返回的编程语言的标准操作模型。时序性质有助于深入了解程序执行过程中事件的时序顺序。现有针对pPDA的时序性质模型检测方法主要关注ω-正则和LTL性质。本文研究了pPDA针对ω-可见下推语言的模型检测问题，这类语言可通过CaRet等规范逻辑进行描述，且严格比ω-正则性质更具表达力。这些逻辑公式能够显式地考虑由过程化程序产生的结构化计算特性。例如，CaRet能够匹配过程调用与其对应的未来返回，从而可以表达诸如总正确性和部分正确性等基本程序性质。