Skip to Main content Skip to Navigation

Induction for Positive Almost Sure Termination - Extended version -

Isabelle Gnaedig 1
1 CARTE - Theoretical adverse computations, and safety
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est
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.
Document type :
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Isabelle Gnaedig Connect in order to contact the contributor
Submitted on : Sunday, May 20, 2007 - 5:49:27 PM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM
Long-term archiving on: : Friday, November 25, 2016 - 4:01:01 PM


Files produced by the author(s)


  • HAL Id : inria-00147450, version 2



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



Les métriques sont temporairement indisponibles