### Distributed Markov Chains

R Saha, J Esparza, S K Jha, M Mukund and P S Thiagarajan

*Proc. VMCAI 2015*, Springer LNCS 8931 (2015) 117-134.

*© Springer-Verlag Berlin Heidelberg*

### Abstract

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. 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.