Proving Termination of Probabilistic Programs Using Patterns

Details Proving Termination of Probabilistic Programs Using Patterns Proving Termination of Probabilistic Programs Using Patterns

2012-04-13

arxiv.org/abs/1204.2932v1

Computer Science

Logic in Computer Science

A shorter version of the paper appeared in the Proceedings of Computer Aided Verification (CAV) 2012

Scientific paper

Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one ("almost-sure termination"), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a "terminating pattern", which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.

Affiliated with

Also associated with

No associations

Rating

Proving Termination of Probabilistic Programs Using Patterns does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Proving Termination of Probabilistic Programs Using Patterns, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Proving Termination of Probabilistic Programs Using Patterns will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-143773