{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:03:19Z","timestamp":1779087799208,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T00:00:00Z","timestamp":1624233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T00:00:00Z","timestamp":1624233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"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"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61802251"],"award-info":[{"award-number":["61802251"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Key Research and Development Project","award":["2017YFB1001800"],"award-info":[{"award-number":["2017YFB1001800"]}]},{"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":["Mobile Netw Appl"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s11036-021-01779-5","type":"journal-article","created":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T15:03:21Z","timestamp":1624287801000},"page":"2392-2406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Runtime Verification of Spatio-Temporal Specification Language"],"prefix":"10.1007","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9531-7128","authenticated-orcid":false,"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":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ling","family":"Yin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xia","family":"Mao","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":[[2021,6,21]]},"reference":[{"key":"1779_CR1","doi-asserted-by":"crossref","unstructured":"Lee EA (2008) Cyber physical systems: Design challenges. In: 2008 11th IEEE international symposium on object oriented real-time distributed computing (ISORC). IEEE","DOI":"10.1109\/ISORC.2008.25"},{"key":"1779_CR2","unstructured":"Gabbay DM, Kurucz A, Wolter F, Zakharyaschev M (2003) Many-dimensional modal logics: theory and applications. Amsterdam; Boston: Elsevier. North Holland"},{"key":"1779_CR3","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2013.07.012","volume":"503","author":"S Konur","year":"2013","unstructured":"Konur S, Fisher M, Schewe S (2013) Combined model checking for temporal, probabilistic, and real-time logics. Theor Comput Sci 503:61\u201388","journal-title":"Theor Comput Sci"},{"key":"1779_CR4","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":"1779_CR5","unstructured":"Wolter F, Zakharyaschev M (2000) Spatio-temporal representation and reasoning based on RCC-8. In: 7Th international conference on principles of knowledge representation and reasoning. Morgan kaufmann, pp 3\u201314"},{"key":"1779_CR6","doi-asserted-by":"crossref","unstructured":"Bennett B (1994) Spatial reasoning with propositional logics. In: 4Th international conference on principles of knowledge representation and reasoning (KR). Morgan kaufmann, pp 51\u201362","DOI":"10.1016\/B978-1-4832-1452-8.50102-0"},{"key":"1779_CR7","unstructured":"Randell DA, Cui Z, Cohn AG (1992) A spatial logic based on regions and connection. In: 3Th international conference on principles of knowledge representation and reasoning. Morgan kaufmann, pp 165\u2013176"},{"key":"1779_CR8","doi-asserted-by":"crossref","unstructured":"Kontchakov R, Kurucz A, Wolter F, Zakharyaschev M (2007) Spatial logic+ temporal logic=?. In: Handbook of spatial logics. Springer, pp 497\u2013564","DOI":"10.1007\/978-1-4020-5587-4_9"},{"key":"1779_CR9","doi-asserted-by":"crossref","unstructured":"Shao Z, Liu J, Ding Z, Chen M, Jiang N (2013) Spatio-temporal properties analysis for cyberphysical systems. In: 18Th international conference on engineering of complex computer systems (ICECCS). IEEE, pp 101\u2013110","DOI":"10.1109\/ICECCS.2013.23"},{"key":"1779_CR10","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: 22nd asia-pacific software engineering conference (APSEC). IEEE, pp 254\u2013260","DOI":"10.1109\/APSEC.2015.58"},{"issue":"1","key":"1779_CR11","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 (JACM) 43(1):116\u2013146","journal-title":"J ACM (JACM)"},{"key":"1779_CR12","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems. Springer, pp 152\u2013166","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"1779_CR13","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. Springer, pp 264\u2013279","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"1779_CR14","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. ACM, pp 239\u2013248","DOI":"10.1145\/2728606.2728628"},{"key":"1779_CR15","doi-asserted-by":"crossref","unstructured":"Haghighi I, Jones A, Kong Z, Bartocci E, Gros R, Belta C (2015) Spatel: a novel spatialtemporal logic and its applications to networked systems. In: Proceedings of the 18th international conference on hybrid systems: computation and control. ACM, pp 189\u2013198","DOI":"10.1145\/2728606.2728633"},{"key":"1779_CR16","doi-asserted-by":"crossref","unstructured":"Li T., Liu J., Kang J., Sun H., Yin W., Chen X., Wang H. (2020) STSL: A novel spatio-temporal specification language for cyber-physical systems. In: The 20th IEEE international conference on software quality, reliability and security. pp. 309\u2013319. IEEE","DOI":"10.1109\/QRS51102.2020.00048"},{"key":"1779_CR17","doi-asserted-by":"crossref","unstructured":"Li T, Liu J, 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. KSI, pp 153\u2013204","DOI":"10.18293\/SEKE2019-222"},{"issue":"4","key":"1779_CR18","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"},{"key":"1779_CR19","doi-asserted-by":"crossref","unstructured":"Van Laarhoven PJ, Aarts EH (1987) Simulated annealing. In: Simulated annealing: theory and applications. Springer, pp 7\u201315","DOI":"10.1007\/978-94-015-7744-1_2"},{"issue":"3","key":"1779_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":"3","key":"1779_CR21","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":"1779_CR22","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1016\/j.future.2018.04.064","volume":"87","author":"H Gao","year":"2018","unstructured":"Gao H, Huang W, Yang X, Duan Y, Yin Y (2018) Toward service selection for workflow reconfiguration: an interface-based computing solution. Futur Gener Comput Syst 87:298\u2013311","journal-title":"Futur Gener Comput Syst"},{"key":"1779_CR23","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. Springer, pp 21\u201337","DOI":"10.1007\/978-3-319-23820-3_2"},{"issue":"1","key":"1779_CR24","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh JV, Donz\u00e9 A, Ghosh S, Jin X, Juniwal G, Seshia SA (2017) Robust online monitoring of signal temporal logic. Form Methods Syst Des 51(1):5\u201330","journal-title":"Form Methods Syst Des"},{"key":"1779_CR25","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Fainekos G (2012) Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM international conference on hybrid systems: computation and control. ACM, pp 125\u2013134","DOI":"10.1145\/2185632.2185653"},{"key":"1779_CR26","doi-asserted-by":"crossref","unstructured":"Nghiem T, Sankaranarayanan S, Fainekos G, Ivancic F, Gupta A, Pappas GJ (2010) Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control. ACM, pp 211\u2013220","DOI":"10.1145\/1755952.1755983"},{"issue":"11","key":"1779_CR27","doi-asserted-by":"publisher","first-page":"1704","DOI":"10.1109\/TCAD.2015.2421907","volume":"34","author":"X Jin","year":"2015","unstructured":"Jin X, Donz\u00e9 A, Deshmukh JV, Seshia SA (2015) Mining requirements from closed-loop control models. IEEE Trans Comput-Aid Des Integr Circ Syst 34(11):1704\u20131717","journal-title":"IEEE Trans Comput-Aid Des Integr Circ Syst"},{"key":"1779_CR28","doi-asserted-by":"crossref","unstructured":"Zhang Z, Hasuo I, Arcaini P (2019) Multi-armed bandits for boolean connectives in hybrid system falsification. In: International conference on computer aided verification. Springer, pp 401\u2013420","DOI":"10.1007\/978-3-030-25540-4_23"},{"issue":"6","key":"1779_CR29","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1063\/1.1699114","volume":"21","author":"N Metropolis","year":"1953","unstructured":"Metropolis N, Rosenbluth AW, Rosenbluth MN, Teller AH, Teller E (1953) Equation of state calculations by fast computing machines. J Chem Phys 21(6):1087\u20131092","journal-title":"J Chem Phys"},{"key":"1779_CR30","doi-asserted-by":"crossref","unstructured":"Yang X, Zhou S, Cao M (2019) An approach to alleviate the sparsity problem of hybrid collaborative filtering based recommendations: the productattribute perspective from user reviews. Mob Netw Appl :1\u201315","DOI":"10.1007\/s11036-019-01246-2"},{"issue":"3","key":"1779_CR31","doi-asserted-by":"publisher","first-page":"99","DOI":"10.20485\/jsaeijae.9.3_99","volume":"9","author":"T Takahama","year":"2018","unstructured":"Takahama T, Akasaka D (2018) Model predictive control approach to design practical adaptive cruise control for traffic jam. Int J Autom Eng 9(3):99\u2013104","journal-title":"Int J Autom Eng"},{"issue":"4","key":"1779_CR32","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1109\/70.508439","volume":"12","author":"LE Kavraki","year":"1996","unstructured":"Kavraki LE, Svestka P, Latombe JC, Overmars MH (1996) Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Trans Robot Autom 12(4):566\u2013580","journal-title":"IEEE Trans Robot Autom"},{"issue":"2","key":"1779_CR33","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/j.tcs.2005.09.067","volume":"351","author":"A Knapp","year":"2006","unstructured":"Knapp A, Merz S, Wirsing M, Zappe J (2006) Specification and refinement of mobile systems in MTLA and mobile uml. Theor Comput Sci 351(2):184\u2013202","journal-title":"Theor Comput Sci"},{"key":"1779_CR34","doi-asserted-by":"crossref","unstructured":"Bresolin D, Sala P, Della Monica D, Montanari A, Sciavicco G (2010) A decidable spatial generalization of metric interval temporal logic. In: 2010 17Th international symposium on temporal representation and reasoning. IEEE, pp 95\u2013102","DOI":"10.1109\/TIME.2010.22"},{"key":"1779_CR35","unstructured":"Balbiani P, Fern\u00e1ndez-Duque D., Lorini E (2017) Exploring the bidimensional space: a dynamic logic point of view. In: Proceedings of the 16th conference on autonomous agents and multiagent systems. International Foundation for Autonomous Agents and Multiagent Systems, pp 132\u2013140"},{"issue":"3","key":"1779_CR36","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"},{"key":"1779_CR37","doi-asserted-by":"crossref","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 :1\u201323","DOI":"10.1007\/s10009-018-0483-8"},{"key":"1779_CR38","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:1\u201338","journal-title":"Log Methods Comput Sci"},{"key":"1779_CR39","doi-asserted-by":"crossref","unstructured":"Bartocci E, Bortolussi L, Loreti M, Nenzi L (2017) Monitoring mobile and spatially distributed cyberphysical systems. In: Proceedings of the 15th ACMIEEE international conference on formal methods and models for system design. ACM, pp 146\u2013155","DOI":"10.1145\/3127041.3127050"},{"key":"1779_CR40","doi-asserted-by":"crossref","unstructured":"Talcott C (2008) Cyber-physical systems and events. In: Software-intensive systems and new computing paradigms. Springer, pp 101\u2013115","DOI":"10.1007\/978-3-540-89437-7_6"},{"key":"1779_CR41","doi-asserted-by":"crossref","unstructured":"Tan Y, Vuran MC, Goddard S (2009) Spatiotemporal event model for cyber-physical systems. In: 2009 29th IEEE international conference on distributed computing systems workshops. IEEE pp. 44\u201350","DOI":"10.1109\/ICDCSW.2009.82"},{"issue":"3","key":"1779_CR42","first-page":"547","volume":"25","author":"H Gao","year":"2019","unstructured":"Gao H, Huang W, Yang X (2019) Applying probabilistic model checking to path planning in an intelligent transportation system using mobility trajectories and their statistical data. Intell Automat Soft Comput 25(3):547\u2013559","journal-title":"Intell Automat Soft Comput"},{"key":"1779_CR43","doi-asserted-by":"publisher","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 :1\u201314. https:\/\/doi.org\/10.1109\/TITS.2020.2983835","DOI":"10.1109\/TITS.2020.2983835"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-021-01779-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-021-01779-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-021-01779-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,14]],"date-time":"2022-02-14T08:26:26Z","timestamp":1644827186000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-021-01779-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,21]]},"references-count":43,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["1779"],"URL":"https:\/\/doi.org\/10.1007\/s11036-021-01779-5","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,21]]},"assertion":[{"value":"10 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}