{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:17:20Z","timestamp":1740107840409,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"17-18","license":[{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"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":"publisher","award":["61572253"],"award-info":[{"award-number":["61572253"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["NJ2020022 and NJ2019010"],"award-info":[{"award-number":["NJ2020022 and NJ2019010"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2024,9]]},"DOI":"10.1007\/s00500-024-09793-x","type":"journal-article","created":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T18:40:56Z","timestamp":1722451256000},"page":"9137-9155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Specification and counterexample generation for cyber-physical systems"],"prefix":"10.1007","volume":"28","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":"Fujun","family":"Wang","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":[[2024,7,31]]},"reference":[{"key":"9793_CR1","unstructured":"Akram\u00a0AL-Saati N, Abd-AlKareem\u00a0Alabajee M (2020) A comparative study on parameter estimation in software reliability modeling using swarm intelligence. arXiv preprint arXiv:2003.04770"},{"issue":"1","key":"9793_CR2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/TSE.2009.57","volume":"36","author":"H Aljazzar","year":"2010","unstructured":"Aljazzar H, Leue S (2010) Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans Software Eng 36(1):37\u201360","journal-title":"IEEE Trans Software Eng"},{"key":"9793_CR3","doi-asserted-by":"crossref","unstructured":"Andr\u00e9s ME, D\u2019Argenio P, van Rossum P (2008) Significant diagnostic counterexamples in probabilistic model checking. In: Haifa Verification Conference, pp. 129\u2013148. Springer","DOI":"10.1007\/978-3-642-01702-5_15"},{"key":"9793_CR4","first-page":"173","volume-title":"Lecture notes in computer science","author":"G Barbon","year":"2018","unstructured":"Barbon G, Leroy V, Sala\u00fcn G (2018) Counterexample simplification for liveness property violation. In: Johnsen EB, Schaefer I (eds) Lecture notes in computer science. Software Engineering and Formal Methods, Cham, pp 173\u2013188"},{"key":"9793_CR5","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka M, Hensel C, Junges S, Katoen JP (2019) Counterexample-driven synthesis for probabilistic program sketches. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Lecture Notes in Computer Science, pp. 101\u2013120. Formal Methods \u2013 The Next 30 Years, Cham","DOI":"10.1007\/978-3-030-30942-8_8"},{"key":"9793_CR6","doi-asserted-by":"crossref","unstructured":"Chen N, Geng S, Li L (2021) Modeling and verification of cps based on uncertain hybrid timed automaton. In: 2021 IEEE Intl Conf on Dependable, Autonomic and Secure Computing, Intl Conf on Pervasive Intelligence and Computing, Intl Conf on Cloud and Big Data Computing, Intl Conf on Cyber Science and Technology Congress (DASC\/PiCom\/CBDCom\/CyberSciTech), pp. 971\u2013978. IEEE","DOI":"10.1109\/DASC-PICom-CBDCom-CyberSciTech52372.2021.00162"},{"issue":"7","key":"9793_CR7","doi-asserted-by":"publisher","first-page":"1520","DOI":"10.1109\/TPDS.2021.3118610","volume":"33","author":"HS Chwa","year":"2022","unstructured":"Chwa HS, Baek H, Lee J (2022) Necessary feasibility analysis for mixed-criticality real-time embedded systems. IEEE Trans Parallel Distrib Syst 33(7):1520\u20131537","journal-title":"IEEE Trans Parallel Distrib Syst"},{"issue":"5","key":"9793_CR8","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"9793_CR9","doi-asserted-by":"publisher","first-page":"53215","DOI":"10.1109\/ACCESS.2020.2980891","volume":"8","author":"F Dai","year":"2020","unstructured":"Dai F, Mo Q, Qiang Z, Huang B, Kou W, Yang H (2020) A choreography analysis approach for microservice composition in cyber-physical-social systems. IEEE Access 8:53215\u201353222","journal-title":"IEEE Access"},{"key":"9793_CR10","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","journal-title":"Sci Comput Program"},{"key":"9793_CR11","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1016\/j.procs.2021.01.034","volume":"179","author":"D Foead","year":"2021","unstructured":"Foead D, Ghifari A, Kusuma MB, Hanafiah N, Gunawan E (2021) A systematic literature review of a* pathfinding. Proc Comput Sci 179:507\u2013514","journal-title":"Proc Comput Sci"},{"key":"9793_CR12","doi-asserted-by":"crossref","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, p. 43. ACM Press, Chicago, IL, USA","DOI":"10.1145\/1967701.1967710"},{"key":"9793_CR13","doi-asserted-by":"crossref","unstructured":"Gorrieri R, Gorrieri R (2017) Labeled transition systems. Process Algebras for Petri Nets: The Alphabetization of Distributed Systems, 15\u201334","DOI":"10.1007\/978-3-319-55559-1_2"},{"issue":"15","key":"9793_CR14","doi-asserted-by":"publisher","first-page":"4850","DOI":"10.1002\/cpe.4850","volume":"32","author":"I Graja","year":"2020","unstructured":"Graja I, Kallel S, Guermouche N, Cheikhrouhou S, Hadj Kacem A (2020) A comprehensive survey on modeling of cyber-physical systems. Concurr Comput Pract Exp 32(15):4850","journal-title":"Concurr Comput Pract Exp"},{"issue":"2","key":"9793_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T Han","year":"2009","unstructured":"Han T, Katoen J-P, Berteun D (2009) Counterexample generation in probabilistic model checking. IEEE Trans Software Eng 35(2):241\u2013257","journal-title":"IEEE Trans Software Eng"},{"key":"9793_CR16","doi-asserted-by":"crossref","unstructured":"Han T, Katoen JP (2007) Counterexamples in probabilistic model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 72\u201386. Springer","DOI":"10.1007\/978-3-540-71209-1_8"},{"issue":"21","key":"9793_CR17","doi-asserted-by":"publisher","first-page":"5613","DOI":"10.1002\/cpe.5613","volume":"32","author":"K Kavitha","year":"2020","unstructured":"Kavitha K, Sharma SC (2020) Performance analysis of aco-based improved virtual machine allocation in cloud for iot-enabled healthcare. Concurr Comput Pract Exp 32(21):5613","journal-title":"Concurr Comput Pract Exp"},{"key":"9793_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/j.matpr.2019.05.363","volume":"21","author":"V Kesavan","year":"2020","unstructured":"Kesavan V, Kamalakannan R, Sudhakarapandian R, Sivakumar P (2020) Heuristic and meta-heuristic algorithms for solving medium and large scale sized cellular manufacturing system np-hard problems: A comprehensive review. Mater Today Proc 21:66\u201372","journal-title":"Mater Today Proc"},{"key":"9793_CR19","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 (2011) Prism 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification, vol 6806. Springer, Berlin, pp 585\u2013591"},{"key":"9793_CR20","doi-asserted-by":"crossref","unstructured":"Lalgudi KN, Papaefthymiou MC (1997) Computing strictly-second shortest paths. Inf Process Lett 63(4):177\u2013181","DOI":"10.1016\/S0020-0190(97)00122-1"},{"key":"9793_CR21","doi-asserted-by":"publisher","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","journal-title":"Inf Comput"},{"issue":"9","key":"9793_CR22","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.3390\/mi12091059","volume":"12","author":"Y Liu","year":"2021","unstructured":"Liu Y, Ma Y, Yang Y, Zheng T (2021) Counterexample generation for probabilistic model checking micro-scale cyber-physical systems. Micromachines 12(9):1059","journal-title":"Micromachines"},{"issue":"07","key":"9793_CR23","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.1142\/S021819401650039X","volume":"26","author":"Y Ma","year":"2016","unstructured":"Ma Y, Cao Z, Liu Y (2016) Counterexample generation in stochastic model checking based on pso algorithm with heuristic. Int J Software Eng Knowl Eng 26(07):1117\u20131143","journal-title":"Int J Software Eng Knowl Eng"},{"key":"9793_CR24","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.eswa.2018.07.033","volume":"114","author":"M Owais","year":"2018","unstructured":"Owais M, Osman MK (2018) Complete hierarchical multi-objective genetic algorithm for transit network design problem. Expert Syst Appl 114:143\u2013154","journal-title":"Expert Syst Appl"},{"issue":"3","key":"9793_CR25","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1109\/TITS.2015.2480885","volume":"17","author":"M Owais","year":"2016","unstructured":"Owais M, Osman MK, Moussa GS (2016) Multi-objective transit route network design as set covering problem. IEEE Trans Intell Transp Syst 17(3):670\u2013679","journal-title":"IEEE Trans Intell Transp Syst"},{"key":"9793_CR26","doi-asserted-by":"crossref","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","DOI":"10.1109\/IJCNN48605.2020.9207384"},{"key":"9793_CR27","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","journal-title":"IEEE Access"},{"key":"9793_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.swevo.2020.100762","volume":"60","author":"M Schranz","year":"2021","unstructured":"Schranz M, Di Caro GA, Schmickl T, Elmenreich W, Arvin F, \u015eekercio\u011flu A, Sende M (2021) Swarm intelligence and cyber-physical systems: concepts, challenges and future trends. Swarm Evol Comput 60:100762","journal-title":"Swarm Evol Comput"},{"key":"9793_CR29","first-page":"2","volume":"1","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 Softw Eng 1:2","journal-title":"IEEE Trans Softw Eng"},{"key":"9793_CR30","doi-asserted-by":"publisher","first-page":"03003","DOI":"10.1051\/matecconf\/201823203003","volume":"232","author":"G Wang","year":"2018","unstructured":"Wang G (2018) A comparative study of cuckoo algorithm and ant colony algorithm in optimal path problems. MATEC Web Conf 232:03003","journal-title":"MATEC Web Conf"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09793-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00500-024-09793-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09793-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T19:25:09Z","timestamp":1729193109000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00500-024-09793-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,31]]},"references-count":30,"journal-issue":{"issue":"17-18","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9793"],"URL":"https:\/\/doi.org\/10.1007\/s00500-024-09793-x","relation":{},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"type":"print","value":"1432-7643"},{"type":"electronic","value":"1433-7479"}],"subject":[],"published":{"date-parts":[[2024,7,31]]},"assertion":[{"value":"1 March 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that we have no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}