# 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

### Deterministically Communicating MDPs

- Date
- Tuesday, May 28 2013 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Madhavan Mukund (Chennai Mathematical Institute)

The formal verification of large probabilistic models remains a
challenge. To better exploit the concurrency that is often present,
we introduce deterministically communicating Markov Decision
Processes (DMDPs) in which the components synchronize to determine
the local probability distribution for their next moves. Two
simultaneously enabled synchronizations are guaranteed to involve
disjoint sets of MDPs. As a result, one can define the global
behavior of a DMDP as a Markov chain without having to introduce
schedulers. In order to cope with the exponential size of this
Markov chain in the number of components, we define an interleaved
semantics in terms of the local synchronization actions. The network
structure induces an independence relation on these actions. Using
Mazurkiewicz trace theory, we establish a strong relationship
between the interleaved semantics and the global Markov chain
semantics. This allows us to construct a natural probability
measure with respect to the interleaved semantics. Consequently,
verification of DMDPs can often be efficiently carried out using the
interleaved semantics without having to construct the global Markov
chain.

To illustrate this we develop a statistical model checking (SMC)
procedure under the interleaved semantics and use it to verify a
probabilistic algorithm for leader election over an anonymous
ring. Our method can easily cope with a ring containing 50
processes while the same SMC procedure applied to the global Markov
chain (using PRISM) can only deal with rings containing at most 3
processes.

This is joint work with Sumit Kumar Jha, Ratul Saha and
P.S. Thiagarajan.