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.

翻译：概率下推自动机（pPDA）是处理离散随机选择与递归过程的编程语言的标准操作模型。时态性质可用于指定程序执行过程中事件的时间顺序。现有针对pPDA的时态性质模型检测方法主要聚焦于$\omega$-正则性质和线性时态逻辑（LTL）性质。本文研究pPDA对$\omega$-可视下推语言（可由CaRet等规范逻辑描述）的模型检测问题的可判定性与复杂性结果。这类逻辑公式能够显式考虑过程式程序产生的结构化计算性质。例如，CaRet可匹配过程调用及其对应的未来返回，从而能够表达诸如完全正确性与部分正确性等基础程序性质。