{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T21:50:54Z","timestamp":1771019454396,"version":"3.50.1"},"reference-count":39,"publisher":"World Scientific Pub Co Pte Ltd","issue":"11","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\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["NJ2024030"],"award-info":[{"award-number":["NJ2024030"]}],"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":["NJ2020022"],"award-info":[{"award-number":["NJ2020022"]}],"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":[[2024,11]]},"abstract":"<jats:p> Temporal Logics are a rich variety of logical systems designed for specifying properties over time, and about events and changes in the world over time. Traditional temporal logic, however, is limited to binary outcomes true or false and lacks the capacity to specify performance properties of a system such as the maximum, minimum, or average costs between states. Current languages do not accommodate the quantification of such performance properties, especially in scenarios involving infinite execution paths where performance property like cumulative sums may fail to converge. To this end, this paper introduces a novel formal language aimed at assessing system performance, which encapsulates not only temporal dynamics but also various performance-related properties. In this study, this paper utilizes reinforcement learning techniques to compute the values of performance property formulas. Finally, in the experimental part, a formal language representation of system performance properties was implemented, and the values of the performance property formulas were computed using reinforcement learning. The effectiveness and feasibility of the proposed method were validated. <\/jats:p>","DOI":"10.1142\/s0218194024500372","type":"journal-article","created":{"date-parts":[[2024,7,19]],"date-time":"2024-07-19T12:43:00Z","timestamp":1721392980000},"page":"1783-1805","source":"Crossref","is-referenced-by-count":4,"title":["A Formal Language for Performance Evaluation Based on Reinforcement Learning"],"prefix":"10.1142","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9902-3859","authenticated-orcid":false,"given":"Fujun","family":"Wang","sequence":"first","affiliation":[{"name":"College of Information Engineering, Yangzhou Polytechnic Institute, Yangzhou 225127, P.\u00a0R.\u00a0China"},{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2978-2697","authenticated-orcid":false,"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"},{"name":"College of Information Engineering, Taizhou University, Taizhou 225300, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4673-200X","authenticated-orcid":false,"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":"Ministry Key Laboratory for Safety-Critical Software Development and Verification, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, P. R. China"},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210023, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6647-7950","authenticated-orcid":false,"given":"Yan","family":"Ma","sequence":"additional","affiliation":[{"name":"College of Accounts, Nanjing University of Finance and Economics, Nanjing 210023, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8966-1451","authenticated-orcid":false,"given":"Li","family":"Zhang","sequence":"additional","affiliation":[{"name":"College of Information Engineering, Yangzhou Polytechnic Institute, Yangzhou 225127, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2024,9,30]]},"reference":[{"key":"S0218194024500372BIB001","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00305-4"},{"key":"S0218194024500372BIB002","first-page":"1","volume-title":"School Organized by the European Educational Forum","author":"Herzog U.","year":"2000"},{"key":"S0218194024500372BIB003","doi-asserted-by":"publisher","DOI":"10.1145\/1810891.1810912"},{"key":"S0218194024500372BIB004","volume-title":"Performance Evaluation: Origins and Directions","author":"Haring G.","year":"2003"},{"key":"S0218194024500372BIB005","volume-title":"Software Reliability Methods","author":"Peled D. A.","year":"2013"},{"key":"S0218194024500372BIB006","volume-title":"Competitive Markov Decision Processes","author":"Filar J.","year":"2012"},{"key":"S0218194024500372BIB007","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.39.10.1095"},{"key":"S0218194024500372BIB008","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008"},{"key":"S0218194024500372BIB009","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"S0218194024500372BIB010","first-page":"52","volume-title":"Workshop on Logic of Programs","author":"Clarke E. M.","year":"1981"},{"key":"S0218194024500372BIB011","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"S0218194024500372BIB012","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.22"},{"key":"S0218194024500372BIB013","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"S0218194024500372BIB014","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v38i16.29679"},{"key":"S0218194024500372BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_35"},{"key":"S0218194024500372BIB016","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"S0218194024500372BIB017","doi-asserted-by":"publisher","DOI":"10.1145\/1805950.1805953"},{"key":"S0218194024500372BIB018","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_6"},{"key":"S0218194024500372BIB019","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.033"},{"key":"S0218194024500372BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_79"},{"key":"S0218194024500372BIB021","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_11"},{"key":"S0218194024500372BIB022","first-page":"697","volume-title":"7th Int. Conf. Autonomous Agents and Multiagent Systems","author":"Jamroga W.","year":"2008"},{"key":"S0218194024500372BIB023","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_37"},{"key":"S0218194024500372BIB024","doi-asserted-by":"publisher","DOI":"10.1587\/transfun.2023KEP0016"},{"key":"S0218194024500372BIB025","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2022.104351"},{"key":"S0218194024500372BIB026","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2023.3341775"},{"key":"S0218194024500372BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0457-3"},{"key":"S0218194024500372BIB028","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2015.04.003"},{"key":"S0218194024500372BIB029","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194022500103"},{"key":"S0218194024500372BIB030","doi-asserted-by":"publisher","DOI":"10.1109\/ISKE54062.2021.9755388"},{"key":"S0218194024500372BIB031","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i9.16919"},{"key":"S0218194024500372BIB032","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"S0218194024500372BIB033","volume-title":"Model Checking","author":"Edmund M.","year":"1999"},{"key":"S0218194024500372BIB034","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0218194024500372BIB035","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"S0218194024500372BIB036","volume-title":"Reinforcement Learning: An Introduction","author":"Sutton R. S.","year":"2018"},{"key":"S0218194024500372BIB037","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-2195-2"},{"key":"S0218194024500372BIB038","volume-title":"Tense Logic and the Theory of Linear Order","author":"Kamp J. A. W.","year":"1968"},{"key":"S0218194024500372BIB039","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567551"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194024500372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T05:13:33Z","timestamp":1732079613000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218194024500372"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,30]]},"references-count":39,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2024,11]]}},"alternative-id":["10.1142\/S0218194024500372"],"URL":"https:\/\/doi.org\/10.1142\/s0218194024500372","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,30]]}}}