Abstract
In concurrent systems, the choice of executing the next transition depends both on the timing between the agents that make independent or collaborative interactions available, and on the conflicts (nondeterministic choices) with other transitions. This creates a challenging modeling and implementation problem. When the system needs to make also probabilistic choices, the situation becomes even more complicated. We use the model of Petri nets to demonstrate the modeling and implementation problem. The proposed solution involves adding sequential observers called agents to the Petri net structure. Distributed probabilistic choices are facilitated in the presence of concurrency and nondeterminism, by selecting agents that make the choices, while guaranteeing that their view is temporarily stable. We provide a distributed scheduling algorithm for implementing a system that allows distributed probabilistic choice.
The first author is supported by the FP7 MEALS and SENSATION projects. The second author is supported by ISF grant 126/12 “Efficient Synthesis of Control for Concurrent Systems”.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abbes, S.: The (True) Concurrent Markov Property and Some Applications to Markov Nets. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 70–89. Springer, Heidelberg (2005)
Albanese, M.: A constrained probabilistic Petri net framework for human activity detection in video. IEEE Trans. on Multimedia 10(6), 982–996 (2008)
Andrés, M.E., Palamidessi, C., van Rossum, P., Sokolova, A.: Information hiding in probabilistic concurrent systems. TCS 412(28), 3072–3089 (2011)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
Beccuti, M., Franceschinis, G., Haddad, S.: Markov Decision Petri Net and Markov Decision Well-Formed Net Formalisms. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 43–62. Springer, Heidelberg (2007)
Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Computers 57(10), 1315–1330 (2008)
Cheung, L., Lynch, N.A., Segala, R., Vaandrager, F.W.: Switched PIOA: Parallel composition via distributed scheduling. TCS 365(1-2), 83–108 (2006)
de Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. In: PROBMIV, pp. 19–32 (1999)
Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and Composition in a Stochastic World. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21–39. Springer, Heidelberg (2010)
Georgievska, S., Andova, S.: Probabilistic may/must testing: retaining probabilities by restricted schedulers. Formal Asp. Comput. 24(4-6), 727–748 (2012)
Giro, S., D’Argenio, P.R.: On the expressive power of schedulers in distributed probabilistic systems. ENTCS 253(3), 45–71 (2009)
Katoen, J.-P.: GSPNs revisited: Simple semantics and new analysis algorithms. In: Application of Concurrency to System Design, pp. 6–11 (2012)
Katz, G., Peled, D.: Code Mutation in Verification and Automatic Code Correction. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 435–450. Springer, Heidelberg (2010)
Katz, G., Peled, D., Schewe, S.: Synthesis of Distributed Control through Knowledge Accumulation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 510–525. Springer, Heidelberg (2011)
Kudlek, M.: Probability in Petri nets. Fund. Inf. 67(1-3), 121–130 (2005)
Lehmann, D.J., Rabin, M.O.: On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In: POPL, pp. 133–138 (1981)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Observing branching structure through probabilistic contexts. SIAM J. Comp. 37(4), 977–1013 (2007)
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley (1995)
Mazurkiewicz, A.: Introduction to trace theory. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces. World Scientific (1995)
Pérez, J.A., Corchuelo, R., Toro, M.: An order-based algorithm for multiparty synchronization. Concurrency - Practice and Experience 16(12), 1173–1206 (2004)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (2005)
Rozenberg, G., Thiagarajan, P.S.: Petri Nets: Basic Notions, Structure, Behaviour. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 585–668. Springer, Heidelberg (1986)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)
Taubenfeld, G.: Synchronization Algorithms for Concurrent Programming. Prentice Hall (2006)
Varacca, D., Nielsen, M.: Probabilistic Petri nets and Mazurkiewicz equivalence (2003) (unpublished manuscript)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katoen, JP., Peled, D. (2013). Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems. In: Felleisen, M., Gardner, P. (eds) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science, vol 7792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37036-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-37036-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37035-9
Online ISBN: 978-3-642-37036-6
eBook Packages: Computer ScienceComputer Science (R0)