{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T18:37:23Z","timestamp":1717439843255},"reference-count":71,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T00:00:00Z","timestamp":1606262400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T00:00:00Z","timestamp":1606262400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"National Key Research and Development Project","award":["2017YFB1001800"],"award-info":[{"award-number":["2017YFB1001800"]}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61972150"],"award-info":[{"award-number":["61972150"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Shanghai Knowledge Service Platform Project","award":["ZF1213"],"award-info":[{"award-number":["ZF1213"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cloud Comp"],"published-print":{"date-parts":[[2020,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL<jats:sub><jats:italic>PC<\/jats:italic><\/jats:sub>, by combining Signal Temporal Logic (STL) with a spatial logic S4<jats:sub><jats:italic>u<\/jats:italic><\/jats:sub>, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL<jats:sub><jats:italic>PC<\/jats:italic><\/jats:sub>combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL<jats:sub><jats:italic>PC<\/jats:italic><\/jats:sub>and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL<jats:sub><jats:italic>PC<\/jats:italic><\/jats:sub>and analyze the complexity of STSL<jats:sub><jats:italic>PC<\/jats:italic><\/jats:sub>. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL<jats:sub><jats:italic>OC<\/jats:italic><\/jats:sub>, and provide the proof of its axiomatization system and decidability.<\/jats:p>","DOI":"10.1186\/s13677-020-00209-3","type":"journal-article","created":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T09:04:17Z","timestamp":1606295057000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A spatio-temporal specification language and its completeness &amp; decidability"],"prefix":"10.1186","volume":"9","author":[{"given":"Tengfei","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haiying","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lipeng","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junfeng","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,25]]},"reference":[{"key":"209_CR1","volume-title":"Introduction to Embedded Systems: A Cyber-physical Systems Approach","author":"EA Lee","year":"2016","unstructured":"Lee EA, Seshia SA (2016) Introduction to Embedded Systems: A Cyber-physical Systems Approach. MIT Press, California."},{"issue":"2","key":"209_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3185502","volume":"2","author":"G Liu","year":"2018","unstructured":"Liu G, Jiang C, Zhou M (2018) Time-soundness of time Petri nets modelling time-critical systems. ACM Trans Cyber Phys Syst 2(2):1\u201327.","journal-title":"ACM Trans Cyber Phys Syst"},{"key":"209_CR3","doi-asserted-by":"crossref","unstructured":"Fan C, Qi B, Mitra S, Viswanathan M, Duggirala PS (2016) Automatic reachability analysis for nonlinear hybrid models with C2E2 In: International Conference on Computer Aided Verification, 531\u2013538, Springer.","DOI":"10.1007\/978-3-319-41528-4_29"},{"key":"209_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TITS.2019.2961217","volume":"21","author":"H Gao","year":"2020","unstructured":"Gao H, Liu C, Li Y, Yang X (2020) V2VR: reliable hybrid-network-oriented V2V data transmission and routing considering RSUs and connectivity probability. IEEE Trans Intell Transp Syst 21:1\u201314. https:\/\/doi.org\/10.1109\/TITS.2020.2983835.","journal-title":"IEEE Trans Intell Transp Syst"},{"issue":"3","key":"209_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-018-7039-7","volume":"13","author":"J Liu","year":"2019","unstructured":"Liu J, Li T, Ding Z, Qian Y, Sun H, He J (2019) AADL+: a simulation-based methodology for cyber-physical systems. Front Comput Sci 13(3):1\u201323.","journal-title":"Front Comput Sci"},{"issue":"6","key":"209_CR6","doi-asserted-by":"publisher","first-page":"897","DOI":"10.1142\/S0218194017500334","volume":"27","author":"H Gao","year":"2017","unstructured":"Gao H, Chu D, Duan Y, Yin Y (2017) Probabilistic model checking-based service selection method for business process modeling. Int J Softw Eng Knowl Eng 27(6):897\u2013923.","journal-title":"Int J Softw Eng Knowl Eng"},{"key":"209_CR7","doi-asserted-by":"crossref","unstructured":"An D, Liu J, Chen X, Li T, Yin L (2019) A Modeling Framework of Cyber-Physical-Social Systems with Human Behavior Classification Based on Machine Learning In: 21st International Conference on Formal Engineering Methods, 522\u2013525, Springer.","DOI":"10.1007\/978-3-030-32409-4_37"},{"issue":"4","key":"209_CR8","doi-asserted-by":"publisher","first-page":"1233","DOI":"10.1007\/s11036-020-01535-1","volume":"25","author":"H Gao","year":"2020","unstructured":"Gao H, Kuang L, Yin Y, Guo B, Dou K (2020) \u2019Mining consuming behaviors with temporal evolution for personalized recommendation in mobile marketing Apps. Mob Netw Appl (MONET) 25(4):1233\u20131248.","journal-title":"Mob Netw Appl (MONET)"},{"issue":"3","key":"209_CR9","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2178\/jsl\/1122038915","volume":"70","author":"F Wolter","year":"2005","unstructured":"Wolter F, Zakharyaschev M (2005) A logic for metric and topology. J Symb Log 70(3):795\u2013828.","journal-title":"J Symb Log"},{"key":"209_CR10","doi-asserted-by":"crossref","unstructured":"Raman V, Donz\u00e9 A, Sadigh D, Murray RM, Seshia SA (2015) Reactive synthesis from signal temporal logic specifications In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 239\u2013248, ACM.","DOI":"10.1145\/2728606.2728628"},{"key":"209_CR11","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A, Ferrere T, Maler O (2013) Efficient robust monitoring for STL In: International Conference on Computer Aided Verification, 264\u2013279, Springer.","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"209_CR12","volume-title":"Modal Logic: Graph. Darst","author":"P Blackburn","year":"2002","unstructured":"Blackburn P, De Rijke M, Venema Y (2002) Modal Logic: Graph. Darst, Vol. 53. Cambridge University Press, Dallas, America."},{"key":"209_CR13","doi-asserted-by":"crossref","unstructured":"Davoren JM (2007) Topological semantics and bisimulations for intuitionistic modal logics and their classical companion logics In: International Symposium on Logical Foundations of Computer Science, 162\u2013179, Springer.","DOI":"10.1007\/978-3-540-72734-7_12"},{"key":"209_CR14","first-page":"100","volume":"8","author":"D Fern\u00e1ndez-Duque","year":"2010","unstructured":"Fern\u00e1ndez-Duque D (2010) Absolute completeness of S4u for its measure-theoretic semantics. Adv Modal Log 8:100\u2013119.","journal-title":"Adv Modal Log"},{"key":"209_CR15","doi-asserted-by":"crossref","unstructured":"Li T, Jing L, An D, Sun H (2019) A Sound and Complete Axiomatisation for Spatio-Temporal Specification Language In: The 31st International Conference on Software Engineering & Knowledge Engineering, 153\u2013204, KSI.","DOI":"10.18293\/SEKE2019-222"},{"key":"209_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119","volume-title":"Temporal Logics in Computer Science: Finite-state Systems","author":"S Demri","year":"2016","unstructured":"Demri S, Goranko V, Lange M (2016) Temporal Logics in Computer Science: Finite-state Systems, Vol. 58. Cambridge University Press, Cambridge, United Kingdom."},{"issue":"6","key":"209_CR17","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1007\/s11225-015-9613-4","volume":"103","author":"Y Zhang","year":"2015","unstructured":"Zhang Y, Li K (2015) Decidability of logics based on an indeterministic metric tense logic. Stud Logica 103(6):1123\u20131162.","journal-title":"Stud Logica"},{"key":"209_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical foundations of cyber-physical systems","author":"A Platzer","year":"2018","unstructured":"Platzer A (2018) Logical foundations of cyber-physical systems. Springer, Gewerbestrasse, Switzerland."},{"key":"209_CR19","volume-title":"Dynamic equations on time scales: An introduction with applications","author":"M Bohner","year":"2012","unstructured":"Bohner M, Peterson A (2012) Dynamic equations on time scales: An introduction with applications. Birkh\u00e4user Boston, Washington D.C., USA."},{"issue":"3","key":"209_CR20","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"RE Ladner","year":"1977","unstructured":"Ladner RE (1977) The computational complexity of provability in systems of modal propositional logic. SIAM J Comput 6(3):467\u2013480.","journal-title":"SIAM J Comput"},{"issue":"4","key":"209_CR21","doi-asserted-by":"publisher","first-page":"117","DOI":"10.2307\/2267105","volume":"6","author":"JCC McKinsey","year":"1941","unstructured":"McKinsey JCC (1941) A solution of the decision problem for the Lewis systems S2 and S4, with an application to topology. J Symb Log 6(4):117\u2013124.","journal-title":"J Symb Log"},{"key":"209_CR22","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1613\/jair.1537","volume":"23","author":"D Gabelaia","year":"2005","unstructured":"Gabelaia D, Kontchakov R, Kurucz A, Wolter F, Zakharyaschev M (2005) Combining spatial and temporal logics: expressiveness vs. complexity. J Artif Intell Res 23:167\u2013243.","journal-title":"J Artif Intell Res"},{"key":"209_CR23","unstructured":"Randell DA, Cui Z, Cohn AG (1992) A spatial logic based on regions and connection In: Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning, 165\u2013176, Morgan."},{"key":"209_CR24","unstructured":"Liu W, Li S, Renz J (2009) Combining RCC-8 with Qualitative Direction Calculi: Algorithms and Complexity In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, 854\u2013859, Morgan Kaufmann."},{"key":"209_CR25","doi-asserted-by":"crossref","unstructured":"Kontchakov R, Kurucz A, Wolter F, Zakharyaschev M (2007) Spatial logic+ temporal logic=? In: Handbook of Spatial Logics, 497\u2013564, Springer.","DOI":"10.1007\/978-1-4020-5587-4_9"},{"issue":"2-3","key":"209_CR26","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1080\/11663081.1999.10510972","volume":"9","author":"V Shehtman","year":"1999","unstructured":"Shehtman V (1999) Everywhere and here. J Appl Non-Class Log 9(2-3):369\u2013379.","journal-title":"J Appl Non-Class Log"},{"key":"209_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs In: 18th Annual Symposium on Foundations of Computer Science, 46\u201357, IEEE.","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"209_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2491509.2491514","volume":"22","author":"M Pradella","year":"2013","unstructured":"Pradella M, Morzenti A, Pietro PS (2013) Bounded satisfiability checking of metric temporal logic specifications. ACM Trans Softw Eng Methodol (TOSEM) 22(3):1\u201354.","journal-title":"ACM Trans Softw Eng Methodol (TOSEM)"},{"key":"209_CR29","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals In: Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems, 152\u2013166, Springer.","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"209_CR30","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals In: International Conference on Formal Modeling and Analysis of Timed Systems, 92\u2013106, Springer.","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"209_CR31","doi-asserted-by":"crossref","unstructured":"Sun H, Liu J, Chen X, Du D (2015) Specifying cyber physical system safety properties with metric temporal spatial logic In: 2015 Asia-Pacific Software Engineering Conference (APSEC), 254\u2013260, IEEE.","DOI":"10.1109\/APSEC.2015.58"},{"key":"209_CR32","doi-asserted-by":"crossref","unstructured":"Gabbay D, Pnueli A, Shelah S, Stavi J (1980) On the temporal analysis of fairness In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 163\u2013173, ACM.","DOI":"10.1145\/567446.567462"},{"key":"209_CR33","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A (1985) Checking that finite state concurrent programs satisfy their linear specification In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 97\u2013107, ACM.","DOI":"10.1145\/318593.318622"},{"key":"209_CR34","doi-asserted-by":"crossref","unstructured":"Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M (2015) Qualitative and quantitative monitoring of spatio-temporal properties In: Runtime Verification, 21\u201337, Springer.","DOI":"10.1007\/978-3-319-23820-3_2"},{"key":"209_CR35","volume-title":"Topology","author":"K Kuratowski","year":"2014","unstructured":"Kuratowski K (2014) Topology, Vol. 1. Elsevier Science, London, England."},{"key":"209_CR36","doi-asserted-by":"crossref","unstructured":"Milner R (2001) Bigraphical reactive systems In: International Conference on Concurrency Theory, 16\u201335.","DOI":"10.1007\/3-540-44685-0_2"},{"key":"209_CR37","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2015.02.011","volume":"577","author":"M Sevegnani","year":"2015","unstructured":"Sevegnani M, Calder M (2015) Bigraphs with sharing. Theor Comput Sci 577:43\u201373.","journal-title":"Theor Comput Sci"},{"issue":"4","key":"209_CR38","first-page":"328","volume":"13","author":"D Lemire","year":"2007","unstructured":"Lemire D (2007) Streaming maximum-minimum filter using no more than three comparisons per element. Nordic J Comput 13(4):328\u2013339.","journal-title":"Nordic J Comput"},{"issue":"1","key":"209_CR39","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli A (1981) The temporal semantics of concurrent programs. Theor Comput Sci 13(1):45\u201360.","journal-title":"Theor Comput Sci"},{"issue":"5","key":"209_CR40","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1093\/logcom\/12.5.701","volume":"12","author":"Y Kesten","year":"2002","unstructured":"Kesten Y, Pnueli A (2002) Complete proof system for QPTL. J Log Comput 12(5):701\u2013745.","journal-title":"J Log Comput"},{"issue":"1-2","key":"209_CR41","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(00)00308-X","volume":"274","author":"PY Schobbens","year":"2002","unstructured":"Schobbens PY, Raskin J-F, Henzinger TA (2002) Axioms for real-time logics. Theor Comput Sci 274(1-2):151\u2013182.","journal-title":"Theor Comput Sci"},{"key":"209_CR42","doi-asserted-by":"publisher","DOI":"10.1111\/b.9781405145756.2002.x","volume-title":"A Companion to Philosophical Logic","author":"D Jacquette","year":"2002","unstructured":"Jacquette D (2002) A Companion to Philosophical Logic. Wiley Online Library, Viotoria, Australia."},{"key":"209_CR43","unstructured":"Balbiani P, Fern\u00e1ndez-Duque D (2016) Axiomatizing the lexicographic products of modal logics with linear temporal logic In: International Conference on Advances in Modal Logic, 78\u201396."},{"issue":"2","key":"209_CR44","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(96)00324-6","volume":"183","author":"A Montanaria","year":"1997","unstructured":"Montanaria A, de Rijkeb M (1997) Two-sorted metric temporal logics. Theor Comput Sci 183(2):187\u2013214.","journal-title":"Theor Comput Sci"},{"issue":"2","key":"209_CR45","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1093\/logcom\/1.2.229","volume":"1","author":"DM Gabbay","year":"1990","unstructured":"Gabbay DM, Hodkinson IM (1990) An axiomatization of the temporal logic with until and since over the real numbers. J Log Comput 1(2):229\u2013259.","journal-title":"J Log Comput"},{"issue":"12","key":"209_CR46","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1016\/j.ic.2010.09.008","volume":"209","author":"K Kojima","year":"2011","unstructured":"Kojima K, Igarashi A (2011) Constructive linear-time temporal logic: Proof systems and Kripke semantics. Inf Comput 209(12):1491\u20131503.","journal-title":"Inf Comput"},{"key":"209_CR47","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"BF Chellas","year":"1980","unstructured":"Chellas BF (1980) Modal Logic: An Introduction. Cambridge university press, New York, USA."},{"issue":"1","key":"209_CR48","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur R, Feder T, Henzinger TA (1996) The benefits of relaxing punctuality. J ACM 43(1):116\u2013146.","journal-title":"J ACM"},{"key":"209_CR49","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett C, Tinelli C (2018) Satisfiability modulo theories In: Handbook of Model Checking, 305\u2013343.. Springer, Cham, Switzerland."},{"key":"209_CR50","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.ic.2015.06.007","volume":"245","author":"MM Bersani","year":"2015","unstructured":"Bersani MM, Rossi M, San Pietro P (2015) An SMT-based approach to satisfiability checking of MITL. Inf Comput 245:72\u201397.","journal-title":"Inf Comput"},{"key":"209_CR51","doi-asserted-by":"crossref","unstructured":"Bersani MM, Rossi M, San Pietro P (2013) Deciding continuous-time metric temporal logic with counting modalities In: International Workshop on Reachability Problems, 70\u201382, Springer.","DOI":"10.1007\/978-3-642-41036-9_8"},{"issue":"3","key":"209_CR52","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri S, D\u2019Souza D (2007) An automata-theoretic approach to constraint LTL. Inf Comput 205(3):380\u2013415.","journal-title":"Inf Comput"},{"key":"209_CR53","doi-asserted-by":"crossref","unstructured":"Bersani MM, Rossi M, Pietro PS (2013) Deciding the satisfiability of MITL specifications In: 4th International Symposium on Games, Automata, Logics and Formal Verification, 64\u201378.","DOI":"10.4204\/EPTCS.119.8"},{"key":"209_CR54","first-page":"1","volume":"66","author":"MM Bersani","year":"2014","unstructured":"Bersani MM, Rossi MG, San Pietro P (2014) On the satisfiability of metric temporal logics over the reals. Electron Commun EASST 66:1\u201315.","journal-title":"Electron Commun EASST"},{"issue":"1","key":"209_CR55","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/568438.568455","volume":"32","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2001) Introduction to automata theory, languages, and computation. Acm Sigact News 32(1):60\u201365.","journal-title":"Acm Sigact News"},{"key":"209_CR56","volume-title":"Many-dimensional modal logics: theory and applications","author":"DM Gabbay","year":"2003","unstructured":"Gabbay DM, Kurucz A, Wolter F, Zakharyaschev M (2003) Many-dimensional modal logics: theory and applications. Elsevier North Holland, London, United Kingdom."},{"key":"209_CR57","unstructured":"Gabelaia D, Kontchakov R, Kurucz A, Wolter F, Zakharyaschev M (2003) On the Computational Complexity of Spatio-Temporal Logics In: FLAIRS Conference, 460\u2013464."},{"issue":"3","key":"209_CR58","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 (2018) Spatio-temporal model checking of vehicular movement in public transport systems. Int J Softw Tools Technol Transfer 20(3):289\u2013311.","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"209_CR59","doi-asserted-by":"crossref","unstructured":"Haghighi I, Jones A, Kong Z, Bartocci E, Gros R, Belta C (2015) SpaTeL: a novel spatial-temporal logic and its applications to networked systems In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 189\u2013198, ACM.","DOI":"10.1145\/2728606.2728633"},{"issue":"4","key":"209_CR60","first-page":"1","volume":"14","author":"L Nenzi","year":"2017","unstructured":"Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M (2017) Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log Methods Comput Sci 14(4):1\u201338.","journal-title":"Log Methods Comput Sci"},{"key":"209_CR61","doi-asserted-by":"crossref","unstructured":"Bartocci E, Bortolussi L, Loreti M, Nenzi L (2017) Monitoring mobile and spatially distributed cyber-physical systems In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, 146\u2013155, ACM.","DOI":"10.1145\/3127041.3127050"},{"issue":"1","key":"209_CR62","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.apal.2004.06.004","volume":"131","author":"P Kremer","year":"2005","unstructured":"Kremer P, Mints G (2005) Dynamic topological logic. Ann Pure Appl Log 131(1):133\u2013158.","journal-title":"Ann Pure Appl Log"},{"key":"209_CR63","doi-asserted-by":"crossref","unstructured":"Xu B, Li Q (2016) A spatial logic for modeling and verification of collision-free control of vehicles In: 2016 21st International Conference on Engineering of Complex Computer Systems (ICECCS), 33\u201342, IEEE.","DOI":"10.1109\/ICECCS.2016.014"},{"key":"209_CR64","unstructured":"Mardare R (2006) Logical analysis of complex systems: Dynamic epistemic spatial logics. PhD thesis, University of Trento."},{"issue":"3","key":"209_CR65","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"Bennett B, Cohn AG, Wolter F, Zakharyaschev M (2002) Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl Intell 17(3):239\u2013251.","journal-title":"Appl Intell"},{"issue":"1","key":"209_CR66","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/TCNS.2016.2609138","volume":"5","author":"E Bartocci","year":"2018","unstructured":"Bartocci E, Gol EA, Haghighi I, Belta C (2018) A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans Control Netw Syst 5(1):308\u2013320.","journal-title":"IEEE Trans Control Netw Syst"},{"key":"209_CR67","unstructured":"Balbiani P, Fern\u00e1ndez-Duque D, Lorini E (2017) Exploring the bidimensional space: a dynamic logic point of view In: The 16th Conference on Autonomous Agents and MultiAgent Systems, 132\u2013140, Springer."},{"key":"209_CR68","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer A (2004) A calculus for shapes in time and space In: International Colloquium on Theoretical Aspects of Computing, 463\u2013477, Springer.","DOI":"10.1007\/978-3-540-31862-0_33"},{"key":"209_CR69","doi-asserted-by":"crossref","unstructured":"Shao Z, Liu J, Ding Z, Chen M, Jiang N (2013) Spatio-temporal properties analysis for cyber-physical systems In: 2013 18th International Conference on Engineering of Complex Computer Systems, 101\u2013110, IEEE.","DOI":"10.1109\/ICECCS.2013.23"},{"issue":"5","key":"209_CR70","doi-asserted-by":"publisher","first-page":"4532","DOI":"10.1109\/JIOT.2019.2956827","volume":"7","author":"H Gao","year":"2020","unstructured":"Gao H, Xu Y, Yin Y, Zhang W, Li R, Wang X (2020) Context-aware QoS prediction with neural collaborative filtering for Internet-of-Things services. IEEE Internet Things J 7(5):4532\u20134542.","journal-title":"IEEE Internet Things J"},{"key":"209_CR71","doi-asserted-by":"publisher","unstructured":"Gao H, Huang W, Duan Y (2020) The cloud-edge based dynamic reconfiguration to service workflow for mobile ecommerce environments: A QoS prediction perspective. ACM Trans Internet Technol. https:\/\/doi.org\/10.1145\/3391198.","DOI":"10.1145\/3391198"}],"container-title":["Journal of Cloud Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13677-020-00209-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1186\/s13677-020-00209-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13677-020-00209-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,15]],"date-time":"2021-04-15T05:59:05Z","timestamp":1618466345000},"score":1,"resource":{"primary":{"URL":"https:\/\/journalofcloudcomputing.springeropen.com\/articles\/10.1186\/s13677-020-00209-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,25]]},"references-count":71,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["209"],"URL":"https:\/\/doi.org\/10.1186\/s13677-020-00209-3","relation":{},"ISSN":["2192-113X"],"issn-type":[{"value":"2192-113X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,25]]},"assertion":[{"value":"1 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 October 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 November 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no competing interests regarding the publication of this manuscript.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"65"}}