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
Qualitative Analysis of Synchronizing Probabilistic Systems
- Date
- Tuesday, December 02 2014 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.