{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T04:08:55Z","timestamp":1750392535489,"version":"3.41.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031939297","type":"print"},{"value":"9783031939303","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-93930-3_10","type":"book-chapter","created":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:27:19Z","timestamp":1750346839000},"page":"159-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parameter Synthesis for\u00a0Families of\u00a0Markov Chains with\u00a0an\u00a0Application to\u00a0Multi-agent Systems Privacy"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Spegni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Spalazzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Rosetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,20]]},"reference":[{"issue":"9","key":"10_CR1","doi-asserted-by":"publisher","first-page":"6569","DOI":"10.1007\/s10489-021-02658-y","volume":"51","author":"A Abate","year":"2021","unstructured":"Abate, A., et al.: Rational verification: game-theoretic verification of multi-agent systems. Appl. Intell. 51(9), 6569\u20136584 (2021). https:\/\/doi.org\/10.1007\/s10489-021-02658-y","journal-title":"Appl. Intell."},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00446-017-0302-6","volume":"31","author":"B Aminof","year":"2018","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distrib. Comput. 31, 187\u2013222 (2018)","journal-title":"Distrib. Comput."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.P., Stupinsk\u1ef3, \u0160.: Paynt: a tool for inductive synthesis of probabilistic programs. In: International Conference on Computer Aided Verification, pp. 856\u2013869. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_40"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-63406-3_1","volume-title":"Formal Methods and Software Engineering","author":"J Arias","year":"2020","unstructured":"Arias, J., Budde, C.E., Penczek, W., Petrucci, L., Sidoruk, T., Stoelinga, M.: Hackers vs. security: attack-defence trees as asynchronous multi-agent systems. In: Lin, S.-W., Hou, Z., Mahony, B. (eds.) ICFEM 2020. LNCS, vol. 12531, pp. 3\u201319. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63406-3_1"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Arming, S., Bartocci, E., Sokolova, A.: SEA-PARAM: exploring schedulers in parametric MDPs. Electron. Proc. Theor. Comput. Sci. 250, 25\u201338 (2017). https:\/\/doi.org\/10.4204\/EPTCS.250.3,http:\/\/arxiv.org\/abs\/1707.04122v1","DOI":"10.4204\/EPTCS.250.3,"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. Springer, Cham (2008). https:\/\/doi.org\/10.1093\/comjnl\/bxp025","DOI":"10.1093\/comjnl\/bxp025"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-66335-7_8","volume-title":"Quant. Eval. Syst.","author":"M Baldi","year":"2017","unstructured":"Baldi, M., et al.: A probabilistic small model theorem to assess confidentiality of dispersed cloud storage. In: Bertrand, N., Bortolussi, L. (eds.) Quant. Eval. Syst., pp. 123\u2013139. Springer, Cham (2017)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Baldi, M., Chiaraluce, F., Senigagliesi, L., Spalazzi, L., Spegni, F.: Security in heterogeneous distributed storage systems: a practically achievable information-theoretic approach. In: 2017 IEEE Symposium on Computers and Communications (ISCC), pp. 1021\u20131028. IEEE (2017)","DOI":"10.1109\/ISCC.2017.8024659"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Baldi, M., Cucchiarelli, A., Senigagliesi, L., Spalazzi, L., Spegni, F.: Parametric and probabilistic model checking of confidentiality in data dispersal algorithms. In: Proceedings of HPCS 2016: Interernational Conference on High Performance Computing & Simulation, pp. 476\u2013483 (2016).https:\/\/doi.org\/10.1109\/HPCSim.2016.7568373","DOI":"10.1109\/HPCSim.2016.7568373"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Baldi, M., Maturo, N., Montali, E., Chiaraluce, F.: AONT-LT: a data protection scheme for cloud and cooperative storage systems. In: Proceedings of HPCS 2014: International Conference on High Performance Computing & Simulation, pp. 566\u2013571 (2014)","DOI":"10.1109\/HPCSim.2014.6903736"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J.P., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 410\u2013429. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Belardinelli, F., Jamroga, W., Mittelmann, M., Murano, A.: Strategic abilities of forgetful agents in stochastic environments. In: Marquis, P., Son, T.C., Kern-Isberner, G. (eds.) Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, pp. 726\u2013731 (2023)","DOI":"10.24963\/kr.2023\/71"},{"key":"10_CR13","unstructured":"Belardinelli, F., Jamroga, W., Mittelmann, M., Murano, A.: Verification of stochastic multi-agent systems with forgetful strategies. In: Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, pp. 160\u2013169 (2024)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of broadcasting multi-agent systems against an epistemic strategy logic. In: IJCAI, vol.\u00a017, pp. 91\u201397 (2017)","DOI":"10.24963\/ijcai.2017\/14"},{"key":"10_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103302","volume":"285","author":"F Belardinelli","year":"2020","unstructured":"Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with public actions against strategy logic. Artif. Intell. 285, 103302 (2020)","journal-title":"Artif. Intell."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Berthon, R., Katoen, J., Mittelmann, M., Murano, A.: Natural strategic ability in stochastic multi-agent systems. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pp. 17308\u201317316. AAAI Press (2024)","DOI":"10.1609\/aaai.v38i16.29678"},{"key":"10_CR17","unstructured":"Boureanu, I., Kouvaros, P., Lomuscio, A.: Verifying security properties in unbounded multiagent systems. In: Proceedings of the 2016 International Confernce on Autonomous Agents & Multiagent Systems, pp. 1209\u20131217 (2016)"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: Profeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30, 45\u201375 (2018)","journal-title":"Formal Aspects Comput."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282\u2013299. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_18","DOI":"10.1007\/978-3-319-23404-5_18"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"10_CR22","unstructured":"Freund, J., Jones, J.: Measuring and Managing Information Risk: A FAIR Approach. Butterworth-Heinemann (2014)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Greenstadt, R., Grosz, B., Smith, M.D.: SSDPOP: improving the privacy of DCOP with secret sharing. In: Proceedings of the 6th International Joint Conference on Autonomous Agents and Multiagent Systems, pp.\u00a01\u20133 (2007)","DOI":"10.1145\/1329125.1329333"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transfer 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"10_CR25","unstructured":"Hansen, E., Bernstein, D., Zilberstein, S.: Dynamic programming for partially observable stochastic games. In: Proceedings of the National Conference on Artificial Intelligence (2000), pp. 709\u2013715 (2004). http:\/\/www.aaai.org\/Papers\/AAAI\/2004\/AAAI04-112.pdf"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"He, L., Liu, G., Zhou, M.: Petri-net-based model checking for privacy-critical multiagent systems. IEEE Trans. Comput. Soc. Syst. (2022)","DOI":"10.1109\/TCSS.2022.3164052"},{"key":"10_CR27","doi-asserted-by":"publisher","DOI":"10.1002\/9781119162315","volume-title":"How to Measure Anything in Cybersecurity Risk","author":"DW Hubbard","year":"2016","unstructured":"Hubbard, D.W., Seiersen, R.: How to Measure Anything in Cybersecurity Risk. Wiley, Hoboken (2016)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis in Markov models: a gentle survey. Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, pp. 407\u2013437 (2022)","DOI":"10.1007\/978-3-031-22337-2_20"},{"key":"10_CR29","unstructured":"Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: Globerson, A., Silva, R. (eds.) Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence, UAI 2018, Monterey, California, USA, August 6-10, 2018, pp. 519\u2013529. AUAI Press (2018)"},{"key":"10_CR30","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jcss.2021.02.006","volume":"119","author":"S Junges","year":"2021","unstructured":"Junges, S., Katoen, J.P., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR31","unstructured":"Knuth, D.: The complexity of nonuniform random number generation, Algorithms and Complexity, New Directions and Results, pp. 357\u2013428 (1976)"},{"key":"10_CR32","unstructured":"Kouvaros, P., Lomuscio, A., Pirovano, E., Punchihewa, H.: Formal verification of open multi-agent systems. In: Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems, pp. 179\u2013187 (2019)"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Krawczyk, H.: Secret sharing made short. In: Annual International Cryptology Conference, pp. 136\u2013146. Springer (1993)","DOI":"10.1007\/3-540-48329-2_12"},{"issue":"1","key":"10_CR34","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93\u2013109 (2007)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"10_CR35","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/MIC.2016.45","volume":"20","author":"M Li","year":"2016","unstructured":"Li, M., Qin, C., Li, J., Lee, P.P.: CDstore: toward reliable, secure, and cost-efficient cloud storage via convergent dispersal. IEEE Internet Comp. 20(3), 45\u201353 (2016)","journal-title":"IEEE Internet Comp."},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Littman, M.L.: Markov games as a framework for multi-agent reinforcement learning. In: Machine Learning Proceedings 1994, pp. 157\u2013163 (1994). http:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9781558603356500271","DOI":"10.1016\/B978-1-55860-335-6.50027-1"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Llerena, Y.R.S., Su, G., Rosenblum, D.S.: Probabilistic model checking of perturbed mdps with applications to cloud computing. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. ESEC\/FSE 2017, pp. 454\u2013464. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3106237.3106301","DOI":"10.1145\/3106237.3106301"},{"key":"10_CR38","unstructured":"Rangarao, D., Gucer, V.: IBM cloud object storage concepts and architecture (2017). http:\/\/www.redbooks.ibm.com\/redpapers\/pdfs\/redp5435.pdf"},{"key":"10_CR39","unstructured":"Resch, J., Plank, J.: AONT-RS: blending security and performance in dispersed storage systems. In: Proceedings of 9th FAST Conference (2011)"},{"issue":"11","key":"10_CR40","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1145\/359168.359176","volume":"22","author":"A Shamir","year":"1979","unstructured":"Shamir, A.: How to share a secret. Commun. ACM 22(11), 612\u2013613 (1979)","journal-title":"Commun. ACM"},{"key":"10_CR41","doi-asserted-by":"crossref","unstructured":"Shen, L., Feng, S., Sun, J., Li, Z., Wang, G., Liu, X.: Clouds: a multi-cloud storage system with multi-level security. In: Proceedings of the International Confernce on Algorithms and Architectures for Parallel Processing, pp. 703\u2013716. Springer (2015)","DOI":"10.1007\/978-3-319-27137-8_51"},{"key":"10_CR42","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/j.tcs.2019.12.026","volume":"813","author":"L Spalazzi","year":"2020","unstructured":"Spalazzi, L., Spegni, F.: Parameterized model checking of networks of timed automata with Boolean guards. Theoret. Comput. Sci. 813, 248\u2013269 (2020)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR43","unstructured":"Tabatabaei, M., Jamroga, W.: Playing to learn, or to keep secret: alternating-time logic meets information theory. arXiv preprint arXiv:2303.00067 (2023)"},{"key":"10_CR44","unstructured":"Tabbara, B., Garg, P.: Shared community storage network (2016). https:\/\/patents.google.com\/patent\/US7869383B2\/en. uS Patent 9,344,378 B2"}],"container-title":["Lecture Notes in Computer Science","Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93930-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:27:37Z","timestamp":1750346857000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93930-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031939297","9783031939303"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93930-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"20 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"EUMAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Conference on Multi-Agent Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"eumas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/euramas.github.io\/eumas2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}