Affiliations: [a] Department of Computational & Systems Biology, University of Pittsburgh, Pittsburgh, USA | [b] State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Zhong Guan Cun, Beijing 100190, P.R. China
Correspondence:
[*]
Address for correspondence: Department of Computational & Systems Biology University of Pittsburgh, Pittsburgh, USA
Note: [†] Partially supported by the NIGMS of the NIH under award number P41GM103712.
Note: [‡] Supported by the National 973 Program of China under Grant 2014CB340701 and by the Natural Science Foundation of Beijing under Grant 4202076.
Abstract: We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics.
