{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:44:35Z","timestamp":1779392675238,"version":"3.53.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031879074","type":"print"},{"value":"9783031879081","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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-87908-1_9","type":"book-chapter","created":{"date-parts":[[2025,4,18]],"date-time":"2025-04-18T08:51:02Z","timestamp":1744966262000},"page":"137-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Achieving Energy Efficiency and\u00a0Service Availability in\u00a06G O-RAN via\u00a0Formal Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6992-4285","authenticated-orcid":false,"given":"Roberto","family":"Metere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2460-7926","authenticated-orcid":false,"given":"Kangfeng","family":"Ye","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8134-5822","authenticated-orcid":false,"given":"Yue","family":"Gu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3457-6919","authenticated-orcid":false,"given":"Zhi","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1365-8026","authenticated-orcid":false,"given":"Dalal","family":"Alrajeh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6773-9481","authenticated-orcid":false,"given":"Michele","family":"Sevegnani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0169-0704","authenticated-orcid":false,"given":"Poonam","family":"Yadav","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,4,19]]},"reference":[{"key":"9_CR1","unstructured":"In the 6G era, we won\u2019t need to sacrifice sustainability for the sake of performance. https:\/\/www.bell-labs.com\/institute\/blog\/in-the-6g-era-we-wont-need-to-sacrifice-sustainability-for-the-sake-of-performance\/#gref"},{"key":"9_CR2","unstructured":"Open Research Area Network (O-RAN) - Map. https:\/\/map.o-ran.org\/"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Design 15(1), 7\u201348 (1999)","DOI":"10.1023\/A:1008739929481"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","DOI":"10.1109\/TSE.2003.1205180"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Baldini, G., et al.: Toward sustainable O-RAN deployment: an in-depth analysis of power consumption. IEEE Trans. Green Commun. Netw. (2024)","DOI":"10.1109\/TGCN.2024.3426108"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Bonati, L., D\u2019Oro, S., Polese, M., Basagni, S., Melodia, T.: Intelligence and learning in o-ran for data-driven NextG cellular networks. IEEE Commun. Mag. 59(10), 21\u201327 (2021)","DOI":"10.1109\/MCOM.101.2001120"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Bonati, L., Polese, M., D\u2019Oro, S., Basagni, S., Melodia, T.: Open, programmable, and virtualized 5G networks: state-of-the-art and the road ahead. Comput. Netw. 182, 107516 (2020)","DOI":"10.1016\/j.comnet.2020.107516"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Brito, J.A., Moreno, J.I., Contreras, L.M., Caamano, M.B.: Architecture and methodology for green MEC services using programmable data planes in 5G and beyond networks. In: 2024 IFIP Networking Conference (IFIP Networking), pp. 738\u2013743. IEEE (2024)","DOI":"10.23919\/IFIPNetworking62109.2024.10619774"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Buckworth, T., Alrajeh, D., Kramer, J., Uchitel, S.: Adapting specifications for reactive controllers. In: 18th IEEE\/ACM Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2023, Melbourne, Australia, May 15-16, 2023, pp. 1\u201312. IEEE (2023)","DOI":"10.1109\/SEAMS59076.2023.00012"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to modelling and checking Markov automata. In: International Conference on Quantitative Evaluation of Systems, pp. 52\u201369. Springer (2019)","DOI":"10.1007\/978-3-030-30281-8_4"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Chataut, R., Nankya, M., Akl, R.: 6G networks and the AI revolution-exploring technologies, applications, and emerging challenges. Sensors 24(6), 1888 (2024)","DOI":"10.3390\/s24061888"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54\u201356. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058022"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: LASER Summer School on Software Engineering, pp. 1\u201330. Springer (2011)","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Duflot, M., Fribourg, L., Herault, T., Lassaigne, R., Magniette, F., Messika, S., Peyronnet, S., Picaronny, C.: Probabilistic model checking of the CSMA\/CD protocol using prism and APMC. Electron. Notes Theor. Comput. Sci. 128(6), 195\u2013214 (2005)","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Gu, Y., Hunt, W., Archibald, B., Xu, M., Sevegnani, M., Soorati, M.D.: Successful swarms: operator situational awareness with modelling and verification at runtime. In: 2023 32nd IEEE International Conference on Robot and Human Interactive Communication (RO-MAN), pp. 541\u2013548. IEEE (2023)","DOI":"10.1109\/RO-MAN57019.2023.10309626"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Guo, X., Niu, Z., Zhou, S., Kumar, P.: Delay-constrained energy-optimal base station sleeping control. IEEE J. Sel. Areas Commun. 34(5), 1073\u20131085 (2016)","DOI":"10.1109\/JSAC.2016.2520221"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theoret. Comput. Sci. 391(3), 239\u2013257 (2008)","DOI":"10.1016\/j.tcs.2007.11.013"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transfer, 1\u201322 (2021)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Jian, Z., Muqing, W., Min, Z.: Energy-efficient switching on\/off strategies analysis for dense cellular networks with partial conventional base-stations. IEEE Access 8, 9133\u20139145 (2019)","DOI":"10.1109\/ACCESS.2019.2958654"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Keshta, I., Soni, M., Deb, N., Saravanan, K., Khan, I.R., et al.: Game theory-based optimization for efficient IoT task offloading in 6G network base stations. Meas. Sens. 33, 101184 (2024)","DOI":"10.1016\/j.measen.2024.101184"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, pp. 200\u2013204. Springer (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: International Conference on Runtime Verification, pp. 122\u2013135. Springer (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Liang, X., Al-Tahmeesschi, A., Wang, Q., Chetty, S., Sun, C., Ahmadi, H.: Enhancing energy efficiency in O-RAN through intelligent xApps deployment. arXiv preprint arXiv:2405.10116 (2024)","DOI":"10.1109\/WINCOM62286.2024.10658116"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Mohan, P., et al.: TPEMLB: a novel two-phase energy minimized load balancing scheme for WSN data collection with successive convex approximation using mobile sink. Ain Shams Eng. J., 102849 (2024)","DOI":"10.1016\/j.asej.2024.102849"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Logical Methods Comput. Sci. 14(4), 2 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:2)2018","DOI":"10.23638\/LMCS-14(4:2)2018"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Niknam, S., et al.: Intelligent O-RAN for beyond 5G and 6G wireless networks. In: 2022 IEEE Globecom Workshops (GC Wkshps), pp. 215\u2013220. IEEE (2022)","DOI":"10.1109\/GCWkshps56602.2022.10008676"},{"key":"9_CR28","unstructured":"Office, T.P.: TIM: among the first operators in Europe and the only one in Italy to launch Open RAN solutions on the mobile network (2021). https:\/\/www.gruppotim.it\/en\/press-archive\/corporate\/2021\/CS-TIM-ORAN-Faenza-26-aprile2021-EN.html"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Polese, M., Bonati, L., D\u2019oro, S., Basagni, S., Melodia, T.: Understanding O-RAN: architecture, interfaces, algorithms, security, and research challenges. IEEE Commun. Surv. Tutorials 25(2), 1376\u20131411 (2023)","DOI":"10.1109\/COMST.2023.3239220"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Rached, N.B., Ghazzai, H., Kadri, A., Alouini, M.S.: A time-varied probabilistic on\/off switching algorithm for cellular networks. IEEE Commun. Lett. 22(3), 634\u2013637 (2018)","DOI":"10.1109\/LCOMM.2018.2792001"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Sesto-Castilla, D., Garcia-Villegas, E., Lyberopoulos, G., Theodoropoulou, E.: Use of machine learning for energy efficiency in present and future mobile networks. In: 2019 IEEE Wireless Communications and Networking Conference (WCNC), pp.\u00a01\u20136. IEEE (2019)","DOI":"10.1109\/WCNC.2019.8885478"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Singh, S.P., Kumar, N., Singh, A., Singh, K.K., Askar, S.S., Abouhawwash, M.: Energy efficient hybrid evolutionary algorithm for internet of everything (IoE)-enabled 6G. IEEE Access (2024)","DOI":"10.1109\/ACCESS.2024.3390939"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Tahat, A., Wahhab, F., Edwan, T.A.: An exemplification of decisions of machine learning classifiers to predict handover in a 5G\/4G\/3G cellular communications network. In: 2024 20th International Conference on the Design of Reliable Communication Networks (DRCN), pp.\u00a01\u20135. IEEE (2024)","DOI":"10.1109\/DRCN60692.2024.10539173"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Thantharate, P., Thantharate, A., Kulkarni, A.: GREENSKY: a fair energy-aware optimization model for UAVs in next-generation wireless networks. Green Energy Intell. Transp. 3(1), 100130 (2024)","DOI":"10.1016\/j.geits.2023.100130"},{"key":"9_CR35","unstructured":"Vodafone: Vodafone deploys OpenRAN in urban locations in European first (2022). https:\/\/www.vodafone.co.uk\/newscentre\/press-release\/openran-deployed-in-urban-locations-in-european-first\/"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Yeh, S.p., Bhattacharya, S., Sharma, R., Moustafa, H.: Deep learning for intelligent and automated network slicing in 5G Open RAN (ORAN) deployment. IEEE Open J. Commun. Soc. (2023)","DOI":"10.1109\/OJCOMS.2023.3337854"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Younes, H.L., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: International Conference on Computer Aided Verification, pp. 223\u2013235. Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. 8(3), 216\u2013228. https:\/\/doi.org\/10.1007\/s10009-005-0187-8","DOI":"10.1007\/s10009-005-0187-8"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Yungaicela-Naula, N.M., Sharma, V., Scott-Hayward, S.: Misconfiguration in O-RAN: analysis of the impact of AI\/ML. Comput. Netw., 110455 (2024)","DOI":"10.1016\/j.comnet.2024.110455"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Zaki, Y., P\u00f6tsch, T., Chen, J., Subramanian, L., G\u00f6rg, C.: Adaptive congestion control for unpredictable cellular networks. In: Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication, pp. 509\u2013522 (2015)","DOI":"10.1145\/2785956.2787498"}],"container-title":["Lecture Notes in Computer Science","From Data to Models and Back"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-87908-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,18]],"date-time":"2025-04-18T08:51:16Z","timestamp":1744966276000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-87908-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031879074","9783031879081"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-87908-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"19 April 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DataMod","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium: From Data to Models and Back","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"5 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 November 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":"datamod2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/datamod2024.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}