@inproceedings{10.1145/3531130.3533351,
    Abstract = {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 {$\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 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.},
    Address = {New York, NY, USA},
    Author = {Li, Guanyan and Murawski, Andrzej and Ong, Luke},
    BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
    File = {Probabilistic Verification Beyond Context-Freeness - 3531130.3533351.pdf},
    ISBN = {9781450393515},
    Keywords = {first-order theory of the reals, probabilistic (affine additive) higher-order recursion schemes, deciding almost sure termination, computing termination probability, restricted (probabilistic) tree stack automata},
    Location = {Haifa, Israel},
    Publisher = {Association for Computing Machinery},
    Series = {LICS '22},
    Title = {Probabilistic Verification Beyond Context-Freeness},
    URL = {https://doi.org/10.1145/3531130.3533351},
    Year = {2022},
    articleno = {33},
    bdsk-url-1 = {https://doi.org/10.1145/3531130.3533351},
    date-added = {2022-08-29 14:27:27 +0200},
    date-modified = {2022-08-29 14:27:27 +0200},
    numpages = {13},
    doi = {10.1145/3531130.3533351}
}

@inproceedings{10.1145/3531130.3533351, Abstract = {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 {$\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 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.}, Address = {New York, NY, USA}, Author = {Li, Guanyan and Murawski, Andrzej and Ong, Luke}, BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, File = {Probabilistic Verification Beyond Context-Freeness - 3531130.3533351.pdf}, ISBN = {9781450393515}, Keywords = {first-order theory of the reals, probabilistic (affine additive) higher-order recursion schemes, deciding almost sure termination, computing termination probability, restricted (probabilistic) tree stack automata}, Location = {Haifa, Israel}, Publisher = {Association for Computing Machinery}, Series = {LICS '22}, Title = {Probabilistic Verification Beyond Context-Freeness}, URL = {https://doi.org/10.1145/3531130.3533351}, Year = {2022}, articleno = {33}, bdsk-url-1 = {https://doi.org/10.1145/3531130.3533351}, date-added = {2022-08-29 14:27:27 +0200}, date-modified = {2022-08-29 14:27:27 +0200}, numpages = {13}, doi = {10.1145/3531130.3533351} }