Ent?te

Logo du LIFL

Depuis le 1er janvier 2015 le LIFL et le LAGIS forment le laboratoire CRIStAL

  1. Actualités

Séminaire de

Sylvain Pradalier

16 décembre 2010
Amphi Turing, Bât M3

Optimisation of markov processes as an extension of stochastic verification

The verification problem consists in answering whether a given model satisfies a given behavioural property. Verification is a problem of high interest because it certifies that the behaviour of a system is correct, in the sense that it satisfies a given specification. It has been studied in most settings, and in particular the probabilistic and stochastic ones, where a model is respectively a Discrete Time Markov Chain or a Continuous Time Markov Chain, and where properties are described using temporal logic such as pCTL or CSL.

Verification is also key in the process of designing a machine (be it mechanical or biological) as it permits to know whether the expected behaviours do occur in the model of the machine. However when faced with a failure, i.e. the model of ones machine does not behave as expected, one is left helpless: knowing that a property is not verified in a model does not help us to understand how to modify the model in order to satisfy the property.

In this talk, I shall present the constraint-solving approach recently designed in the CONTRAINTES team in order to cope with this issue, and how I was able to adapt to the stochastic setting. The key ingredient is to go from a yes/no notion of satisfaction to a continuous one. Given a system S and a behavioural property expressed as a formula phi, we define a continuous violation degree d(phi,S) equals to 0 if S satisfies phi and that otherwise measures how S is far from satisfying phi. This degree can then be used as a fitness function in order to perform optimizations and parameter searches with respect to behavioural properties.


First I present the approach depicted above, then I recall the usual techniques used for the verification of stochastic systems and finally I present how to adapt this optimization techniques to the stochastic settings.

Ours

UMR 8022 - Laboratoire d'Informatique Fondamentale de Lille - Copyright © 2012 Sophie TISON - Crédits & Mentions légales

Page respectant XHTML et CSS.

Pour tout commentaire / Comments and remarks : webmaster