| סיכום: | <p>Probability theory and probabilistic modelling have become indispensable across a wide range of scientific disciplines, with probabilistic programs emerging as a particularly flexible means of encoding sophisticated models in executable code. These programs, which merge traditional programming constructs with probabilistic reasoning, play a pivotal role in areas such as machine learning and systems biology. However, as these programs gain prominence, the demand for robust verification methods becomes increasingly urgent.</p>
<br>
<p>While Markov Chains (MCs) have long been foundational tools in this field, their limitations in modelling complex, recursive systems have prompted the development of more expressive models, such as Recursive Markov Chains (RMCs) and Probabilistic Pushdown Automata (pPDAs). Recent advancements, including extensions to higher-order grammars like Probabilistic Higher-Order Recursion Schemes (PHORS), offer enhanced expressiveness but introduce significant challenges, such as the undecidability of Almost Sure Termination (AST). This underscores the need for models that balance expressiveness with decidability.</p>
<br>
<p>This research presents and examines the Restricted Probabilistic Tree-Stack Automaton (rPTSA), a novel probabilistic model that extends recursive models while circumventing the undecidability issues associated with PHORS. Originating from the Restricted Tree-Stack Automaton (rTSA), the rPTSA model inherits broad connections to various fields, including linguistics and higher-order verification. Building on these connections, the research also introduces Probabilistic Additive HORS (PAHORS), which incorporates an affineness constraint and pair-product structures into PHORS.</p>
<br>
<p>We demonstrate that these two models, rPTSA and PAHORS, are equi-expressive, as they inherit characteristics from their non-probabilistic counterparts, rTSA and Multiplicative Additive HORS (MAHORS). Furthermore, rPTSA and PAHORS are shown to be strictly more expressive than order-1 PHORS and incomparable to order-2 PHORS, and they hence offer a balance between expressiveness and decidability.</p>
<br>
<p>Utilising their equi-expressiveness, this work primarily focuses on the rPTSA model. Firstly, it establishes the decidability of the Almost-Sure Termination (AST) and Positive Almost-Sure Termination (PAST) properties for rPTSA, and develops methods for quantitatively analysing termination probability and expected termination time. The research also delves into model checking for both linear-time properties (ω-regular and LTL) and branching-time properties (PCTL*). Notably, the PCTL* model checking procedure relies heavily upon the algorithm established for LTL. Additionally, this research examines the restriction property of rPTSA, a crucial feature that prevents rPTSA from attaining Turing-completeness.</p>
<br>
<p>The practical contribution of this work is the development of the Probabilistic Tree-Stack Verifier (PTSV), an efficient tool for determining termination probability and expected termination time. Further attention is given to PAHORS and other key models, such as pPDA and MCFG. The study discusses the mutual conversions between rPTSA and PAHORS, as well as conversions from other models of interest, such as pPDA and Stochastic MCFG, to rPTSA.</p>
|
|---|