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

- 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.