一句话：证明受限概率树栈自动机的几乎必然终止与ω-正则模型检测可判定，并对应概率 MAHORS。
概率下推自动机等递归状态机具有可判定的终止与线性时序模型检测问题；但概率高阶递归方案（HORS）的几乎必然终止即使在 order-2 也已不可判定。本文为寻找仍可验证的超越上下文无关模型，研究受限概率树栈自动机（rPTSA）。该模型在非确定性情形对应 multiple context-free languages，是上下文无关语言的真扩展。作者证明 rPTSA 上的几乎必然终止、正几乎必然终止以及 ω-正则模型检测均可判定。在高阶层面，这对应于可验证概率版 MAHORS；MAHORS 扩展 order-1 方案，且与 order-2 方案不可比。
Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems concerning termination (time) and linear-time model checking. Higher-order recursion schemes (HORS) are a prominent formalism for the analysis of higher-order computation. Recent studies showed that, for the probabilistic variant of HORS, even the basic problem of determining whether a scheme terminates almost surely is undecidable. Moreover, the undecidability already holds for order-2 schemes (order-1 schemes are known to correspond to pushdown automata). Motivated by these results, we study restricted probabilistic tree-stack automata (rPTSA), which in the nondeterministic setting are known to characterise a proper extension of context-free languages, namely, the multiple context-free languages. We show that several verification problems, such as almost-sure termination, positive almost-sure termination and ω-regular model checking are decidable for this class. At the level of higher-order recursion schemes, this corresponds to being able to verify a probabilistic version of MAHORS (which are a multiplicative-additive version of higher-order recursion schemes). MAHORS extend order-1 recursion schemes and are incomparable with order-2 schemes.