Distributed markov chains

Ratul Saha, Javier Esparza, Sumit Kumar Jha, Madhavan Mukund, P. S. Thiagarajan

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations


The formal verification of large probabilistic models is challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a class of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key property of this class is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. As a result, such a network of agents can be viewed as a succinct and distributed presentation of a large global Markov chain. A rich class of Markov chains can be represented this way.

We use partial-order notions to define an interleaved semantics that can be used to efficiently verify properties of the global Markov chain represented by the network. To demonstrate this, we develop a statistical model checking (SMC) procedure and use it to verify two large networks of probabilistic agents.

We also show that our model, called distributed Markov chains (DMCs), is closely related to deterministic cyclic negotiations, a recently introduced model for concurrent systems [10]. Exploiting this connection we show that the termination of a DMC that has been endowed with a global final state can be checked in polynomial time.

Original languageEnglish
Title of host publicationVerification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings
EditorsDeepak D’Souza, Akash Lal, Kim Guldstrand Larsen
PublisherSpringer Verlag
Number of pages18
ISBN (Electronic)9783662460801
StatePublished - 2015
Event16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015 - Mumbai, India
Duration: 12 Jan 201514 Jan 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015


Dive into the research topics of 'Distributed markov chains'. Together they form a unique fingerprint.

Cite this