HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Tuesday, October 3, 2006 - 11:18:57 AM
Last modification on : Friday, May 13, 2022 - 10:18:05 PM

Identifiers

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE | INRIA2

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 Datacite

Share

Metrics

Record views

29

 

Contact                    Legal Notice                    Personal Data