Proving Positive Almost Sure Termination Under Strategies

Bournez Olivier (1) , Garnier Florent (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

In last RTA, we introduced the notion of probabilistic rewrite systems and we gave some conditions entailing termination of those systems within a finite mean number of reduction steps. Termination was considered under arbitrary unrestricted policies. Policies correspond to strategies for non-probabilistic rewrite systems. This is often natural or more useful to restrict policies to a subclass. We introduce the notion of positive almost sure termination under strategies, and we provide sufficient criteria to prove termination of a given probabilitic rewrite system under strategies. This is illustrated with several examples.

Domaines: Complexité [cs.CC]

Bournez Olivier, Garnier Florent. Proving Positive Almost Sure Termination Under Strategies. 17th International Conference on Rewriting Techniques and Applications - RTA'2006, Aug 2006, Seattle, WA/USA, pp.357--371, ⟨10.1007/11805618⟩. ⟨inria-00102945⟩