{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T08:10:31Z","timestamp":1746778231794,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031737084"},{"type":"electronic","value":"9783031737091"}],"license":[{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"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-73709-1_18","type":"book-chapter","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T10:12:01Z","timestamp":1728382321000},"page":"287-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Strategies in\u00a0Spatio-Temporal Logics for\u00a0Multi-agent Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4662-2019","authenticated-orcid":false,"given":"Paolo","family":"Bottoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5405-5531","authenticated-orcid":false,"given":"Anna","family":"Labella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8687-6323","authenticated-orcid":false,"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,9]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","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:1\u201310248:29 (2020)","DOI":"10.1016\/j.scico.2020.102428"},{"issue":"5","key":"18_CR2","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Alechina, N., Logan, B., Nga Nguyen, H., Raimondi, F.: Model-checking for resource-bounded ATL with production and consumption of resources. J. Comput. Syst. Sci., 88, 126\u2013144 (2017)","DOI":"10.1016\/j.jcss.2017.03.008"},{"issue":"4","key":"18_CR4","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1017\/S0960129517000019","volume":"28","author":"P Bottoni","year":"2018","unstructured":"Bottoni, P., Gorla, D., Kasangian, S., Labella, A.: A doctrinal approach to modal\/temporal heyting logic and non-determinism in processes. Math. Struct. in Comp. Sci. 28(4), 508\u2013532 (2018)","journal-title":"Math. Struct. in Comp. Sci."},{"issue":"2","key":"18_CR5","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.jvlc.2011.11.006","volume":"23","author":"P Bottoni","year":"2012","unstructured":"Bottoni, P., Labella, A., Kasangian, S.: Spatial and temporal aspects in visual interaction. J. Visual Lang. Comput. 23(2), 91\u2013102 (2012)","journal-title":"J. Visual Lang. Comput."},{"issue":"1","key":"18_CR6","first-page":"51","volume":"2","author":"P Bottoni","year":"2006","unstructured":"Bottoni, P., De Rosa, F., Hoffmann, K., Mecella, M.: Applying algebraic approaches for modeling workflows and their transformations in mobile networks. Mob. Inf. Syst. 2(1), 51\u201376 (2006)","journal-title":"Mob. Inf. Syst."},{"issue":"3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10009-018-0483-8","volume":"20","author":"V Ciancia","year":"2018","unstructured":"Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transfer 20(3), 289\u2013311 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0483-8","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10575-8_1","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"100511","DOI":"10.1016\/j.jlamp.2019.100511","volume":"111","author":"R De Nicola","year":"2020","unstructured":"De Nicola, R., Ferrari, G., Pugliese, R., Tiezzi, F.: A formal approach to the engineering of domain-specific distributed systems. J. Log. Algebraic Meth. Program. 111, 100511 (2020)","journal-title":"J. Log. Algebraic Meth. Program."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Labella, A.: Tree morphisms and bisimulations. In: Jancar, P., Kret\u00ednsk\u00fd, M., eds, Proceedings of the MFCS \u201998 Workshop on Concurrency, volume\u00a018 of ENTCS, pp. 46\u201364. Elsevier (1998)","DOI":"10.1016\/S1571-0661(05)80249-X"},{"issue":"1","key":"18_CR11","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/963927.963930","volume":"5","author":"R De Nicola","year":"2004","unstructured":"De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Log. 5(1), 79\u2013128 (2004)","journal-title":"ACM Trans. Comput. Log."},{"issue":"7","key":"18_CR12","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1017\/S0960129521000207","volume":"31","author":"F Dagnino","year":"2021","unstructured":"Dagnino, F., Rosolini, G.: Doctrines, modalities and comonads. Math. Struct. Comput. Sci. 31(7), 769\u2013798 (2021)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"18_CR13","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM (JACM) 42(2), 458\u2013487 (1995)","journal-title":"J. ACM (JACM)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpers, J.Y.: Sometimes and not never revisited: on branching versus linear time (preliminary report). In: Proceedings POPL 1983, pp. 127\u2013140, New York, NY, USA, ACM (1983)","DOI":"10.1145\/567067.567081"},{"issue":"3","key":"18_CR15","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/s00224-019-09926-y","volume":"64","author":"P Gardy","year":"2020","unstructured":"Gardy, P., Bouyer, P., Markey, N.: Dependences in strategy logic. Theory Comput. Syst. 64(3), 467\u2013507 (2020)","journal-title":"Theory Comput. Syst."},{"key":"18_CR16","unstructured":"Grilletti, G.: Spatio-temporal model checking: explicit and abstraction-based methods. Master Thesis, Dip. Matematica, Pisa University (2016)"},{"issue":"4","key":"18_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BF01784885","volume":"3","author":"JY Halpern","year":"1989","unstructured":"Halpern, J.Y., Fagin, R.: Modelling knowledge and action in distributed systems. Distrib. Comput. 3(4), 159\u2013177 (1989)","journal-title":"Distrib. Comput."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-40948-6_13","volume-title":"Logic, Rationality, and Interaction","author":"A Herzig","year":"2013","unstructured":"Herzig, A., Lorini, E., Walther, D.: Reasoning about actions meets strategic logics. In: Grossi, D., Roy, O., Huang, H. (eds.) LORI 2013. LNCS, vol. 8196, pp. 162\u2013175. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40948-6_13"},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M.: Logic in computer science: modelling and reasoning about systems, Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511810275"},{"key":"18_CR21","unstructured":"Jamroga, W., Mittelmann, M., Murano, A., Perelli, G.: Playing quantitative games against an authority: on the module checking problem. In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V., eds, AAMAS\u201924, pp. 926\u2013934. International Foundation for Autonomous Agents and Multiagent Systems \/ ACM (2024)"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic + temporal logic = ? In: Handbook of Spatial Logics, pp. 497\u2013564. Springer Netherlands (2007). https:\/\/doi.org\/10.1007\/978-1-4020-5587-4_9","DOI":"10.1007\/978-1-4020-5587-4_9"},{"issue":"6","key":"18_CR23","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1017\/S0960129599002935","volume":"9","author":"S Kasangian","year":"1999","unstructured":"Kasangian, S., Labella, A.: Observational trees as models for concurrency. Math. Struct. Comput. Sci. 9(6), 687\u2013718 (1999)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"18_CR24","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0022-4049(01)00048-2","volume":"168","author":"M Kelly","year":"2002","unstructured":"Kelly, M., Labella, A., Schmitt, V., Street, R.: Categories enriched on two sides. J. Pure Appl. Algebra 168(1), 53\u201398 (2002)","journal-title":"J. Pure Appl. Algebra"},{"key":"18_CR25","unstructured":"Milner, R.: Communication and concurrency, PHI Series in computer science. Prentice Hall (1989)"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM TOCL, 15(4), 34:1\u201334:47 (2014)","DOI":"10.1145\/2631917"},{"key":"18_CR27","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the satisfiability problem. Log. Meth. Comp. Sci., 13(1) (2017)"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Maximova, M., Schneider, S., Giese, H.: Compositional analysis of probabilistic timed graph transformation systems. Form. Asp. Comput. 35(3), 16:1\u201316:79 (2023)","DOI":"10.1145\/3572782"},{"key":"18_CR29","first-page":"394","volume":"24","author":"C Pisani","year":"2010","unstructured":"Pisani, C.: A logic for categories. Theory and Applications of Categories 24, 394\u2013417 (2010)","journal-title":"Theory and Applications of Categories"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS-77, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73709-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:06:32Z","timestamp":1729674392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73709-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,9]]},"ISBN":["9783031737084","9783031737091"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73709-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,9]]},"assertion":[{"value":"9 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}