Distributed Markov chains

Saha, Ratul ; Esparza, Javier ; Jha, Sumit Kumar ; Mukund, Madhavan ; Thiagarajan, P. S. (2015) Distributed Markov chains In: 16th International Conference, VMCAI 2015, 12-14 Jan 2015, Mumbai, India.

Full text not available from this repository.

Official URL: https://link.springer.com/chapter/10.1007/978-3-66...

Related URL: http://dx.doi.org/10.1007/978-3-662-46081-8_7


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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Markov Chain; Probability Measure; Global State; Maximal Step; Trajectory Space
ID Code:114106
Deposited On:25 May 2018 04:55
Last Modified:25 May 2018 04:55

Repository Staff Only: item control page