Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Tweaking The Odds -- Parameter Synthesis in Markov Models

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Joost-Pieter   Katoen
Date
Le mercredi 04 octobre 2017 à 14:00
Lieu
Auditorium Daniel Chemla (Bât. Institut D'Alembert)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents