{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:16:32Z","timestamp":1774984592395,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005760","name":"University of Gothenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005760","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interaction interfaces by forming collectives and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. In this article, we provide a modelling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK (please find the associated toolkit repository here:<jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/dsynma\/recipe\">https:\/\/github.com\/dsynma\/recipe<\/jats:ext-link>). R-CHECK supports a high-level input language with matching enumerative and symbolic semantics and provides modelling convenience for features such as reconfiguration, coalition formation, and self-organisation. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.<\/jats:p>","DOI":"10.1007\/s10009-023-00729-8","type":"journal-article","created":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T13:02:13Z","timestamp":1698930133000},"page":"765-784","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Language support for verifying reconfigurable interacting systems"],"prefix":"10.1007","volume":"25","author":[{"given":"Yehia Abd","family":"Alrahman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaun","family":"Azzopardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Di Stefano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,11,2]]},"reference":[{"issue":"2","key":"729_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-021-09521-x","volume":"35","author":"Y. Abd Alrahman","year":"2021","unstructured":"Abd Alrahman, Y., Piterman, N.: Modelling and verification of reconfigurable multi-agent systems. Auton. Agents Multi Agent Syst. 35(2), 47 (2021). https:\/\/doi.org\/10.1007\/s10458-021-09521-x","journal-title":"Auton. Agents Multi Agent Syst."},{"key":"729_CR2","doi-asserted-by":"publisher","unstructured":"Abd Alrahman, Y., Vieira, H.T.: A coordination protocol language for power grid operation control. J. Log. Algebraic Methods Program. 109 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100487","DOI":"10.1016\/j.jlamp.2019.100487"},{"key":"729_CR3","doi-asserted-by":"publisher","unstructured":"Abd Alrahman, Y., De Nicola, R., Loreti, M.: A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. 268 (2019). https:\/\/doi.org\/10.1016\/j.ic.2019.104457","DOI":"10.1016\/j.ic.2019.104457"},{"key":"729_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102428","volume":"192","author":"Y. Abd Alrahman","year":"2020","unstructured":"Abd Alrahman, Y., De Nicola, R., Loreti, M.: Programming interactions in collective adaptive systems by relying on attribute-based communication. Sci. Comput. Program. 192, 102428 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102428","journal-title":"Sci. Comput. Program."},{"key":"729_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.5555\/3398761.3398768","volume-title":"Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201920","author":"Y. Abd Alrahman","year":"2020","unstructured":"Abd Alrahman, Y., Perelli, G., Piterman, N.: Reconfigurable interaction for MAS modelling. In: Seghrouchni, A.E.F., Sukthankar, G., An, B., Yorke-Smith, N. (eds.) Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201920, Auckland, New Zealand, May 9-13, 2020, pp.\u00a07\u201315. International Foundation for Autonomous Agents and Multiagent Systems (2020). https:\/\/doi.org\/10.5555\/3398761.3398768"},{"key":"729_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-031-19759-8_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings, Part III","author":"Y. Abd Alrahman","year":"2022","unstructured":"Abd Alrahman, Y., Azzopardi, S., Piterman, N.: Model checking reconfigurable interacting systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Proceedings, Part III, Rhodes, Greece, October 22-30, 2022. Lecture Notes in Computer Science, vol.\u00a013703, pp.\u00a0373\u2013389. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-19759-8_23"},{"key":"729_CR7","doi-asserted-by":"publisher","first-page":"1518","DOI":"10.5555\/3535850.3536020","volume-title":"Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201922","author":"Y. Abd Alrahman","year":"2022","unstructured":"Abd Alrahman, Y., Azzopardi, S., Piterman, N.: R-check: a model checker for verifying reconfigurable mas. In: Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201922, pp.\u00a01518\u20131520. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2022). https:\/\/doi.org\/10.5555\/3535850.3536020"},{"key":"729_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-031-17715-6_5","volume-title":"Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Proceedings","author":"Y. Abd Alrahman","year":"2022","unstructured":"Abd Alrahman, Y., Martel, M., Piterman, N.: A PO characterisation of reconfiguration. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Proceedings, Tbilisi, Georgia, September 27\u201329, 2022. Lecture Notes in Computer Science, vol.\u00a013572, pp.\u00a042\u201359. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_5"},{"key":"729_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling, Specification and Verification","author":"L. Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007). https:\/\/doi.org\/10.1017\/CBO9780511814105"},{"issue":"1","key":"729_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Form. Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Form. Methods Syst. Des."},{"issue":"5","key":"729_CR11","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"729_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/SEFM.2006.27","volume-title":"3th International Conference on Software Engineering and Formal Methods (SEFM)","author":"A. Basu","year":"2006","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: 3th International Conference on Software Engineering and Formal Methods (SEFM), pp.\u00a03\u201312. IEEE, Pune (2006). https:\/\/doi.org\/10.1109\/SEFM.2006.27"},{"issue":"10","key":"729_CR13","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S. Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008). https:\/\/doi.org\/10.1109\/TC.2008.26","journal-title":"IEEE Trans. Comput."},{"key":"729_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, Part II","author":"O. Bunte","year":"2019","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mcrl2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, Part II, Prague, Czech Republic, April 6-11, 2019. Lecture Notes in Computer Science, vol.\u00a011428, pp.\u00a021\u201339. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"729_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings","author":"A. Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings, Berkeley, CA, USA, July 7-13, 2012. Lecture Notes in Computer Science, vol.\u00a07358, pp.\u00a0277\u2013293. Springer, Berkeley (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23"},{"key":"729_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings, Copenhagen, Denmark, July 27-31, 2002. Lecture Notes in Computer Science, vol.\u00a02404, pp.\u00a0359\u2013364. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"729_CR17","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"2\u20133","key":"729_CR18","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0004-3702(90)90055-5","volume":"42","author":"P.R. Cohen","year":"1990","unstructured":"Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artif. Intell. 42(2\u20133), 213\u2013261 (1990). https:\/\/doi.org\/10.1016\/0004-3702(90)90055-5","journal-title":"Artif. Intell."},{"key":"729_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-16310-9_1","volume-title":"Software Engineering for Collective Autonomic Systems - the ASCENS Approach","author":"R. De Nicola","year":"2015","unstructured":"De Nicola, R., Latella, D., Lluch-Lafuente, A., Loreti, M., Margheri, A., Massink, M., Morichetta, A., Pugliese, R., Tiezzi, F., Vandin, A.: The SCEL language: design, implementation, verification. In: Wirsing, M., H\u00f6lzl, M.M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems - the ASCENS Approach. Lecture Notes in Computer Science, vol.\u00a08998, pp.\u00a03\u201371. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-16310-9_1"},{"key":"729_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-030-03424-5_2","volume-title":"8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","author":"R. De Nicola","year":"2018","unstructured":"De Nicola, R., Maggi, A., Sifakis, J.: DReAM: dynamic reconfigurable architecture modeling. In: Margaria, T., Steffen, B. (eds.) 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). LNCS, vol.\u00a011246, pp.\u00a013\u201331. Springer, Limassol (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_2"},{"key":"729_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-030-61470-6_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings, Part II","author":"R. De Nicola","year":"2020","unstructured":"De Nicola, R., Duong, T., Inverso, O.: Verifying abc specifications via emulation. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings, Part II, Rhodes, Greece, October 20-30, 2020. Lecture Notes in Computer Science, vol.\u00a012477, pp.\u00a0261\u2013279. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61470-6_16"},{"key":"729_CR22","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1109\/ASE.2008.78","volume-title":"23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2008)","author":"N. D\u2019Ippolito","year":"2008","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2008), L\u2019Aquila, Italy, 15\u201319 September 2008, pp.\u00a0475\u2013476. IEEE Comput. Soc., Los Alamitos (2008). https:\/\/doi.org\/10.1109\/ASE.2008.78"},{"key":"729_CR23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"issue":"2","key":"729_CR24","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H. Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"729_CR25","first-page":"257","volume-title":"Proceedings of the 9th European Software Engineering and 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering","author":"D. Giannakopoulou","year":"2003","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of the 9th European Software Engineering and 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp.\u00a0257\u2013266. ACM, New York (2003)"},{"key":"729_CR26","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/j.artint.2017.04.003","volume":"248","author":"J. Gutierrez","year":"2017","unstructured":"Gutierrez, J., Harrenstein, P., Wooldridge, M.: From model checking to equilibrium checking: reactive modules for rational verification. Artif. Intell. 248, 123\u2013157 (2017). https:\/\/doi.org\/10.1016\/j.artint.2017.04.003","journal-title":"Artif. Intell."},{"key":"729_CR27","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/3477355.3477364","volume-title":"Theories of Programming: The Life and Works of Tony Hoare","author":"C.A.R. Hoare","year":"2021","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Jones, C.B., Misra, J. (eds.) Theories of Programming: The Life and Works of Tony Hoare, pp.\u00a0157\u2013186. ACM \/ Morgan & Claypool, New York (2021). https:\/\/doi.org\/10.1145\/3477355.3477364"},{"key":"729_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-030-61470-6_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings, Part II","author":"O. Inverso","year":"2020","unstructured":"Inverso, O., Trubiani, C., Tuosto, E.: Abstractions for collective adaptive systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings, Part II, Rhodes, Greece, October 20-30, 2020. Lecture Notes in Computer Science, vol.\u00a012477, pp.\u00a0243\u2013260. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61470-6_15"},{"key":"729_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings","author":"G. Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings, London, UK, April 11-18, 2015. Lecture Notes in Computer Science, vol.\u00a09035, pp.\u00a0692\u2013707. Springer, London (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"729_CR30","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Statistical Model Checking","author":"A. Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical Model Checking, pp.\u00a0478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"issue":"1","key":"729_CR31","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A. Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"729_CR32","series-title":"Advanced Lectures, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-34096-8_4","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems - 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2016","author":"M. Loreti","year":"2016","unstructured":"Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems - 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2016, Bertinoro, Italy, June 20-24, 2016. Advanced Lectures, Lecture Notes in Computer Science, vol.\u00a09700, pp.\u00a083\u2013119. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_4"},{"issue":"1","key":"729_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inform. and Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"Inform. and Comput."},{"key":"729_CR34","doi-asserted-by":"publisher","DOI":"10.4108\/eai.25-10-2016.2266978","volume-title":"10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016","author":"L. Nenzi","year":"2016","unstructured":"Nenzi, L., Bortolussi, L., Loreti, M.: jsstl - a tool to monitor spatio-temporal properties. In: Puliafito, A., Trivedi, K.S., Tuffin, B., Scarpa, M., Machida, F., Alonso, J. (eds.) 10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016, Taormina, Italy, 25th-28th Oct 2016. ACM, (2016). https:\/\/doi.org\/10.4108\/eai.25-10-2016.2266978"},{"key":"729_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-16310-9_1","volume-title":"Software Engineering for Collective Autonomic Systems - the ASCENS Approach","author":"R.D. Nicola","year":"2015","unstructured":"Nicola, R.D., Latella, D., Lluch-Lafuente, A., Loreti, M., Margheri, A., Massink, M., Morichetta, A., Pugliese, R., Tiezzi, F., Vandin, A.: The SCEL language: design, implementation, verification. In: Wirsing, M., H\u00f6lzl, M.M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems - the ASCENS Approach. Lecture Notes in Computer Science, vol.\u00a08998, pp.\u00a03\u201371. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-16310-9_1"},{"key":"729_CR36","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-10575-8_2","volume-title":"Handbook of Model Checking","author":"N. Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp.\u00a027\u201373. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2"},{"key":"729_CR37","volume-title":"An Introduction to MultiAgent Systems","author":"M.J. Wooldridge","year":"2009","unstructured":"Wooldridge, M.J.: An Introduction to MultiAgent Systems, 2nd edn. Wiley, New York (2009)","edition":"2"},{"key":"729_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1007\/978-3-319-47166-2_47","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Proceedings, Part I","author":"N. Zon","year":"2016","unstructured":"Zon, N., Gilmore, S., Hillston, J.: Rigorous graphical modelling of movement in collective adaptive systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Proceedings, Part I, Corfu, Greece, October 10-14, 2016. Lecture Notes in Computer Science, vol.\u00a09952, pp.\u00a0674\u2013688 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_47"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00729-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00729-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00729-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T07:44:53Z","timestamp":1730447093000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00729-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,2]]},"references-count":38,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["729"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00729-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,2]]},"assertion":[{"value":"10 October 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}