×

zbMATH — the first resource for mathematics

Petri games: synthesis of distributed systems with causal memory. (English) Zbl 1362.68211
Summary: We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
91A43 Games involving graphs
Software:
MCGP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Finkbeiner, B.; Olderog, E.-R., Petri games: synthesis of distributed systems with causal memory, (Peron, A.; Piazza, C., Proc. Fifth Intern. Symp. on Games, Automata, Logics and Formal Verification (GandALF), EPTCS, vol. 161, (2014)), 217-230
[2] Zielonka, W., Asynchronous automata, (Rozenberg, G.; Diekert, V., Book of Traces, (1995), World Scientific), 205-248
[3] Gastin, P.; Lerman, B.; Zeitoun, M., Distributed games with causal memory are decidable for series-parallel systems, (Proc. FSTTCS, (2004)), 275-286 · Zbl 1117.68448
[4] Madhusudan, P.; Thiagarajan, P. S.; Yang, S., The MSO theory of connectedly communicating processes, (Proc. FSTTCS’05, LNCS, vol. 3821, (2005), Springer), 201-212 · Zbl 1172.68556
[5] Genest, B.; Gimbert, H.; Muscholl, A.; Walukiewicz, I., Asynchronous games over tree architectures, (Proc. ICALP’13, Part II, LNCS, vol. 7966, (2013), Springer), 275-286 · Zbl 1334.68150
[6] Nielsen, M.; Plotkin, G. D.; Winskel, G., Petri nets, event structures and domains, part I, Theor. Comput. Sci., 13, 85-108, (1981) · Zbl 0452.68067
[7] Engelfriet, J., Branching processes of Petri nets, Acta Inform., 28, 6, 575-591, (1991) · Zbl 0743.68106
[8] Esparza, J.; Heljanko, K., Unfoldings - A partial-order approach to model checking, (2008), Springer · Zbl 1153.68035
[9] Stockmeyer, L. J.; Chandra, A. K., Provably difficult combinatorial games, SIAM J. Comput., 8, 2, 151-174, (1979) · Zbl 0421.68044
[10] Reisig, W., Petri nets - an introduction, (1985), Springer · Zbl 0555.68033
[11] Reisig, W., Elements of distributed algorithms - modeling and analysis with Petri nets, (1998), Springer · Zbl 0907.68130
[12] Best, E.; Fernández, C., Nonsequential processes, (1988), Springer · Zbl 0656.68005
[13] Esparza, J., Model checking using net unfoldings, Sci. Comput. Program., 23, 151-195, (1994) · Zbl 0834.68087
[14] Meseguer, J.; Montanari, U.; Sassone, V., Process versus unfolding semantics for place/transition Petri nets, Theor. Comput. Sci., 153, 171-210, (1996) · Zbl 0872.68130
[15] Khomenko, V.; Koutny, M.; Vogler, W., Canonical prefixes of Petri net unfoldings, Acta Inform., 40, 95-118, (2003) · Zbl 1072.68072
[16] Hoare, C. A.R., Communicating sequential processes, (1985), Prentice Hall · Zbl 0637.68007
[17] Olderog, E.-R., Nets, terms and formulas: three views of concurrent processes and their relationship, (1991), Cambridge University Press · Zbl 0741.68002
[18] Chatterjee, K.; Henzinger, M., An \(O(n^2)\) time algorithm for alternating Büchi games, (Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’12, (2012), SIAM), 1386-1399
[19] Katz, G.; Peled, D.; Schewe, S., Synthesis of distributed control through knowledge accumulation, (Proc. CAV, LNCS, vol. 6806, (2011), Springer), 510-525
[20] Mayr, E. W., An algorithm for the general Petri net reachability problem, (Proc. 13th ACM STOC, (1981), ACM), 238-246
[21] Abdulla, P. A.; Bouajjani, A.; d’Orso, J., Deciding monotonic games, (Proc. CSL, LNCS, vol. 2803, (2003), Springer), 1-14 · Zbl 1116.68491
[22] Giua, A., Petri nets as discrete event models for supervisory control, (1992), Rensselaer Polytechnic Institute, PhD thesis
[23] Zhou, Q.; Wang, M.; Dutta, S. P., Generation of optimal control policy for flexible manufacturing cells: a Petri net approach, Int. J. Adv. Manuf. Technol., 10, 59-65, (1995)
[24] Raskin, J.-F.; Samuelides, M.; Begin, L. V., Petri games are monotone but difficult to decide, (2003), Université Libre De Bruxelles, Technical report
[25] Buy, U.; Darabi, H.; Lehene, M.; Venepally, V., Supervisory control of time Petri nets using net unfolding, (Annual International Computer Software and Applications Conference, vol. 2, (2005)), 97-100
[26] Pnueli, A.; Rosner, R., Distributed reactive systems are hard to synthesize, (Proc. FOCS, (1990), IEEE Computer Society Press), 746-757
[27] Walukiewicz, I.; Mohalik, S., Distributed games, (Proc. FSTTCS’03, LNCS, vol. 2914, (2003)), 338-351 · Zbl 1205.68089
[28] Rosner, R., Modular synthesis of reactive systems, (1992), Weizmann Institute of Science Rehovot, Israel, PhD thesis
[29] Kupferman, O.; Vardi, M. Y., Synthesizing distributed systems, (Proc. LICS, (2001), IEEE Computer Society Press), 389-398
[30] Finkbeiner, B.; Schewe, S., Uniform distributed synthesis, (Proc. LICS, (2005), IEEE Computer Society Press), 321-330
[31] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713, (2002) · Zbl 1326.68181
[32] Zielonka, W., Notes on finite asynchronous automata, RAIRO Theor. Inform. Appl., 21, 2, 99-135, (1987) · Zbl 0623.68055
[33] Muscholl, A.; Walukiewicz, I., Distributed synthesis for acyclic architectures, (Raman, V.; Suresh, S. P., Proc. FSTTCS, Leibniz International Proceedings in Informatics (LIPIcs), vol. 29, (2014), Schloss Dagstuhl-Leibniz-Zentrum für Informatik), 639-651 · Zbl 1360.68594
[34] Muscholl, A.; Walukiewicz, I.; Zeitoun, M., A look at the control of asynchronous automata, (Perspectives in Concurrency Theory, (2009), CRC Press) · Zbl 1194.68145
[35] van der Aalst, W. M.P., The application of Petri nets to workflow management, J. Circuits Syst. Comput., 8, 21-66, (1998)
[36] Finkbeiner, B.; Gieseking, M.; Olderog, E.-R., Adam: causality-based synthesis of distributed systems, (Kroening, D.; Pasareanu, C. S., Computer Aided Verification (CAV), Part I, LNCS, vol. 9206, (2015), Springer), 433-439
[37] Finkbeiner, B., Bounded synthesis for Petri games, (Meyer, R.; Platzer, A.; Wehrheim, H., Correct System Design, LNCS, vol. 9360, (2015), Springer), 223-237 · Zbl 1443.68110
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.