Proving almost-sure termination by omega-regular decomposition

9Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Almost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. Our approach automatically decomposes the runs of the probabilistic program into a finite union of ω-regular subsets and then proves almost-sure termination of each subset based on the notion of localized ranking supermartingales. Compared to the lexicographic methods and the compositional methods, our approach does not require a lexicographic order over the ranking supermartingales as well as the so-called unaffecting condition. Thus it has high generality. We present the algorithm of our approach and prove its soundness, as well as its relative completeness. We show that our approach can be applied to some hard cases and the evaluation on the benchmarks of previous works shows the significant efficiency of our approach.

Cite

CITATION STYLE

APA

Chen, J., & He, F. (2020). Proving almost-sure termination by omega-regular decomposition. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (pp. 869–882). Association for Computing Machinery. https://doi.org/10.1145/3385412.3386002

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free