A Theory of Distributed Markov Chains

• Autorzy: Thiagarajan P. S. , Yang Shaofa

Identyfikatory

DOI

10.3233/FI-2020-1958

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Markov processes; Petri nets; statistical models; synchronization; logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 175, nr 1-4
• Strony: 301--325
• Opis fizyczny: Bibliogr. 35 poz., rys.

Twórcy

autor

Thiagarajan P. S.

• Department of Computational & Systems Biology, University of Pittsburgh, Pittsburgh, USA

autor

Yang Shaofa

• State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Zhong Guan Cun, Beijing 100190, P.R. China

Bibliografia

• [1] Saha R, Esparza J, Jha SK, Mukund M, Thiagarajan PS. Distributed Markov Chains. In: Proc. of VMCAI 2015, LNCS 8931. Springer, 2015 pp. 117-134. Section 8 of the conference paper — depending crucially on the relationship between DMCs and the formalism of deterministic cyclic negotiations developed by Esparza et al. — contains a bug which was caught after the paper was published. A corrected version in which this material has been removed together with an explanation of the bug is available as a technical report at: www.cmi.ac.in/~madhavan/papers/pdf/dmcs-techreport-corrected.pdf.
• [2] Silberschatz A, Galvin PB, Gagne G. Operating System Concepts, 10th Edition. Wiley, 2018. ISBN:978-1-119-32091-3.
• [3] Hahne EL. Round-robin scheduling for max-min fairness in data networks. IEEE Journal on Selected Areas in Communications, 1991. 9(7):1024-1039. doi:10.1109/49.103550.
• [4] Saha R. Quantitative Model Checking of Distributed Probabilistic Systems. Ph.D. thesis, National Univ. of Singapore, 2017. URL http://scholarbank.nus.edu.sg/handle/10635/138180.
• [5] PRISM. Case studies, www.prismmodelchecker.org/casestudies.
• [6] Größer M, Baier C. Partial Order Reduction for Markov Decision Processes: A Survey. In: Proc. of FMCO 2005, LNCS 4111. 2005 pp. 408-427. doi:10.1007/11804192_19.
• [7] Baier C, de Alfaro L, Forejt V, Kwiatkowska M. Model Checking Probabilistic Systems. In: Handbook of Model Checking, 2018 pp. 963-999. doi:10.1007/978-3-319-10575-8_28.
• [8] Younes HLS. Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2004. ISBN:978-0-496-93475-1.
• [9] Best E. Structure Theory of Petri Nets: The Free Choice Hiatus. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, LNCS 254. 1986 pp. 168-205. doi:10.1007/BFb0046840.
• [10] McMillan KL. A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des., 1995. 6(1):45-65. doi:10.1007/BF01384314.
• [11] Baier C, Hermanns H, Katoen J. The 10, 000 Facets of MDP Model Checking. In: Computing and Software Science - State of the Art and Perspectives, 2019 pp. 420-451. doi:10.1007/978-3-319-91908-9_21.
• [12] Díaz Á F, Baier C, Earle CB, Fredlund L. Static Partial Order Reduction for Probabilistic Concurrent Systems. In: Proc. of QEST 2012 pp. 104-113. doi:10.1109/QEST.2012.22.
• [13] Bogdoll J, Fioriti LMF, Hartmanns A, Hermanns H. Partial Order Methods for Statistical Model Checking and Simulation. In: Proc. of Joint FMOODS 2011 and FORTE 2011, vol. 6722 LNCS. 2011 pp. 59-74. doi:10.1007/978-3-642-21461-5_4.
• [14] Fox G, Stan D, Hermanns H. Syntactic Partial Order Compression for Probabilistic Reachability. In: Proc. of VMCAI 2019, vol. 11388 LNCS. 2019 pp. 446-467. doi:10.1007/978-3-030-11245-5_21.
• [15] Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Springer, 1995. ISBN:978-3-540-60761-8.
• [16] Abbes S, Benveniste A. True-concurrency probabilistic models: Markov nets and a law of large numbers. Theor. Comput. Sci., 2008. 390(2-3):129-170. doi:10.1016/j.tcs.2007.09.018.
• [17] Abbes S, Benveniste A. True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures. Inf. Comput., 2006. 204(2):231-274. doi:10.1016/j.ic.2005.10.001.
• [18] Varacca D, Völzer H, Winskel G. Probabilistic event structures and domains. Theor. Comput. Sci., 2006. 358(2-3):173-199. doi:10.1016/j.tcs.2006.01.015.
• [19] Haar S. Probabilistic Cluster Unfoldings. Fundam. Inform., 2002. 53(3-4):281-314.
• [20] Völzer H. Randomized Non-sequential Processes. In: Larsen KG, Nielsen M (eds.), Proc. of CONCUR 2001, vol. 2154 LNCS. Springer, 2001 pp. 184-201. doi:10.1007/3-540-44685-0_13.
• [21] Abbes S, Benveniste A. Concurrency, σ-Algebras, and Probabilistic Fairness. In: Proc. of FOSSACS 2009, vol. 5504 LNCS, 2009 pp. 380-394. doi:10.1007/978-3-642-00596-1_27.
• [22] Jesi S, Pighizzini G, Sabadini N. Probabilistic Asynchronous Automata. Math. Systems Theory, 1996. 29(1):5-31. doi:10.1007/BF01201811.
• [23] Norris JR. Markov Chains. Cambridge Univ. Press, 1998. ISBN:978-0-521-63396-3.
• [24] Baier C, Katoen JP. Principles of Model Checking. MIT Press, 2008. ISBN:978-0-262-02649-9.
• [25] Diekert V, Rozenberg G. The Book of Traces. World Scientific, Singapore, 1995. ISBN:978-9-814-50126-2.
• [26] Durrett R. Probability: Theory and Examples. World Scientific, Singapore, 3rd edition, 2005. ISBN:978-0-534-42441-1.
• [27] Gastin P. Infinite Traces. In: Semantics of Systems of Concurrent Processes, Proc. of LITP Spring School on Theoretical Computer Science 1990, vol. 469 LNCS. Springer, 1990 pp. 277-308. doi:10.1007/3-540-53479-2_12.
• [28] Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P. A Bayesian approach to model checking biological systems. In: Proc. of Computational Methods in Systems Biology (CMSB) 2009, vol. 5688 LNCS. 2009 pp. 218-234. doi:10.1007/978-3-642-03845-7_15.
• [29] Amparore EG, Beccuti M, Donatelli S. (Stochastic) Model Checking in GreatSPN. In: Ciardo G, Kindler E (eds.), Proc. of PETRI NETS 2014, vol. 8489 LNCS. Springer, 2014 pp. 354-363. doi:10.1007/978-3-319-07734-5_19.
• [30] Desel J, Esparza J. Reachability in Cyclic Extended Free-Choice Systems. Theor. Comput. Sci., 1993. 114(1):93-118. doi:10.1016/0304-3975(93)90154-L.
• [31] Desel J, Esparza J. Free Choice Petri Nets. Cambridge Univ. Press, 1995. doi:10.1017/CBO9780511526558.
• [32] Nielsen M, Plotkin G, Winskel G. Petri nets, event structures and domains, Part 1. Theor. Comp. Sci., 1981. 13:85-108. doi:10.1016/0304-3975(81)90112-2.
• [33] Winskel G. Event Structures. In: Petri Nets: Applications and Relationships to Other Models of Concurrency, LNCS 255. Springer, 1987 pp. 325-392. doi:10.1007/3-540-17906-2_31.
• [34] Clarke EM, Grumberg O, Peled DA. Model checking. MIT Press, 2001. ISBN:978-0-262-03883-6.
• [35] Esparza J, Heljanko K. Unfoldings - A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2008. doi:10.1007/978-3-540-77426-6.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).