Sylvain Pradalier (Inria Rocquencourt)

Approximation, optimization and synthesis of stochastic processes.

Abstract:

In the last decade, several independent works investigated approximate reasoning. I focus on two lines of work. The first approach, mainly due to J.Desharnais and P.Panangaden, investigates the approximation of probabilistic processes using a notion of distance relaxing probabilistic bisimulation. It is grounded on a continuous satisfaction degree of a formula by a model and has given birth to several approximation techniques. The second approach, due to the Contraintes team at Inria Rocquencourt, extends model-checking to the problem of computing the parameters for which a model satisfies a formula. It is grounded on a continuous violation degree of a formula by a model and has been illustrated through optimization and synthesis of biochemical processes.

I shall present the following contributions. I identify and highlight the important aspects shared by the two approaches. Then I point out a result providing the key ingredients of both approaches: a characterization of stochastic bisimulation by a negation-free fragment of the continuous stochastic logic CSL. Finally I bridge the gap between the two approaches by adapting them to the stochastic settings and to this fragment of CSL, thus providing a setting to compare and relate them.

The expected applications of this work concern the approximation, optimization and synthesis of stochastic processes, among which the concurrent processes and the biochemical processes are in pole-position.