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.