Abstract
Petri games have been introduced as a multi-player game model representing causal memory to address the synthesis of distributed systems. For Petri games with one environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy is EXPTIME-complete. This result forms the basis of the tool AdamSYNT that implements an algorithm for the synthesis of distributed controllers from Petri games. To evaluate the tool, it has been checked on a series of parameterized benchmarks from manufacturing and workflow scenarios.
In this paper, we introduce a new possibility to represent benchmark families for the synthesis of distributed systems modeled with Petri games. It enables the user to specify an entire benchmark family as one parameterized high-level net. We describe example benchmark families as a high-level version of a Petri game and exhibit an instantiation yielding a concrete 1-bounded Petri game. We identify improvements either regarding the size or the functionality of the benchmark families by examining the high-level Petri games.
This work was supported by the German Research Foundation (DFG) through the grant Petri Games (No. 392735815).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bloem, R.P., Gamauf, H.J., Hofferek, G., Könighofer, B., Könighofer, R.: Synthesizing robust systems with RATSY. In: Peled, D.A., Schewe, S. (eds.) Proceedings of First Workshop on Synthesis (SYNT), EPTCS, vol. 84, pp. 47–53 (2012)
Bohy, A., Bruyère, V., Filiot, E., **, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_45
Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. 1, pp. 3–50. Cornell University, Ithaca (1957)
Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272–275. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_25
Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)
Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-77426-6
Finkbeiner, B.: Bounded synthesis for Petri games. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 223–237. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23506-6_15
Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.R.: Symbolic vs. bounded synthesis for Petri games. In: Fisman, D., Jacobs, S. (eds.) Proceedings of Sixth Workshop on Synthesis (SYNT), EPTCS, vol. 202, pp. 19–39 (2017)
Finkbeiner, B., Gieseking, M., Olderog, E.-R.: Adam: causality-based synthesis of distributed systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 433–439. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_25
Finkbeiner, B., Gölz, P.: Synthesis in distributed environments. In: Lokam, S.V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs, vol. 93, pp. 28:1–28:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
Finkbeiner, B., Olderog, E.R.: Petri games: synthesis of distributed systems with causal memory. In: Peron, A., Piazza, C. (eds.) Proceedings of Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF), EPTCS, vol. 161, pp. 217–230 (2014). https://doi.org/10.4204/EPTCS.161.19
Finkbeiner, B., Olderog, E.R.: Petri games: synthesis of distributed systems with causal memory. Inf. Comput. 253(Part 2), 181–203 (2017). https://doi.org/10.1016/j.ic.2016.07.006
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Logic in Computer Science (LICS), pp. 321–330. IEEE (2005). https://doi.org/10.1109/LICS.2005.53
Gastin, P., Lerman, B., Zeitoun, M.: Distributed games with causal memory are decidable for series-parallel systems. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 275–286. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30538-5_23
Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 275–286. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_26
Genrich, H.J., Lautenbach, K.: System modelling with high-level Petri nets. Theor. Comput. Sci. 13, 109–136 (1981). https://doi.org/10.1016/0304-3975(81)90113-4
Güdemann, M., Ortmeier, F., Reif, W.: Formal modeling and verification of systems with self-x properties. In: Yang, L.T., **, H., Ma, J., Ungerer, T. (eds.) ATC 2006. LNCS, vol. 4158, pp. 38–47. Springer, Heidelberg (2006). https://doi.org/10.1007/11839569_4
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1. Springer, Heidelberg (1992). https://doi.org/10.1007/978-3-662-06289-0
Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_29
Jonsson, B.: A model and proof system for asynchronous networks. In: Malcolm, M.A., Strong, H.R. (eds.) Proceedings of Fourth Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 49–58. ACM (1985). https://doi.org/10.1145/323596.323601
Jonsson, B.: Compositional verification of distributed systems. Ph.D. thesis, Department of Computer Systems, Uppsala University, Sweden (1987)
Madhusudan, P., Thiagarajan, P.S., Yang, S.: The MSO theory of connectedly communicating processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 201–212. Springer, Heidelberg (2005). https://doi.org/10.1007/11590156_16
Muscholl, A., Walukiewicz, I.: Distributed synthesis for acyclic architectures. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs, vol. 29, pp. 639–651. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014). https://doi.org/10.4230/LIPIcs.FSTTCS.2014.639
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13, 85–108 (1981)
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Foundations of Computer Science (FOCS), pp. 746–757. IEEE (1990)
Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-69968-9
Reisig, W.: Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-33278-4
Zielonka, W.: Notes on finite asynchronous automata. Theoret. Inform. Appli. (ITA) 21(2), 99–135 (1987)
Acknowledgement
We thank Wolfgang Reisig for suggesting to use high-level Petri nets to represent families of benchmarks during a Dagstuhl Workshop. We also thank two anonymous reviewers for their helpful comments.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Gieseking, M., Olderog, ER. (2021). High-Level Representation of Benchmark Families for Petri Games. In: Olderog, ER., Steffen, B., Yi, W. (eds) Model Checking, Synthesis, and Learning. Lecture Notes in Computer Science(), vol 13030. Springer, Cham. https://doi.org/10.1007/978-3-030-91384-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-91384-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-91383-0
Online ISBN: 978-3-030-91384-7
eBook Packages: Computer ScienceComputer Science (R0)