Tags:computing termination probability, deciding almost sure termination, first-order theory of the reals, probabilistic (affine additive) higher-order recursion schemes, quantitative/qualitative verification of omega-regular properties and restricted probabilistic tree stack automata
Abstract:
Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems about 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 omega-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 the so-called affine-additive higher-order recursion schemes (PAHORS). PAHORS extend order-1 recursion schemes and are incomparable with order-2 schemes.