{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,18]],"date-time":"2024-07-18T02:09:09Z","timestamp":1721268549634},"reference-count":27,"publisher":"World Scientific Pub Co Pte Lt","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2019,10]]},"abstract":"<jats:p> Counterexample-guided abstraction refinement (CEGAR) is an extremely successful methodology for combating the state-space explosion problem in model checking. State-space explosion problem is more serious in the field of stochastic model checking, and it is still a challengeable problem to apply CEGAR in stochastic model checking effectively. In this paper, we formalize the problem of applying CEGAR in stochastic model checking, and propose a novel CEGAR framework for it. In our framework, the abstract model is presented by a quotient probabilistic automaton by making a set of variables or latches invisible, which can distinguish more degrees of abstraction for each variable. The counterexample is described by a diagnostic sub-model. Validating counterexample is performed on diagnostic loop paths, and the directed explicit state-space search algorithm is used for searching diagnostic loop paths. Sample learning, particle swarm optimization algorithm (PSO) and some effective heuristics are integrated for refining abstract model guided by invalid counterexample. A prototype tool is implemented for the framework, and the feasibility and efficiency are shown by some large cases. <\/jats:p>","DOI":"10.1142\/s0218194019500463","type":"journal-article","created":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T08:54:21Z","timestamp":1572598461000},"page":"1465-1495","source":"Crossref","is-referenced-by-count":2,"title":["A PSO-Based CEGAR Framework for Stochastic Model Checking"],"prefix":"10.1142","volume":"29","author":[{"given":"Yan","family":"Ma","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, 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 210016, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Logistics Science and Engineering, Shanghai Maritime University, Shanghai, 201306, P. R. China"},{"name":"School of Computing, National University of Singapore, 117417, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2019,11,1]]},"reference":[{"issue":"11","key":"S0218194019500463BIB001","first-page":"2145","volume":"38","author":"Liu Y.","year":"2015","journal-title":"J. Comput."},{"key":"S0218194019500463BIB002","first-page":"266","volume-title":"Logic in Computer Science","author":"Jonsson B.","year":"1991"},{"key":"S0218194019500463BIB003","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"S0218194019500463BIB004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"S0218194019500463BIB005","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898.ch7"},{"key":"S0218194019500463BIB006","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"S0218194019500463BIB007","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"S0218194019500463BIB008","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44804-7_3"},{"key":"S0218194019500463BIB009","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45605-8_5"},{"key":"S0218194019500463BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_5"},{"key":"S0218194019500463BIB011","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2009.5"},{"key":"S0218194019500463BIB012","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838553"},{"key":"S0218194019500463BIB013","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.829807"},{"key":"S0218194019500463BIB014","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.105"},{"key":"S0218194019500463BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"S0218194019500463BIB016","first-page":"104","volume-title":"Proc. Conf. Uncertainty in Artificial Intelligence","author":"Chatterjee K.","year":"2005"},{"key":"S0218194019500463BIB017","doi-asserted-by":"publisher","DOI":"10.1142\/S021819401650039X"},{"key":"S0218194019500463BIB018","doi-asserted-by":"publisher","DOI":"10.1016\/0377-2217(95)00159-X"},{"key":"S0218194019500463BIB019","doi-asserted-by":"publisher","DOI":"10.1057\/palgrave.jors.2601317"},{"key":"S0218194019500463BIB020","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2001.934374"},{"key":"S0218194019500463BIB021","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2006.880326"},{"key":"S0218194019500463BIB022","first-page":"1","author":"Khanesar M. A.","year":"2009","journal-title":"Particle Swarm Optim."},{"key":"S0218194019500463BIB023","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.1997.637339"},{"key":"S0218194019500463BIB024","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"S0218194019500463BIB025","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2011.19"},{"key":"S0218194019500463BIB026","doi-asserted-by":"publisher","DOI":"10.1145\/290163.290168"},{"key":"S0218194019500463BIB027","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.34"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194019500463","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T08:54:42Z","timestamp":1572598482000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194019500463"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":27,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["10.1142\/S0218194019500463"],"URL":"https:\/\/doi.org\/10.1142\/s0218194019500463","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10]]}}}