一句话：给出概率下推自动机对 ω-可见下推语言（如 CaRet 可描述的性质）模型检测的可判定性与复杂度结果。
概率下推自动机（pPDA）是含离散随机选择与递归过程的程序语言的标准操作模型，时序性质可用于刻画程序执行中事件的时间顺序。已有 pPDA 模型检测工作主要针对 ω-正则与 LTL 性质。本文研究了 pPDA 相对于 ω-可见下推语言的模型检测问题，这类语言可由 CaRet 等规约逻辑描述。CaRet 能匹配过程调用与其对应的未来返回，因此可表达全正确性与部分正确性等基本程序性质。作者给出了该模型检测问题的可判定性与复杂度结果，从而将 pPDA 的时序验证从 ω-正则/LTL 扩展到能显式考虑过程式程序结构化计算的一类性质。
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.
@article{paperbot2170,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:24)2023}
}