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.
Type de document :
Communication dans un congrès
Frank Pfenning. 17th International Conference on Rewriting Techniques and Applications - RTA'2006, Aug 2006, Seattle, WA/USA, Springer, 4098, pp.357--371, 2006, Lecture Notes in Computer Science. 〈10.1007/11805618〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00102945
Contributeur : Olivier Bournez <>
Soumis le : mardi 3 octobre 2006 - 11:18:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Bournez Olivier, Garnier Florent. Proving Positive Almost Sure Termination Under Strategies. Frank Pfenning. 17th International Conference on Rewriting Techniques and Applications - RTA'2006, Aug 2006, Seattle, WA/USA, Springer, 4098, pp.357--371, 2006, Lecture Notes in Computer Science. 〈10.1007/11805618〉. 〈inria-00102945〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

52

Contact


archive-ouverte@inria.fr