Skip to Main content Skip to Navigation
Conference papers

Proving Positive Almost Sure Termination Under Strategies

Bournez Olivier 1 Garnier Florent 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00102945
Contributor : Olivier Bournez <>
Submitted on : Tuesday, October 3, 2006 - 11:18:57 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

93

 

Contact                    Legal Notice                    Personal Data