Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTermination of Monotone Programs
128
0
0.0
(
0
)
Added by
Omar Al-Bataineh I.
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present an efficient approach to prove termination of monotone programs with integer variables, an expressive class of loops that is often encountered in computer programs. Our approach is based on a lightweight static analysis method and takes advantage of simple %nice properties of monotone functions. Our preliminary implementation %beats shows that our tool has an advantage over existing tools and can prove termination for a high percentage of loops for a class of benchmarks.
rate research
Read More
Extending our own and others earlier approaches to reasoning about termination of probabilistic programs, we propose and prove a new rule for termination with probability one, also known as almost-certain termination. The rule uses both (non-strict) super martingales and guarantees of progress, together, and it seems to cover significant cases that earlier methods do not. In particular, it suffices for termination of the unbounded symmetric random walk in both one- and two dimensions: for the first, we give a proof; for the second, we use a theorem of Foster to argue that a proof exists. Non-determinism (i.e. demonic choice) is supported; but we do currently restrict to discrete distributions.
106 -
Desharnais Jules (Departement dinformatique et de genie logiciel
, n Universite Laval
, Quebec
2010
Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, Lobs formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additively idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.
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.
We present a reduction of the termination problem for a Turing machine (in the simplified form of the Post correspondence problem) to the problem of determining whether a continuous-time Markov chain presented as a set of Kappa graph-rewriting rules has an equilibrium. It follows that the problem of whether a computable CTMC is dissipative (ie does not have an equilibrium) is undecidable.
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
