{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:39:01Z","timestamp":1740123541478,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"16","license":[{"start":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T00:00:00Z","timestamp":1684540800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T00:00:00Z","timestamp":1684540800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100007834","name":"Ningbo Natural Science Foundation of China","doi-asserted-by":"crossref","award":["No. 2019A610088"],"award-info":[{"award-number":["No. 2019A610088"]}],"id":[{"id":"10.13039\/100007834","id-type":"DOI","asserted-by":"crossref"}]},{"name":"the Open Subject of Key Laboratory of Embedded and Service Computing of Ministry of Education of China","award":["No. ESSCKF 2019-07"],"award-info":[{"award-number":["No. ESSCKF 2019-07"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2023,11]]},"DOI":"10.1007\/s11227-023-05388-9","type":"journal-article","created":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T14:01:32Z","timestamp":1684591292000},"page":"18886-18909","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Identify spatio-temporal properties of network traffic by model checking"],"prefix":"10.1007","volume":"79","author":[{"given":"Yuan","family":"Zheke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niu","family":"Jun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu","family":"Xurong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Fangmeng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,20]]},"reference":[{"issue":"4","key":"5388_CR1","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1109\/TGCN.2018.2869039","volume":"2","author":"X Liu","year":"2018","unstructured":"Liu X, Ansari N (2018) Dual-battery enabled profit driven user association in green heterogeneous cellular networks. IEEE Trans Green Commun Netw 2(4):1002\u20131011. https:\/\/doi.org\/10.1109\/TGCN.2018.2869039","journal-title":"IEEE Trans Green Commun Netw"},{"key":"5388_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.comcom.2021.01.021","volume":"170","author":"M Abbasi","year":"2021","unstructured":"Abbasi M, Shahraki A, Taherkordi A (2021) Deep learning for network traffic monitoring and analysis (NTMA: a survey. Comput Commun 170:19\u201341. https:\/\/doi.org\/10.1016\/j.comcom.2021.01.021","journal-title":"Comput Commun"},{"key":"5388_CR3","unstructured":"Cecil A (2006) A summary of network traffic monitoring and analysis techniques. Computer systems analysis, pp 4\u20137"},{"issue":"3","key":"5388_CR4","doi-asserted-by":"publisher","first-page":"800","DOI":"10.1109\/TNSM.2019.2933358","volume":"16","author":"A D\u2019Alconzo","year":"2019","unstructured":"D\u2019Alconzo A, Drago I, Morichetta A et al (2019) A survey on big data for network traffic monitoring and analysis. IEEE Trans Netw Serv Manag 16(3):800\u2013813. https:\/\/doi.org\/10.1109\/TNSM.2019.2933358","journal-title":"IEEE Trans Netw Serv Manag"},{"key":"5388_CR5","doi-asserted-by":"publisher","unstructured":"Wang J, Tang J, Xu Z et\u00a0al (2017) Spatiotemporal modeling and prediction in cellular networks: a big data enabled deep learning approach. In: IEEE INFOCOM 2017-IEEE Conference on Computer Communications. IEEE, pp 1\u20139. https:\/\/doi.org\/10.1109\/INFOCOM.2017.8057090","DOI":"10.1109\/INFOCOM.2017.8057090"},{"key":"5388_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511791383.020","volume-title":"Dynamical processes on complex networks","author":"A Barrat","year":"2008","unstructured":"Barrat A, Barth\u00e9lemy M, Vespignani A (2008) Dynamical processes on complex networks. Cambridge University Press, Cambridge. https:\/\/doi.org\/10.1017\/CBO9780511791383.020"},{"key":"5388_CR7","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199206650.001.0001","volume-title":"Networks: an introduction","author":"M Newman","year":"2010","unstructured":"Newman M (2010) Networks: an introduction. Oxford University Press, Oxford. https:\/\/doi.org\/10.1093\/acprof:oso\/9780199206650.001.0001"},{"key":"5388_CR8","doi-asserted-by":"publisher","first-page":"1801","DOI":"10.1007\/s11071-020-05867-1","volume":"101","author":"Y Wang","year":"2020","unstructured":"Wang Y, Wei Z, Cao J (2020) Epidemic dynamics of influenza-like diseases spreading in complex networks. Nonlinear Dyn 101:1801\u20131820. https:\/\/doi.org\/10.1007\/s11071-020-05867-1","journal-title":"Nonlinear Dyn"},{"key":"5388_CR9","doi-asserted-by":"publisher","unstructured":"Shafiq MZ, Ji L, Liu AX et\u00a0al (2012) Characterizing geospatial dynamics of application usage in a 3G cellular data network. In: 2012 Proceedings IEEE INFOCOM. IEEE, pp 1341\u20131349. https:\/\/doi.org\/10.1109\/INFCOM.2012.6195497","DOI":"10.1109\/INFCOM.2012.6195497"},{"key":"5388_CR10","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/s11036-015-0648-6","volume":"21","author":"A Nika","year":"2016","unstructured":"Nika A, Ismail A, Zhao BY et al (2016) Understanding and predicting data hotspots in cellular networks. Mobile Netw Appl 21:402\u2013413. https:\/\/doi.org\/10.1007\/s11036-015-0648-6","journal-title":"Mobile Netw Appl"},{"issue":"9","key":"5388_CR11","doi-asserted-by":"publisher","first-page":"2029","DOI":"10.1109\/LCOMM.2017.2717398","volume":"21","author":"Y Zhou","year":"2017","unstructured":"Zhou Y, Zhao Z, Li R et al (2017) Cooperation-based probabilistic caching strategy in clustered cellular networks. IEEE Commun Lett 21(9):2029\u20132032. https:\/\/doi.org\/10.1109\/LCOMM.2017.2717398","journal-title":"IEEE Commun Lett"},{"key":"5388_CR12","doi-asserted-by":"publisher","unstructured":"Zhou L, Chen X (2019) SVM hotspot identification for cellular networks. In: 2019 IEEE 5th International Conference on Computer and Communications (ICCC). IEEE, pp 1103\u20131107. https:\/\/doi.org\/10.1109\/ICCC47050.2019.9064447","DOI":"10.1109\/ICCC47050.2019.9064447"},{"key":"5388_CR13","doi-asserted-by":"publisher","unstructured":"Masood U, Asghar A, Imran A et\u00a0al (2018) Deep learning based detection of sleeping cells in next generation cellular networks. In: 2018 IEEE Global Communications Conference (GLOBECOM). IEEE, pp 206\u2013212. https:\/\/doi.org\/10.1109\/GLOCOM.2018.8647689","DOI":"10.1109\/GLOCOM.2018.8647689"},{"key":"5388_CR14","doi-asserted-by":"publisher","DOI":"10.1088\/1742-6596\/1624\/5\/052016","author":"L Zhou","year":"2020","unstructured":"Zhou L, Chen X, Dong R et al (2020) Hotspots prediction based on LSTM neural network for cellular networks. J Phys Conf Ser. https:\/\/doi.org\/10.1088\/1742-6596\/1624\/5\/052016","journal-title":"J Phys Conf Ser"},{"key":"5388_CR15","doi-asserted-by":"publisher","unstructured":"Zhang C, Patras P (2018) Long-term mobile traffic forecasting using deep spatio-temporal neural networks. In: Proceedings of the Eighteenth ACM International Symposium on Mobile Ad Hoc Networking and Computing, pp 231\u2013240. https:\/\/doi.org\/10.1145\/3209582.3209606","DOI":"10.1145\/3209582.3209606"},{"key":"5388_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2020.102890","volume":"173","author":"G D\u2019Angelo","year":"2021","unstructured":"D\u2019Angelo G, Palmieri F (2021) Network traffic classification using deep convolutional recurrent autoencoder neural networks for spatial-temporal features extraction. J Netw Comput Appl 173:102890. https:\/\/doi.org\/10.1016\/j.jnca.2020.102890","journal-title":"J Netw Comput Appl"},{"key":"5388_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/s11036-021-01846-x","author":"H Gao","year":"2021","unstructured":"Gao H, Zhang Y, Miao H et al (2021) SDTIOA: modeling the timed privacy requirements of IoT service composition: a user interaction perspective for automatic transformation from BPEL to timed automata. Mobile Netw Appl. https:\/\/doi.org\/10.1007\/s11036-021-01846-x","journal-title":"Mobile Netw Appl"},{"issue":"1","key":"5388_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3517154","volume":"19","author":"H Gao","year":"2023","unstructured":"Gao H, Dai B, Miao H et al (2023) A novel GAPG approach to automatic property generation for formal verification: the GAN perspective. ACM Trans Multimed Comput Commun Appl 19(1):1\u201322. https:\/\/doi.org\/10.1145\/3517154","journal-title":"ACM Trans Multimed Comput Commun Appl"},{"key":"5388_CR19","doi-asserted-by":"publisher","unstructured":"Hussain SR, Echeverria M, Karim I et\u00a0al (2019) 5Greasoner: a property-directed security and privacy analysis framework for 5g cellular network protocol. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. ACM, pp 669\u2013684. https:\/\/doi.org\/10.1145\/3319535.3354263","DOI":"10.1145\/3319535.3354263"},{"issue":"6","key":"5388_CR20","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.1007\/s00607-020-00898-3","volume":"103","author":"S Zroug","year":"2021","unstructured":"Zroug S, Kahloul L, Benharzallah S et al (2021) A hierarchical formal method for performance evaluation of WSNS protocol. Computing 103(6):1183\u20131208. https:\/\/doi.org\/10.1007\/s00607-020-00898-3","journal-title":"Computing"},{"key":"5388_CR21","doi-asserted-by":"publisher","unstructured":"Hou K, Li Y, Yu Y et\u00a0al (2021) Discovering emergency call pitfalls for cellular networks with formal methods. In: Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services, pp 296\u2013309. https:\/\/doi.org\/10.1145\/3458864.3466625","DOI":"10.1145\/3458864.3466625"},{"issue":"2","key":"5388_CR22","doi-asserted-by":"publisher","DOI":"10.1002\/nem.2009","volume":"28","author":"X Cai","year":"2018","unstructured":"Cai X, John W, Meirosu C (2018) Automatic data aggregation for recursively modeled NFV services. Int J Netw Manag 28(2):e2009. https:\/\/doi.org\/10.1002\/nem.2009","journal-title":"Int J Netw Manag"},{"key":"5388_CR23","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"5388_CR24","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-1-4020-5587-4_5","volume-title":"Handbook of spatial logics","author":"J van Benthem","year":"2007","unstructured":"van Benthem J, Bezhanishvili G (2007) Modal logics of space. In: Aiello M, Pratt-Hartmann I, Van Benthem J (eds) Handbook of spatial logics. Springer, Dordrecht, pp 217\u2013298. https:\/\/doi.org\/10.1007\/978-1-4020-5587-4_5"},{"key":"5388_CR25","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:2)2016","author":"M Massink","year":"2017","unstructured":"Massink M, Loreti M, Latella D et al (2017) Model checking spatial logics for closure spaces. Log Methods Comput Sci. https:\/\/doi.org\/10.2168\/LMCS-12(4:2)2016","journal-title":"Log Methods Comput Sci"},{"key":"5388_CR26","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-662-49224-6_24","volume-title":"SEFM 2015 collocated workshops","author":"V Ciancia","year":"2015","unstructured":"Ciancia V, Grilletti G, Latella D et al (2015) An experimental spatio-temporal model checker. In: Bianculli D, Calinescu R, Rumpe B (eds) SEFM 2015 collocated workshops. Springer, Berlin, pp 297\u2013311. https:\/\/doi.org\/10.1007\/978-3-662-49224-6_24"},{"key":"5388_CR27","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(1:4)2022","author":"M Loreti","year":"2022","unstructured":"Loreti M, Bortolussi L, Bartocci E et al (2022) A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Log Methods Comput Sci. https:\/\/doi.org\/10.46298\/LMCS-18(1:4)2022","journal-title":"Log Methods Comput Sci"},{"key":"5388_CR28","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-019-00511-9","volume":"22","author":"F Banci Buonamici","year":"2020","unstructured":"Banci Buonamici F, Belmonte G, Ciancia V et al (2020) Spatial logics and model checking for medical imaging. Int J Softw Tools Technol Transf 22:195\u2013217. https:\/\/doi.org\/10.1007\/s10009-019-00511-9","journal-title":"Int J Softw Tools Technol Transf"},{"key":"5388_CR29","doi-asserted-by":"publisher","unstructured":"Ciancia V, Latella D, Massink M et\u00a0al (2015) Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops. IEEE, pp 74\u201379. https:\/\/doi.org\/10.1109\/SASOW.2015.17","DOI":"10.1109\/SASOW.2015.17"},{"key":"5388_CR30","doi-asserted-by":"publisher","unstructured":"Ciancia V, Latella D, Massink M et\u00a0al (2016) A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: International Symposium on Leveraging Applications of Formal Methods. Springer, pp 657\u2013673. https:\/\/doi.org\/10.1007\/978-3-319-47166-2_46","DOI":"10.1007\/978-3-319-47166-2_46"},{"issue":"3","key":"5388_CR31","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 et al (2018) Spatio-temporal model checking of vehicular movement in public transport systems. Int J Softw Tools Technol Transf 20(3):289\u2013311. https:\/\/doi.org\/10.1007\/s10009-018-0483-8","journal-title":"Int J Softw Tools Technol Transf"},{"key":"5388_CR32","doi-asserted-by":"publisher","unstructured":"Bartocci E, Bortolussi L, Loreti M et\u00a0al (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, pp 146\u2013155. https:\/\/doi.org\/10.1145\/3127041.3127050","DOI":"10.1145\/3127041.3127050"},{"key":"5388_CR33","unstructured":"Vana L, Visconti E, Nenzi L et\u00a0al (2021) Posterior predictive model checking using formal methods in a spatio-temporal model. arXiv preprint arXiv:2110.01360"},{"key":"5388_CR34","doi-asserted-by":"publisher","unstructured":"Wang H, Ding J, Li Y et\u00a0al (2015) Characterizing the spatio-temporal inhomogeneity of mobile traffic in large-scale cellular data networks. In: Proceedings of the 7th International Workshop on Hot Topics in Planet-Scale MObile Computing and Online Social NeTworking. ACM, pp 19\u201324. https:\/\/doi.org\/10.1145\/2757513.2757518","DOI":"10.1145\/2757513.2757518"},{"issue":"5","key":"5388_CR35","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1109\/TSC.2016.2599878","volume":"9","author":"F Xu","year":"2016","unstructured":"Xu F, Lin Y, Huang J et al (2016) Big data driven mobile traffic understanding and forecasting: a time series approach. IEEE Trans Serv Comput 9(5):796\u2013805. https:\/\/doi.org\/10.1109\/TSC.2016.2599878","journal-title":"IEEE Trans Serv Comput"},{"key":"5388_CR36","doi-asserted-by":"publisher","unstructured":"Laner M, Svoboda P, Schwarz S et\u00a0al (2012) Users in cells: a data traffic analysis. In: 2012 IEEE Wireless Communications and Networking Conference (WCNC). IEEE, pp 3063\u20133068. https:\/\/doi.org\/10.1109\/WCNC.2012.6214330","DOI":"10.1109\/WCNC.2012.6214330"},{"key":"5388_CR37","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2021.108567","volume":"201","author":"F Salahdine","year":"2021","unstructured":"Salahdine F, Opadere J, Liu Q et al (2021) A survey on sleep mode techniques for ultra-dense networks in 5G and beyond. Comput Netw 201:108567. https:\/\/doi.org\/10.1016\/j.comnet.2021.108567","journal-title":"Comput Netw"},{"key":"5388_CR38","doi-asserted-by":"publisher","unstructured":"Debaillie B, Desset C, Louagie F (2015) A flexible and future-proof power model for cellular base stations. In: 2015 IEEE 81st Vehicular Technology Conference (VTC Spring). IEEE, pp 1\u20137. https:\/\/doi.org\/10.1109\/VTCSpring.2015.7145603","DOI":"10.1109\/VTCSpring.2015.7145603"},{"issue":"1","key":"5388_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1038\/sdata.2015.55","volume":"2","author":"G Barlacchi","year":"2015","unstructured":"Barlacchi G, De Nadai M, Larcher R et al (2015) A multi-source dataset of urban life in the city of Milan and the province of Trentino. Sci. Data 2(1):1\u201315. https:\/\/doi.org\/10.1038\/sdata.2015.55","journal-title":"Sci. Data"},{"issue":"6","key":"5388_CR40","doi-asserted-by":"publisher","first-page":"3533","DOI":"10.1109\/TITS.2020.2983835","volume":"22","author":"H Gao","year":"2020","unstructured":"Gao H, Liu C, Li Y et al (2020) V2VR: reliable hybrid-network-oriented V2V data transmission and routing considering RSUS and connectivity probability. IEEE Trans Intell Transp Syst 22(6):3533\u20133546. https:\/\/doi.org\/10.1109\/TITS.2020.2983835","journal-title":"IEEE Trans Intell Transp Syst"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05388-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11227-023-05388-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05388-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,18]],"date-time":"2023-09-18T08:13:32Z","timestamp":1695024812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11227-023-05388-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,20]]},"references-count":40,"journal-issue":{"issue":"16","published-print":{"date-parts":[[2023,11]]}},"alternative-id":["5388"],"URL":"https:\/\/doi.org\/10.1007\/s11227-023-05388-9","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"type":"print","value":"0920-8542"},{"type":"electronic","value":"1573-0484"}],"subject":[],"published":{"date-parts":[[2023,5,20]]},"assertion":[{"value":"5 May 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"I declare that the authors have no competing interests as defined by Springer, or other interests that might be perceived to influence the results and\/or discussion reported in this paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval"}}]}}