{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T22:17:09Z","timestamp":1774909029989,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T00:00:00Z","timestamp":1696291200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T00:00:00Z","timestamp":1696291200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100012130","name":"Aviation Science Foundation of China","doi-asserted-by":"crossref","award":["20185152035"],"award-info":[{"award-number":["20185152035"]}],"id":[{"id":"10.13039\/501100012130","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61572253"],"award-info":[{"award-number":["61572253"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["NJ2020022"],"award-info":[{"award-number":["NJ2020022"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["NJ2019010"],"award-info":[{"award-number":["NJ2019010"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s11227-023-05669-3","type":"journal-article","created":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T06:02:20Z","timestamp":1696312940000},"page":"5616-5653","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Performance modeling and quantitative evaluation for cyber-physical systems based on LTS"],"prefix":"10.1007","volume":"80","author":[{"given":"Zhen","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zining","family":"Cao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Xing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,3]]},"reference":[{"key":"5669_CR1","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1016\/j.jmsy.2020.11.017","volume":"58","author":"DGS Pivoto","year":"2021","unstructured":"Pivoto DGS, de Almeida LFF, da Rosa Righi R, Rodrigues JJPC, Lugli AB, Alberti AM (2021) Cyber-physical systems architectures for industrial internet of things applications in industry 4.0: a literature review. J Manuf Syst 58:176\u2013192. https:\/\/doi.org\/10.1016\/j.jmsy.2020.11.017","journal-title":"J Manuf Syst"},{"key":"5669_CR2","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.iotcps.2021.12.002","volume":"1","author":"AK Tyagi","year":"2021","unstructured":"Tyagi AK, Sreenath N (2021) Cyber physical systems: analyses, challenges and possible solutions. Internet Things Cyber-Phys Syst 1:22\u201333. https:\/\/doi.org\/10.1016\/j.iotcps.2021.12.002","journal-title":"Internet Things Cyber-Phys Syst"},{"key":"5669_CR3","doi-asserted-by":"publisher","first-page":"103201","DOI":"10.1016\/j.micpro.2020.103201","volume":"77","author":"J-PA Yaacoub","year":"2020","unstructured":"Yaacoub J-PA, Salman O, Noura HN, Kaaniche N, Chehab A, Malli M (2020) Cyber-physical systems security: limitations, issues and future trends. Microprocessors Microsyst 77:103201. https:\/\/doi.org\/10.1016\/j.micpro.2020.103201","journal-title":"Microprocessors Microsyst"},{"issue":"24","key":"5669_CR4","doi-asserted-by":"publisher","first-page":"4481","DOI":"10.1002\/cpe.4481","volume":"31","author":"T Sanislav","year":"2019","unstructured":"Sanislav T, Zeadally S, Mois GD, Fouchal H (2019) Reliability, failure detection and prevention in cyber-physical systems (cpss) with agents. Concurr Comput: Pract Exp 31(24):4481. https:\/\/doi.org\/10.1002\/cpe.4481","journal-title":"Concurr Comput: Pract Exp"},{"key":"5669_CR5","doi-asserted-by":"publisher","unstructured":"Yang C, Sun H, Liu J, Kang J, Yin W, Wang H, Li T (2021) Uncertainty modeling and quantitative evaluation of cyber-physical systems. In: 2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC), pp 874\u2013883. https:\/\/doi.org\/10.1109\/COMPSAC51774.2021.00120","DOI":"10.1109\/COMPSAC51774.2021.00120"},{"key":"5669_CR6","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking, vol 26202649"},{"key":"5669_CR7","doi-asserted-by":"publisher","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R (eds) (2018) Handbook of model checking. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"5669_CR8","doi-asserted-by":"publisher","first-page":"101850","DOI":"10.1016\/j.sysarc.2020.101850","volume":"112","author":"A Rashid","year":"2021","unstructured":"Rashid A, Hasan O (2021) Formal analysis of the continuous dynamics of cyber\u2013physical systems using theorem proving. J Syst Architect 112:101850. https:\/\/doi.org\/10.1016\/j.sysarc.2020.101850","journal-title":"J Syst Architect"},{"key":"5669_CR9","doi-asserted-by":"publisher","first-page":"104656","DOI":"10.1016\/j.ic.2020.104656","volume":"282","author":"M Fr\u00e4nzle","year":"2022","unstructured":"Fr\u00e4nzle M, Shirmohammadi M, Swaminathan M, Worrell J (2022) Costs and rewards in priced timed automata. Inf Comput 282:104656. https:\/\/doi.org\/10.1016\/j.ic.2020.104656","journal-title":"Inf Comput"},{"key":"5669_CR10","doi-asserted-by":"publisher","first-page":"25371","DOI":"10.1109\/ACCESS.2021.3057911","volume":"9","author":"X Zhang","year":"2021","unstructured":"Zhang X, Li J (2021) Power control for cognitive users of perception layer in complex industrial cps based on dqn. IEEE Access 9:25371\u201325382. https:\/\/doi.org\/10.1109\/ACCESS.2021.3057911","journal-title":"IEEE Access"},{"key":"5669_CR11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3174408","author":"K Tei","year":"2022","unstructured":"Tei K, Tahara Y, Ohsuga A (2022) Towards scalable model checking of reflective systems via labeled transition systems. IEEE Trans Software Eng. https:\/\/doi.org\/10.1109\/TSE.2022.3174408","journal-title":"IEEE Trans Software Eng"},{"key":"5669_CR12","doi-asserted-by":"publisher","first-page":"26314","DOI":"10.1109\/ACCESS.2019.2899761","volume":"7","author":"Y Yang","year":"2019","unstructured":"Yang Y, Zu Q, Ke W, Zhang M, Li X (2019) Real-time system modeling and verification through labeled transition system analyzer. IEEE Access 7:26314\u201326323. https:\/\/doi.org\/10.1109\/ACCESS.2019.2899761","journal-title":"IEEE Access"},{"key":"5669_CR13","doi-asserted-by":"publisher","first-page":"13089","DOI":"10.1109\/ACCESS.2022.3146390","volume":"10","author":"L Rao","year":"2022","unstructured":"Rao L, Liu S, Peng H (2022) An integrated formal method combining labeled transition system and event-b for system model refinement. IEEE Access 10:13089\u201313102. https:\/\/doi.org\/10.1109\/ACCESS.2022.3146390","journal-title":"IEEE Access"},{"key":"5669_CR14","doi-asserted-by":"publisher","unstructured":"Cleaveland R, Roscoe AW, Smolka SA (2018) Process algebra and model checking. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer, Cham, pp 1149\u20131195. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_32","DOI":"10.1007\/978-3-319-10575-8_32"},{"issue":"9","key":"5669_CR15","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier C, Haverkort BR, Hermanns H, Katoen J-P (2010) Performance evaluation and model checking join forces. Commun ACM 53(9):76\u201385. https:\/\/doi.org\/10.1145\/1810891.1810912","journal-title":"Commun ACM"},{"issue":"1","key":"5669_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-009-0088-7","volume":"36","author":"C Baier","year":"2010","unstructured":"Baier C, Cloth L, Haverkort BR, Hermanns H, Katoen J-P (2010) Performability assessment by model checking of Markov reward models. Formal Methods Syst Design 36(1):1\u201336. https:\/\/doi.org\/10.1007\/s10703-009-0088-7","journal-title":"Formal Methods Syst Design"},{"key":"5669_CR17","doi-asserted-by":"publisher","unstructured":"Qian L, Liu J (2020) Safe reinforcement learning via probabilistic timed computation tree logic. In: 2020 International Joint Conference on Neural Networks (IJCNN), pp 1\u20138. https:\/\/doi.org\/10.1109\/IJCNN48605.2020.9207384","DOI":"10.1109\/IJCNN48605.2020.9207384"},{"issue":"2","key":"5669_CR18","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193\u2013244. https:\/\/doi.org\/10.1006\/inco.1994.1045","journal-title":"Inf Comput"},{"key":"5669_CR19","doi-asserted-by":"publisher","unstructured":"Chaki S, Gurfinkel A (2018) Bdd-based symbolic model checking. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer, Cham, pp 219\u2013245. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_8","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"5669_CR20","doi-asserted-by":"publisher","unstructured":"Clarke EM, Grumberg O, Mcmillan KL, Zhao X (2003) Efficient generation of counterexamples and witnesses in symbolic model checking. International Journal on Software Tools for Technology Transfer (STTT). https:\/\/doi.org\/10.1007\/11513988_9","DOI":"10.1007\/11513988_9"},{"key":"5669_CR21","doi-asserted-by":"publisher","unstructured":"Ciesinski F, Baier C, Gr\u00f6\u00dfer M, Parker D (2008) Generating compact mtbdd-representations from probmela specifications. In: Havelund K, Majumdar R, Palsberg J (eds) Model checking software. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, pp 60\u201376. https:\/\/doi.org\/10.1007\/978-3-540-85114-1_7","DOI":"10.1007\/978-3-540-85114-1_7"},{"issue":"1","key":"5669_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H Hermanns","year":"2003","unstructured":"Hermanns H, Kwiatkowska M, Norman G, Parker D, Siegle M (2003) On the use of mtbdds for performability analysis and verification of stochastic systems. J Logic Algebraic Program 56(1):23\u201367. https:\/\/doi.org\/10.1016\/S1567-8326(02)00066-8","journal-title":"J Logic Algebraic Program"},{"key":"5669_CR23","doi-asserted-by":"publisher","unstructured":"Mikusek P (2009) Multi-terminal bdd synthesis and applications. In: 2009 International Conference on Field Programmable Logic and Applications, pp 721\u2013722. https:\/\/doi.org\/10.1109\/FPL.2009.5272326","DOI":"10.1109\/FPL.2009.5272326"},{"issue":"2","key":"5669_CR24","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita M, McGeer PC, Yang JC-Y (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst Design 10(2):149\u2013169. https:\/\/doi.org\/10.1023\/A:1008647823331","journal-title":"Formal Methods Syst Design"},{"key":"5669_CR25","doi-asserted-by":"publisher","unstructured":"Stefanakos I, Calinescu R, Douthwaite J, Aitken J, Law J (2022) Safety controller synthesis for a mobile manufacturing cobot. In: Schlingloff B-H, Chai M (eds) Software engineering and formal methods, vol 13550, pp 271\u2013287. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-17108-6_17","DOI":"10.1007\/978-3-031-17108-6_17"},{"key":"5669_CR26","doi-asserted-by":"publisher","unstructured":"Debbi H (2021) Modeling and performance analysis of resource provisioning in cloud computing using probabilistic model checking. Informatica. https:\/\/doi.org\/10.31449\/inf.v45i4.3308","DOI":"10.31449\/inf.v45i4.3308"},{"issue":"9","key":"5669_CR27","doi-asserted-by":"publisher","first-page":"4973","DOI":"10.1002\/cpe.4973","volume":"31","author":"X Guo","year":"2019","unstructured":"Guo X (2019) Performance analysis of Israeli\u2013Jalfon\u2019s algorithm using probabilistic model checking. Concurr Comput: Pract Exp 31(9):4973. https:\/\/doi.org\/10.1002\/cpe.4973","journal-title":"Concurr Comput: Pract Exp"},{"issue":"7","key":"5669_CR28","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska M, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205(7):1027\u20131077. https:\/\/doi.org\/10.1016\/j.ic.2007.01.004","journal-title":"Inf Comput"},{"key":"5669_CR29","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle M, Hahn EM, Hermanns H, Wolovick N, Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control - HSCC \u201911. ACM Press, Chicago, IL, USA, , p 43. https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"key":"5669_CR30","doi-asserted-by":"crossref","unstructured":"Clarke EM (1997) Model checking. In: Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18\u201320, 1997 Proceedings 17. Springer, pp 54\u201356","DOI":"10.1007\/BFb0058022"},{"key":"5669_CR31","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s13272-015-0149-0","volume":"6","author":"J Shetty","year":"2015","unstructured":"Shetty J, Lawson CP, Shahneh AZ (2015) Simulation for temperature control of a military aircraft cockpit to avoid pilot\u2019s thermal stress. CEAS Aeronaut J 6:319\u2013333","journal-title":"CEAS Aeronaut J"},{"key":"5669_CR32","doi-asserted-by":"publisher","first-page":"104618","DOI":"10.1016\/j.ic.2020.104618","volume":"279","author":"R Lanotte","year":"2021","unstructured":"Lanotte R, Merro M, Tini S (2021) A probabilistic calculus of cyber-physical systems. Inf Comput 279:104618. https:\/\/doi.org\/10.1016\/j.ic.2020.104618","journal-title":"Inf Comput"},{"key":"5669_CR33","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.scico.2018.05.005","volume":"166","author":"D Du","year":"2018","unstructured":"Du D, Huang P, Jiang K, Mallet F (2018) pcssl: A stochastic extension to marte\/ccsl for modeling uncertainty in cyber physical systems. Sci Comput Program 166:71\u201388. https:\/\/doi.org\/10.1016\/j.scico.2018.05.005","journal-title":"Sci Comput Program"},{"key":"5669_CR34","doi-asserted-by":"publisher","unstructured":"Basile D, Di\u00a0Giandomenico F, Gnesi S (2019) On quantitative assessment of reliability and energy consumption indicators in railway systems. In: Kharchenko V, Kondratenko Y, Kacprzyk J (eds) Green IT Engineering: Social, Business and Industrial Applications. Springer, Cham, pp 423\u2013447. https:\/\/doi.org\/10.1007\/978-3-030-00253-4_18","DOI":"10.1007\/978-3-030-00253-4_18"},{"key":"5669_CR35","unstructured":"Parker DA (2003) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05669-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11227-023-05669-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-023-05669-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,14]],"date-time":"2024-02-14T10:24:16Z","timestamp":1707906256000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11227-023-05669-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,3]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["5669"],"URL":"https:\/\/doi.org\/10.1007\/s11227-023-05669-3","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,3]]},"assertion":[{"value":"12 September 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 October 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":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"The authors declare that they have no known competing fnancial interests or personal relationships that could have appeared to infuence the work reported in this paper.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}