{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T19:51:04Z","timestamp":1780516264492,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Advanced Grant no.227977 (SMScom)"],"award-info":[{"award-number":["Advanced Grant no.227977 (SMScom)"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106299","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"38-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":41,"title":["Modeling and verification of evolving cyber-physical spaces"],"prefix":"10.1145","author":[{"given":"Christos","family":"Tsigkanos","sequence":"first","affiliation":[{"name":"Politecnico di Milano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Timo","family":"Kehrer","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlo","family":"Ghezzi","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2307\/2707998"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2882784"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Filip Biljecki Hugo Ledoux and Jantien Stoter. 2016. Generation of multi-LOD 3D city models in CityGML with the procedural modelling engine Random3Dcity. ISPRS Ann. Photogramm. Remote Sens. Spatial Inf. Sci. (2016) 51\u201359.  Filip Biljecki Hugo Ledoux and Jantien Stoter. 2016. Generation of multi-LOD 3D city models in CityGML with the procedural modelling engine Random3Dcity. ISPRS Ann. Photogramm. Remote Sens. Spatial Inf. Sci. (2016) 51\u201359.","DOI":"10.5194\/isprs-annals-IV-4-W1-51-2016"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.013"},{"key":"e_1_3_2_1_5_1","volume-title":"Spatial Data Import and Export","author":"Bivand Roger S","unstructured":"Roger S Bivand , Edzer Pebesma , and Virgilio G\u00f3mez-Rubio . 2013. Spatial Data Import and Export . Springer . Roger S Bivand, Edzer Pebesma, and Virgilio G\u00f3mez-Rubio. 2013. Spatial Data Import and Export. Springer."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0270-3"},{"key":"e_1_3_2_1_7_1","first-page":"1","article-title":"A spatial logic for concurrency","volume":"1","author":"Cardelli Luca","year":"2001","unstructured":"Luca Cardelli and Lu\u00eds Caires . 2001 . A spatial logic for concurrency . In TACS , Vol. 1. 1 \u2013 37 . Luca Cardelli and Lu\u00eds Caires. 2001. A spatial logic for concurrency. In TACS, Vol. 1. 1\u201337.","journal-title":"TACS"},{"key":"e_1_3_2_1_8_1","volume-title":"Automata, Languages and Programming","author":"Cardelli Luca","unstructured":"Luca Cardelli , Philippa Gardner , and Giorgio Ghelli . 2002. A spatial logic for querying graphs . In Automata, Languages and Programming . Springer , 597\u2013610. Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. 2002. A spatial logic for querying graphs. In Automata, Languages and Programming. Springer, 597\u2013610."},{"key":"e_1_3_2_1_9_1","volume-title":"Mobile Ambients. In Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure. 140\u2013155","author":"Cardelli Luca","unstructured":"Luca Cardelli and Andrew D. Gordon . 1998 . Mobile Ambients. In Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure. 140\u2013155 . Luca Cardelli and Andrew D. Gordon. 1998. Mobile Ambients. In Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure. 140\u2013155."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49224-6_24"},{"key":"e_1_3_2_1_11_1","volume-title":"Theoretical Computer Science","author":"Ciancia Vincenzo","unstructured":"Vincenzo Ciancia , Diego Latella , Michele Loreti , and Mieke Massink . 2014. Specifying and verifying properties of space . In Theoretical Computer Science . Springer , 222\u2013235. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2014. Specifying and verifying properties of space. In Theoretical Computer Science. Springer, 222\u2013235."},{"key":"e_1_3_2_1_12_1","volume-title":"Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science 12, 4","author":"Ciancia Vincenzo","year":"2016","unstructured":"Vincenzo Ciancia , Diego Latella , Michele Loreti , and Mieke Massink . 2016. Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science 12, 4 ( 2016 ). Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. 2016. Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science 12, 4 (2016)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SASOW.2015.17"},{"key":"e_1_3_2_1_14_1","unstructured":"Edmund M Clarke Orna Grumberg and Doron A Peled. 1999. Model Checking. MIT press.   Edmund M Clarke Orna Grumberg and Doron A Peled. 1999. Model Checking. MIT press."},{"key":"e_1_3_2_1_15_1","volume-title":"Spatial logics for bigraphs","author":"Conforti Giovanni","unstructured":"Giovanni Conforti , Damiano Macedonio , and Vladimiro Sassone . 2005. Spatial logics for bigraphs . Springer . Giovanni Conforti, Damiano Macedonio, and Vladimiro Sassone. 2005. Spatial logics for bigraphs. Springer."},{"key":"e_1_3_2_1_16_1","volume-title":"Carlo Sansone, and Mario Vento","author":"Conte Donatello","year":"2004","unstructured":"Donatello Conte , Pasquale Foggia , Carlo Sansone, and Mario Vento . 2004 . Thirty years of graph matching in pattern recognition. International journal of pattern recognition and artificial intelligence 18, 03 (2004), 265\u2013298. Donatello Conte, Pasquale Foggia, Carlo Sansone, and Mario Vento. 2004. Thirty years of graph matching in pattern recognition. International journal of pattern recognition and artificial intelligence 18, 03 (2004), 265\u2013298."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Andrea Corradini Ugo Montanari Francesca Rossi Hartmut Ehrig Reiko Heckel and Michael L\u00f6we. 1997. Algebraic Approaches to Graph Transformation-Part I: Basic Concepts and Double Pushout Approach.. In Handbook of Graph Grammars. 163\u2013246.  Andrea Corradini Ugo Montanari Francesca Rossi Hartmut Ehrig Reiko Heckel and Michael L\u00f6we. 1997. Algebraic Approaches to Graph Transformation-Part I: Basic Concepts and Double Pushout Approach.. In Handbook of Graph Grammars. 163\u2013246.","DOI":"10.1142\/9789812384720_0003"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.3390\/aerospace3010001"},{"key":"e_1_3_2_1_19_1","volume-title":"A topological data model for spatial databases","author":"Egenhofer Max J","unstructured":"Max J Egenhofer , Andrew U Frank , and Jeffrey P Jackson . 1989. A topological data model for spatial databases . Springer . Max J Egenhofer, Andrew U Frank, and Jeffrey P Jackson. 1989. A topological data model for spatial databases. Springer."},{"key":"e_1_3_2_1_20_1","first-page":"94","article-title":"Categorizing binary topological relations between regions, lines, and points in geographic databases","volume":"9","author":"Egenhofer Max J","year":"1990","unstructured":"Max J Egenhofer and John Herring . 1990 . Categorizing binary topological relations between regions, lines, and points in geographic databases . The 9 (1990), 94 \u2013 91 . Max J Egenhofer and John Herring. 1990. Categorizing binary topological relations between regions, lines, and points in geographic databases. The 9 (1990), 94\u20131.","journal-title":"The"},{"key":"e_1_3_2_1_21_1","volume-title":"Workshop on Graph Computation Models (GCM","volume":"61","author":"Faithfull Alexander","year":"2013","unstructured":"Alexander Faithfull , Gian Perrone , and Thomas Hildebrandt . 2013 . Big red: A development environment for bigraphs. In Selected Revised Papers from the 4th Intl . Workshop on Graph Computation Models (GCM 2012), Vol. 61 . Alexander Faithfull, Gian Perrone, and Thomas Hildebrandt. 2013. Big red: A development environment for bigraphs. In Selected Revised Papers from the 4th Intl. Workshop on Graph Computation Models (GCM 2012), Vol. 61."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.39"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00156915"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622503.1622508"},{"key":"e_1_3_2_1_25_1","volume-title":"International Workshop on Theory and Application of Graph Transformations. Springer, 310\u2013322","author":"Gadducci Fabio","year":"1998","unstructured":"Fabio Gadducci , Reiko Heckel , and Manuel Koch . 1998 . A fully abstract model for graph-interpreted temporal logic . In International Workshop on Theory and Application of Graph Transformations. Springer, 310\u2013322 . Fabio Gadducci, Reiko Heckel, and Manuel Koch. 1998. A fully abstract model for graph-interpreted temporal logic. In International Workshop on Theory and Application of Graph Transformations. Springer, 310\u2013322."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00701-6"},{"key":"e_1_3_2_1_27_1","volume-title":"Protocol Specification","author":"Gerth Rob","unstructured":"Rob Gerth , Doron Peled , Moshe Y Vardi , and Pierre Wolper . 1996. Simple onthe-fly automatic verification of linear temporal logic . In Protocol Specification , Testing and Verification XV. Springer , 3\u201318. Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. 1996. Simple onthe-fly automatic verification of linear temporal logic. In Protocol Specification, Testing and Verification XV. Springer, 3\u201318."},{"key":"e_1_3_2_1_28_1","volume-title":"Lars Birkedal, and Espen H\u00f8jsgaard.","author":"Glenstrup Arne John","year":"2008","unstructured":"Arne John Glenstrup , Troels Christoffer Damgaard , Lars Birkedal, and Espen H\u00f8jsgaard. 2008 . An Implementation of Bigraph Matching . (2008). Arne John Glenstrup, Troels Christoffer Damgaard, Lars Birkedal, and Espen H\u00f8jsgaard. 2008. An Implementation of Bigraph Matching. (2008)."},{"key":"e_1_3_2_1_29_1","unstructured":"Gerhard Gr\u00f6ger Thomas H Kolbe Angela Czerwinski Claus Nagel and others. 2008. OpenGIS city geography markup language (CityGML) encoding standard version 1.0. 0. (2008).  Gerhard Gr\u00f6ger Thomas H Kolbe Angela Czerwinski Claus Nagel and others. 2008. OpenGIS city geography markup language (CityGML) encoding standard version 1.0. 0. (2008)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053588"},{"key":"e_1_3_2_1_31_1","volume-title":"An EMOF-Compliant Abstract Syntax for Bigraphs. CoRR abs\/1612.01638","author":"Kehrer Timo","year":"2016","unstructured":"Timo Kehrer , Christos Tsigkanos , and Carlo Ghezzi . 2016. An EMOF-Compliant Abstract Syntax for Bigraphs. CoRR abs\/1612.01638 ( 2016 ). Timo Kehrer, Christos Tsigkanos, and Carlo Ghezzi. 2016. An EMOF-Compliant Abstract Syntax for Bigraphs. CoRR abs\/1612.01638 (2016)."},{"key":"e_1_3_2_1_32_1","unstructured":"Jessie Kennedy Peter Barclay and others. 1996. A survey of query languages for geographic information systems. (1996).  Jessie Kennedy Peter Barclay and others. 1996. A survey of query languages for geographic information systems. (1996)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759394.1759416"},{"key":"e_1_3_2_1_34_1","volume-title":"Spatial logic+ temporal logic=? In Handbook of spatial logics","author":"Kontchakov Roman","unstructured":"Roman Kontchakov , Agi Kurucz , Frank Wolter , and Michael Zakharyaschev . 2007. Spatial logic+ temporal logic=? In Handbook of spatial logics . Springer , 497\u2013564. Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. 2007. Spatial logic+ temporal logic=? In Handbook of spatial logics. Springer, 497\u2013564."},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the Agent-Directed Simulation Symposium. Society for Computer Simulation International, 7.","author":"Madey Alexander G","year":"2013","unstructured":"Alexander G Madey and Gregory R Madey . 2013 . Design and evaluation of UAV swarm command and control strategies . In Proceedings of the Agent-Directed Simulation Symposium. Society for Computer Simulation International, 7. Alexander G Madey and Gregory R Madey. 2013. Design and evaluation of UAV swarm command and control strategies. In Proceedings of the Agent-Directed Simulation Symposium. Society for Computer Simulation International, 7."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.07.003"},{"key":"e_1_3_2_1_37_1","volume-title":"The Space and Motion of Communicating Agents","author":"Milner Robin","unstructured":"Robin Milner . 2009. The Space and Motion of Communicating Agents . Cambridge University Press . Robin Milner. 2009. The Space and Motion of Communicating Agents. Cambridge University Press."},{"key":"e_1_3_2_1_38_1","volume-title":"Runtime Verification","author":"Nenzi Laura","unstructured":"Laura Nenzi , Luca Bortolussi , Vincenzo Ciancia , Michele Loreti , and Mieke Massink . 2015. Qualitative and quantitative monitoring of spatio-temporal properties . In Runtime Verification . Springer , 21\u201337. Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. 2015. Qualitative and quantitative monitoring of spatio-temporal properties. In Runtime Verification. Springer, 21\u201337."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/237661.237683"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0210-2"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.25"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1155\/2016\/8132812"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.02.011"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/523986.857995"},{"key":"e_1_3_2_1_46_1","volume-title":"Spatio-temporal Hybrid Automata for Cyber-Physical Systems","author":"Shao Zhucheng","unstructured":"Zhucheng Shao and Jing Liu . 2013. Spatio-temporal Hybrid Automata for Cyber-Physical Systems . Springer Berlin Heidelberg , Berlin, Heidelberg , 337\u2013354. Zhucheng Shao and Jing Liu. 2013. Spatio-temporal Hybrid Automata for Cyber-Physical Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 337\u2013354."},{"key":"e_1_3_2_1_47_1","volume-title":"Specifying Cyber Physical System Safety Properties with Metric Temporal Spatial Logic. In 2015 Asia-Pacific Software Engineering Conference (APSEC). IEEE, 254\u2013260","author":"Sun Haiying","year":"2015","unstructured":"Haiying Sun , Jing Liu , Xiaohong Chen , and Dehui Du . 2015 . Specifying Cyber Physical System Safety Properties with Metric Temporal Spatial Logic. In 2015 Asia-Pacific Software Engineering Conference (APSEC). IEEE, 254\u2013260 . Haiying Sun, Jing Liu, Xiaohong Chen, and Dehui Du. 2015. Specifying Cyber Physical System Safety Properties with Metric Temporal Spatial Logic. In 2015 Asia-Pacific Software Engineering Conference (APSEC). IEEE, 254\u2013260."},{"key":"e_1_3_2_1_48_1","volume-title":"On Formalizing and Identifying Patterns in Cloud Workload Specifications. In 13th Working IEEE\/IFIP Conference on Software Architecture, WICSA 2016","author":"Tsigkanos Christos","year":"2016","unstructured":"Christos Tsigkanos and Timo Kehrer . 2016 . On Formalizing and Identifying Patterns in Cloud Workload Specifications. In 13th Working IEEE\/IFIP Conference on Software Architecture, WICSA 2016 , Venice, Italy , April 5-8, 2016. 262\u2013267. Christos Tsigkanos and Timo Kehrer. 2016. On Formalizing and Identifying Patterns in Cloud Workload Specifications. In 13th Working IEEE\/IFIP Conference on Software Architecture, WICSA 2016, Venice, Italy, April 5-8, 2016. 262\u2013267."},{"key":"e_1_3_2_1_49_1","unstructured":"Christos Tsigkanos Timo Kehrer and Carlo Ghezzi. 2017. Accompanied material and data for this paper. http:\/\/home.deib.polimi.it\/tsigkanos\/fse17. (2017).  Christos Tsigkanos Timo Kehrer and Carlo Ghezzi. 2017. Accompanied material and data for this paper. http:\/\/home.deib.polimi.it\/tsigkanos\/fse17. (2017)."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897035.2897042"},{"key":"e_1_3_2_1_51_1","first-page":"1","article-title":"On the Interplay Between Cyber and Physical Spaces for Adaptive Security","volume":"99","author":"Tsigkanos Christos","year":"2016","unstructured":"Christos Tsigkanos , Liliana Pasquale , Carlo Ghezzi , and Bashar Nuseibeh . 2016 . On the Interplay Between Cyber and Physical Spaces for Adaptive Security . IEEE Transactions on Dependable and Secure Computing PP , 99 (2016), 1 \u2013 1 . Christos Tsigkanos, Liliana Pasquale, Carlo Ghezzi, and Bashar Nuseibeh. 2016. On the Interplay Between Cyber and Physical Spaces for Adaptive Security. IEEE Transactions on Dependable and Secure Computing PP, 99 (2016), 1\u20131.","journal-title":"IEEE Transactions on Dependable and Secure Computing PP"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2014.6912262"},{"key":"e_1_3_2_1_53_1","unstructured":"Junfei Xie Firas AI-Emrani Yixin Gu Yan Wan and Shengli Fu. 2016. UAVCarried Long Distance Wi-Fi Communication Infrastructure. In AIAA Infotech@ Aerospace. 0747.  Junfei Xie Firas AI-Emrani Yixin Gu Yan Wan and Shengli Fu. 2016. UAVCarried Long Distance Wi-Fi Communication Infrastructure. In AIAA Infotech@ Aerospace. 0747."}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Paderborn Germany","acronym":"ESEC\/FSE'17","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106299","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":52,"alternative-id":["10.1145\/3106237.3106299","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106299","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}