LSV Seminar

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.