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

Qualitative Analysis of Synchronizing Probabilistic Systems

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

 Mahsa Shirmohammadi
Date
Le mardi 02 décembre 2014 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Mahsa Shirmohammadi (LSV, ENS Cachan & Université Libre de Bruxelles)

Markov decision processes (MDPs) are finite-state probabilistic systems with both strategic and random choices, hence well-established to model the interactions between a controller and its randomly responding environment. An MDP is viewed as a 1/2-player stochastic game played in rounds when the controller chooses an action, and the environment chooses a successor according to a fixed probability distribution.

Recently, MDPs have been viewed as generators of sequences of probability distributions over states, called the distribution-outcome. We introduce synchronizing conditions defined on distribution-outcomes, which intuitively requires that some (group of) state(s) tend to accumulate all the probability mass. We consider the following modes of synchronization: the always mode where all distributions of the distribution-outcome must be synchronized, the eventually mode where some distributions must be synchronized, the weakly mode where infinitely many distributions must be synchronized, and the strongly mode where all but finitely many distributions must be synchronized.

For each synchronizing mode, we study three winning modes: sure, almost-sure and limit-sure. In this talk, we present the various synchronization modes and winning modes, as well as an overview of the key properties for their analysis.

We also give hints on synchronization in probabilistic automata (PAs), that are kind of MDPs where controllers are restricted to use only word-strategies; i.e. no ability to observe the history of the system execution, but the number of choices made so far.

This talk will be concluded by introducing different variants of synchronization for timed and weighted automata including synchronization to a unique location with possibly different clock valuation or accumulated weight, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints).

The talk is based on Mahsa Shirmohammadi's PhD thesis, which is carried out jointly in ULB (Belgium) and LSV, ENS Cachan (France). The official defense takes place in Brussels.


À 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