# LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue).
If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

## Past Seminars

### Tweaking The Odds -- Parameter Synthesis in Markov Models

- Date
- Wednesday, October 04 2017 at 02:00PM
- Place
- Auditorium Daniel Chemla (Bât. Institut D'Alembert)
- Speaker
- Joost-Pieter Katoen (RWTH Aachen)

A major practical obstacle in probabilistic verification is that all
probabilities (rates) in Markov models have to be fixed. However, at
early development stages, certain system quantities such as failure
rates, reaction speeds, packet loss ratios, etc. are often not -- or at
best partially -- known. This motivates considering parametric models
with transition probabilities specified as functions over parameters.

This talks considers parameter synthesis: Given a parametric Markov
model, what are the parameter values for which a given property meets a
given threshold? For example, what failure rates are tolerable ensuring
that the likelihood of a system breakdown is below 0,00000001?

We present an exact SMT-approach and discuss a simple approximation
whose beauty is its applicability to Markov chains and MDPs. Its usage
on finding minimal recovery times for randomized self-stabilizing
algorithms is shown. Finally, we indicate how geometric programming can
be used to do synthesis for multiple objectives on parametric MDPs.