Induction for Positive Almost Sure Termination - Extended version -

Isabelle Gnaedig 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In this paper, we propose an inductive approach to prove positive almost sure termination of probabilistic rewriting under the innermost strategy. We extend to the probabilistic case a technique we proposed for termination of usual rewriting under strategies. The induction principle consists in assuming that terms smaller than the starting terms for an induction ordering are positively almost surely terminating. The proof is developed in generating proof trees, modelizing rewriting trees, in alternatively applying abstraction steps, expressing the application of the induction hypothesis, and narrowing steps, simulating the possible rewriting steps after abstraction. This technique is fully automatable for rewrite systems on constants, very useful to modelize probabilistic protocols.
Type de document :
Rapport
[Research Report] 2007, pp.16
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00147450
Contributeur : Isabelle Gnaedig <>
Soumis le : dimanche 20 mai 2007 - 17:49:27
Dernière modification le : jeudi 11 janvier 2018 - 06:21:25
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 16:01:01

Fichier

IPAS-termin-extended.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00147450, version 2

Collections

Citation

Isabelle Gnaedig. Induction for Positive Almost Sure Termination - Extended version -. [Research Report] 2007, pp.16. 〈inria-00147450v2〉

Partager

Métriques

Consultations de la notice

213

Téléchargements de fichiers

84