Paper Info
Title
Probabilistic choice, reversibility, loops, and miracles
Abstract
We consider an addition of probabilistic choice to Abrial's Generalised Substitution Language (GSL) in a form that accommodates the backtracking interpretation of non-deterministic choice. Our formulation is introduced as an extension of the Prospective Values formalism we have developed to describe the results from a backtracking search. Significant features are that probabilistic choice is governed by feasibility, and non-termination is strict. The former property allows us to use probabilistic choice to generate search heuristics. In this paper we are particularly interested in iteration. By demonstrating sub-conjunctivity and monotonicity properties of expectations we give the basis for a fixed point semantics of iterative constructs, and we consider the practical proof treatment of probabilistic loops. We discuss loop invariants, loops with probabilistic behaviour, and probabilistic termination in the context of a formalism in which a small probability of non-termination can dominate our calculations, proposing a method of limits to avoid this problem. The formal programming constructs described have been implemented in a reversible virtual machine (RVM).
Year
DOI
Venue
2010
10.1007/978-3-642-16690-7_13
UTP
Keywords
Field
DocType
prospective values,non-deterministic choice,backtracking search,generalised substitution language,probabilistic choice,probabilistic loop,backtracking interpretation,search heuristics,probabilistic behaviour,probabilistic termination,fixed point,virtual machine
Computer science,Algorithm,Probabilistic CTL,Theoretical computer science,Heuristics,Loop invariant,Probabilistic argumentation,Fixed point,Probabilistic logic,Probabilistic relevance model,Backtracking
Conference
Volume
ISSN
ISBN
6445
0302-9743
3-642-16689-X
Citations 
PageRank 
References 
2
0.36
15
Authors
2
Name
Order
Citations
PageRank
Bill Stoddart113515.69
Pete Bell220.36