Grande Salle de VERIMAG
12 November 2009 - 11h00
A classification of randomized fair strategies for studying termination of term rewriting
by Florent Garnier from Vermimagg- Team DCS
Abstract: In this talk, we tackled the problem of the probabilistic termination of infinite state space rule-based programs when non-deterministic choices are solved using randomized strategies. In this talk, we consider the probabilistic termination of Term Rewrite Systems (TRS) under randomized fair strategies. In this context, randomized strategies are an adaption of Vardi's
Schedulers to the realm of term rewriting and probabilistic fairness we consider corresponds to de Alfaro's definition of probabilistic fairness. In this work, we consider the following problem:
Which are the term rewrite systems that terminate under all randomized fair strategies of the
following classes:
Infinite precision strategies with an unbounded memory, Infinite precision strategy with a
bounded memory, and finite precision strategies.
We also prove that termination under such strategies satisfies
interesting modular properties that does not hold in the non-probabilistic case.
I'm presenting a co-joint work done together with Pascal Lafourcade.