{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T03:57:34Z","timestamp":1782359854783,"version":"3.54.5"},"reference-count":27,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","funder":[{"name":"the Korea government","award":["2019R1F1A1062828"],"award-info":[{"award-number":["2019R1F1A1062828"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2020,4]]},"abstract":"<jats:p> The Alternating-time Temporal Logic (ATL) is a temporal logic for formal verification of open systems, which supports selective quantification over paths. The open system can be represented as a game where the system and the environment pick their moves in turn or simultaneously. The ATL model checker Mocha has been developed by using Binary Decision Diagrams (BDDs), and successfully employed for open system verification. However, since Mocha symbolically manipulates a set of states by a BDD, it is hard to generate a winning strategy as a witness or a counter-example. In this paper, we propose a novel algorithm to efficiently construct a winning strategy tree and report that our technique has been successfully implemented on Mocha. <\/jats:p>","DOI":"10.1142\/s0218194020500199","type":"journal-article","created":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T07:46:16Z","timestamp":1588751176000},"page":"555-573","source":"Crossref","is-referenced-by-count":2,"title":["Winning Strategy Tree Construction for BDD-Based ATL Model Checkers"],"prefix":"10.1142","volume":"30","author":[{"given":"Wonhong","family":"Nam","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Konkuk University, Seoul 05029, Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Haejin","family":"Yang","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Konkuk University, Seoul 05029, Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hyunyoung","family":"Kil","sequence":"additional","affiliation":[{"name":"Department of Software, Korea Aerospace University, Goyang, Gyeonggi 10540, Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2020,5,6]]},"reference":[{"key":"S0218194020500199BIB001","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"S0218194020500199BIB002","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"S0218194020500199BIB003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028774"},{"key":"S0218194020500199BIB004","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0179-0"},{"key":"S0218194020500199BIB005","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"S0218194020500199BIB006","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1734"},{"key":"S0218194020500199BIB007","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"S0218194020500199BIB008","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"S0218194020500199BIB009","first-page":"52","volume-title":"Proc. Workshop on Logic of Programs","author":"Clarke E.","year":"1981"},{"key":"S0218194020500199BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"S0218194020500199BIB011","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"S0218194020500199BIB012","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029814"},{"key":"S0218194020500199BIB013","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39910-0_9"},{"key":"S0218194020500199BIB014","volume-title":"Introduction to Algorithms","author":"Cormen T. H.","year":"2016","edition":"3"},{"key":"S0218194020500199BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"S0218194020500199BIB017","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4"},{"key":"S0218194020500199BIB018","doi-asserted-by":"publisher","DOI":"10.1109\/TSSC.1968.300136"},{"key":"S0218194020500199BIB019","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_5"},{"key":"S0218194020500199BIB020","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"S0218194020500199BIB021","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-005-0944-9"},{"key":"S0218194020500199BIB022","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"S0218194020500199BIB023","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_18"},{"key":"S0218194020500199BIB024","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_18"},{"key":"S0218194020500199BIB025","first-page":"120","volume-title":"IARCS Annual Conf. Foundations of Software Technology and Theoretical Computer Science","author":"Lopes A. D. C.","year":"2010"},{"key":"S0218194020500199BIB026","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"S0218194020500199BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_32"},{"key":"S0218194020500199BIB028","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160665"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194020500199","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T07:46:57Z","timestamp":1588751217000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194020500199"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4]]},"references-count":27,"journal-issue":{"issue":"04","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["10.1142\/S0218194020500199"],"URL":"https:\/\/doi.org\/10.1142\/s0218194020500199","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4]]}}}