Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAutomated Termination Analysis of Polynomial Probabilistic Programs
88
0
0.0
(
0
)
Added by
Marcel Moosbrugger
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions - including the constraints on supermartingales - of a proof rule. Our software tool Amber can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.
rate research
Read More
We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the best of our knowledge, the considered family of MPPs is hitherto the largest one for which termination is decidable. We present an explicit recursive function which is essentially Ackermannian, to compute the maximal length of ascending chains of polynomial ideals under a control function, and thereby obtain a complete answer to the questions raised by Seidenberg. This maximal length facilitates a precise complexity analysis of our algorithms for computing the NTI and deciding termination of MPPs. We extend our method to programs with polynomial guarded commands and show how an incomplete procedure for MPPs with inequality guards can be obtained. An application of our techniques to invariant generation of polynomial programs is further presented.
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $Pi^0_2$-complete. We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.
The extension of classical imperative programs with real-valued random variables and random branching gives rise to probabilistic programs. The termination problem is one of the most fundamental liveness properties for such programs. The qualitative (aka almost-sure) termination problem asks whether a given program terminates with probability 1. Ranking functions provide a sound and complete approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via ranking supermartingales (RSMs). RSMs have been extended to lexicographic RSMs to handle programs with involved control-flow structure, as well as for compositional approach. There are two key limitations of the existing RSM-based approaches: First, the lexicographic RSM-based approach requires a strong nonnegativity assumption, which need not always be satisfied. The second key limitation of the existing RSM-based algorithmic approaches is that they rely on pre-computed invariants. The main drawback of relying on pre-computed invariants is the insufficiency-inefficiency trade-off: weak invariants might be insufficient for RSMs to prove termination, while using strong invariants leads to inefficiency in computing them. Our contributions are twofold: First, we show how to relax the strong nonnegativity condition and still provide soundness guarantee for almost-sure termination. Second, we present an incremental approach where the process of computing lexicographic RSMs proceeds by iterative pruning of parts of the program that were already shown to be terminating, in cooperation with a safety prover. In particular, our technique does not rely on strong pre-computed invariants. We present experimental results to show the applicability of our approach to examples of probabilistic programs from the literature.
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions.
The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gamblers Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
