{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T06:43:19Z","timestamp":1740120199861,"version":"3.37.3"},"reference-count":45,"publisher":"World Scientific Pub Co Pte Ltd","issue":"02","funder":[{"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\/501100012130","name":"Aviation Science Foundation of China","doi-asserted-by":"crossref","award":["20185152035","20150652008"],"award-info":[{"award-number":["20185152035","20150652008"]}],"id":[{"id":"10.13039\/501100012130","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["NJ2020022","NJ2019010","NJ20170007"],"award-info":[{"award-number":["NJ2020022","NJ2019010","NJ20170007"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:p> Probabilistic behavior is omnipresent in computer-controlled systems, in particular, so-called safety-critical hybrid systems, due to various reasons, like uncertain environments or fundamental properties of nature. In this paper, we extend the existing hybrid process algebra ACP[Formula: see text] with probability without sacrificing the nondeterministic choice operator. The existing approximate probabilistic bisimulation relation is fragile and not robust in the sense of being dependent on the deviation range of the transition probability. To overcome this defect, a novel approximate probabilistic bisimulation is proposed which is inspired by the idea of Probably Approximately Correct (PAC) by relaxing the constraints of transition probability deviation range. Traditional temporal logics, even probabilistic temporal logics, are expressive enough, but they are limited to producing only true or false responses, as they are still logics and not suitable for performance evaluation. To settle this problem, we present a new performance evaluation language that expands quantitative analysis from the value range of [Formula: see text] to real number to reason over probabilistic systems. After that, the corresponding algorithms for performance evaluation are given. Finally, an industrial example is given to demonstrate the effectiveness of our method. <\/jats:p>","DOI":"10.1142\/s0218194022500103","type":"journal-article","created":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:42:30Z","timestamp":1649155350000},"page":"283-315","source":"Crossref","is-referenced-by-count":1,"title":["Formal Modeling and Performance Evaluation for Hybrid Systems: A Probabilistic Hybrid Process Algebra-Based Approach"],"prefix":"10.1142","volume":"32","author":[{"given":"Fujun","family":"Wang","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zining","family":"Cao","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"},{"name":"Key Laboratory of Safety-Critical Software, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"},{"name":"Science and Technology on Electro-optic Control Laboratory, Luoyang 471000, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lixing","family":"Tan","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"Li","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2022,4,25]]},"reference":[{"key":"S0218194022500103BIB001","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"Henzinger T. A.","year":"2000"},{"issue":"1","key":"S0218194022500103BIB002","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.jlap.2005.10.005","volume":"68","author":"van Beek D. A.","year":"2006","journal-title":"J. Logic Algebraic Program"},{"key":"S0218194022500103BIB003","first-page":"511","volume-title":"Int. Hybrid Systems Workshop","author":"Zhou C. C.","year":"1996"},{"key":"S0218194022500103BIB004","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-642-39721-9_5","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","author":"Zhan N. J.","year":"2013"},{"issue":"2","key":"S0218194022500103BIB005","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.jlap.2004.02.001","volume":"62","author":"Cuijpers P. J. L.","year":"2005","journal-title":"J. Logic Algebraic Program."},{"key":"S0218194022500103BIB006","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/3-540-36580-X_32","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control","author":"Rounds W. C.","year":"2003"},{"issue":"2","key":"S0218194022500103BIB007","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/j.tcs.2004.04.019","volume":"335","author":"Bergstra J. A.","year":"2005","journal-title":"Theor. Comput. Sci."},{"key":"S0218194022500103BIB008","first-page":"7","volume-title":"The Fourth Int. Conf. Computational Logics, Algebras, Programming, Tools, and Benchmarking","author":"Cao Z. N.","year":"2013"},{"key":"S0218194022500103BIB009","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-319-53733-7_8","volume-title":"Int. Conf. Language and Automata Theory and Applications","author":"Lanotte R.","year":"2017"},{"key":"S0218194022500103BIB010","doi-asserted-by":"crossref","first-page":"104618","DOI":"10.1016\/j.ic.2020.104618","volume":"279","author":"Lanotte M. M.","year":"2021","journal-title":"Inform. Comput."},{"key":"S0218194022500103BIB011","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-319-25942-0_6","volume-title":"Int. Symp. Dependable Software Engineering: Theories, Tools, and Applications","author":"Peng Y.","year":"2015"},{"key":"S0218194022500103BIB012","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008330914786"},{"issue":"2","key":"S0218194022500103BIB013","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1142\/S0218194005002385","volume":"15","author":"Man K. L.","year":"2005","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"S0218194022500103BIB014","first-page":"6","author":"Khadim U.","year":"2006","journal-title":"Comput. Sci. Rep."},{"key":"S0218194022500103BIB016","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Int. Conf. Foundations of Software Technology and Theoretical Computer Science","author":"Bianco A.","year":"1995"},{"key":"S0218194022500103BIB017","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebra","author":"Jonsson B.","year":"2001"},{"volume-title":"Machine Learning: A Theoretical Approach","year":"2014","author":"Natarajan B. K.","key":"S0218194022500103BIB018"},{"issue":"11","key":"S0218194022500103BIB019","doi-asserted-by":"crossref","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"27","author":"Waltz D.","year":"1984","journal-title":"Commun. ACM"},{"key":"S0218194022500103BIB020","first-page":"371","volume-title":"Int. Conf. Concurrency Theory","author":"Cattani S.","year":"2002"},{"issue":"50","key":"S0218194022500103BIB021","doi-asserted-by":"crossref","first-page":"4291","DOI":"10.1016\/j.tcs.2010.09.003","volume":"411","author":"Lanotte R.","year":"2010","journal-title":"Theor. Comput. Sci."},{"key":"S0218194022500103BIB022","first-page":"702","volume-title":"Int. Symp. Formal Methods","author":"Yan G. G.","year":"2016"},{"key":"S0218194022500103BIB024","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.895849"},{"key":"S0218194022500103BIB025","first-page":"443","volume-title":"Proc. IFIP TC2 Working Conf. Programming Concepts and Methods","author":"Giacalone A.","year":"1990"},{"volume-title":"Principles of Model Checking","year":"2008","author":"Baier C.","key":"S0218194022500103BIB026"},{"key":"S0218194022500103BIB027","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Int. Conf. Computer Aided Verification","author":"Aziz A.","year":"1996"},{"key":"S0218194022500103BIB028","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"S0218194022500103BIB029","first-page":"35","volume-title":"Int. Conf. Runtime Verification","author":"Bartocci E.","year":"2018"},{"issue":"3","key":"S0218194022500103BIB030","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/s00165-018-0457-3","volume":"30","author":"Jing Y. P.","year":"2018","journal-title":"Formal Aspects Comput."},{"key":"S0218194022500103BIB031","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/j.peva.2015.04.003","volume":"90","author":"Ballarini P.","year":"2015","journal-title":"Perform. Eval."},{"key":"S0218194022500103BIB032","first-page":"413","volume-title":"Proc. 17th Annual IEEE Symp. Logic in Computer Science","author":"Desharnais J.","year":"2002"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner R.","key":"S0218194022500103BIB033"},{"key":"S0218194022500103BIB036","doi-asserted-by":"crossref","first-page":"109386","DOI":"10.1016\/j.automatica.2020.109386","volume":"125","author":"Gatsis K.","year":"2021","journal-title":"Automatica"},{"issue":"4","key":"S0218194022500103BIB037","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2739046","volume":"14","author":"Bak S.","year":"2015","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"S0218194022500103BIB038","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"S0218194022500103BIB039","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Int. Conf. Computer Aided Verification","author":"Aziz A.","year":"1995"},{"issue":"3","key":"S0218194022500103BIB040","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"Alur R.","year":"1996","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"9","key":"S0218194022500103BIB041","doi-asserted-by":"crossref","first-page":"3029","DOI":"10.1109\/TCOMM.2015.2434384","volume":"63","author":"Rappaport T. S.","year":"2015","journal-title":"IEEE Trans. Commun."},{"issue":"4","key":"S0218194022500103BIB042","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1145\/1851275.1851203","volume":"40","author":"Halperin D.","year":"2010","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"volume-title":"Introduction to Numerical Analysis","year":"2013","author":"Stoer J.","key":"S0218194022500103BIB043"},{"key":"S0218194022500103BIB044","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"22","key":"S0218194022500103BIB045","doi-asserted-by":"crossref","first-page":"2202","DOI":"10.1016\/j.tcs.2010.01.027","volume":"411","author":"Tini S.","year":"2010","journal-title":"Theor. Comput. Sci."},{"key":"S0218194022500103BIB046","first-page":"32","volume-title":"Proc. Combined 20th Int. Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics","author":"Gebler D.","year":"2013"},{"key":"S0218194022500103BIB047","first-page":"148","volume-title":"Proc. Ninth Workshop on Quantitative Aspects of Programming Languages","author":"Tracol M.","year":"2011"},{"key":"S0218194022500103BIB048","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1109\/QEST.2008.42","volume-title":"2008 Fifth Int. Conf. Quantitative Evaluation of Systems","author":"Desharnais L. F.","year":"2008"},{"key":"S0218194022500103BIB049","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-319-06880-0_2","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden","author":"Alessandro N. G. Abate.","year":"2014"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194022500103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,26]],"date-time":"2022-04-26T02:44:39Z","timestamp":1650941079000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218194022500103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2]]},"references-count":45,"journal-issue":{"issue":"02","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["10.1142\/S0218194022500103"],"URL":"https:\/\/doi.org\/10.1142\/s0218194022500103","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"type":"print","value":"0218-1940"},{"type":"electronic","value":"1793-6403"}],"subject":[],"published":{"date-parts":[[2022,2]]}}}