{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T11:47:35Z","timestamp":1753876055370,"version":"3.41.2"},"reference-count":41,"publisher":"Oxford University Press (OUP)","license":[{"start":{"date-parts":[[2021,9,3]],"date-time":"2021-09-03T00:00:00Z","timestamp":1630627200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100001691","name":"JSPS","doi-asserted-by":"publisher","award":["JP18K18028","JP21K11756"],"award-info":[{"award-number":["JP18K18028","JP21K11756"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Realizability is an important requirement for reactive system specifications. A reactive system interacts with an environment and responds to input events. Realizability ensures the reactive system behaves as specified, no matter how its environment provides input. Typically, reactive system specifications are given using linear temporal logic (LTL), and they can be tested to ascertain whether the specification is realizable. However, the LTL specification realizability problem is 2EXPTIME-complete, which hinders its application to large-scale systems. In this article, we present a modularization method to mitigate this computational challenge.<\/jats:p>","DOI":"10.1093\/comjnl\/bxab116","type":"journal-article","created":{"date-parts":[[2021,8,5]],"date-time":"2021-08-05T11:09:48Z","timestamp":1628161788000},"source":"Crossref","is-referenced-by-count":0,"title":["Efficient Realizability Checking by Modularization of LTL Specifications"],"prefix":"10.1093","author":[{"given":"Sohei","family":"Ito","sequence":"first","affiliation":[{"name":"Nagasaki University, School of Information and Data Sciences, Graduate School of Engineering, 1-14 Bunkyomachi, Nagasaki City 852-8521, Japan"}]},{"given":"Kenji","family":"Osari","sequence":"additional","affiliation":[{"name":"Mercari, Inc, Roppongi Hills Mori Tower, 6-10-1 Roppongi, Minato-ku, Tokyo 106-6118, Japan"}]},{"given":"Masaya","family":"Shimakawa","sequence":"additional","affiliation":[{"name":"Takushoku University, Department of Computer Science, Faculty of Engineering, 815-1 Tatemachi, Hachioji-shi, Tokyo 193-0985, Japan"}]},{"given":"Shigeki","family":"Hagihara","sequence":"additional","affiliation":[{"name":"Chitose Institute of Science and Technology, Department of Information Systems Engineering, Faculty of Science and Technology, 758-65 Bibi, Chitose, Hokkaido 066-8655, Japan"}]},{"given":"Naoki","family":"Yonezaki","sequence":"additional","affiliation":[{"name":"The Open University of Japan, Tokyo Shibuya learning center, Goto-Ikueikai Building F1, 1-10-7 Dougenzaka, Shibuya-ku, Tokyo 150-0043, Japan"}]}],"member":"286","published-online":{"date-parts":[[2021,9,3]]},"reference":[{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"2021090612514257100_ref1"},{"key":"2021090612514257100_ref2","first-page":"1","volume-title":"Proceedings of ICALP 89","author":"Abadi","year":"1989"},{"key":"2021090612514257100_ref3","first-page":"407","volume-title":"Information Modeling and Knowledge Bases IV, Frontiers in Artificial Intelligence and Applications","author":"Mori","year":"1993"},{"key":"2021090612514257100_ref4","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/75277.75293","volume-title":"Proceedings of POPL 89","author":"Pnueli","year":"1989"},{"key":"2021090612514257100_ref5","first-page":"42","volume-title":"Proceedings of SPIT 2012","author":"Shimakawa","year":"2012"},{"key":"2021090612514257100_ref6","doi-asserted-by":"crossref","first-page":"2187","DOI":"10.1587\/transinf.E96.D.2187","article-title":"Complexity of strong satisfiability problems for reactive system specifications","volume":"E96.D","author":"Shimakawa","year":"2013","journal-title":"IEICE Trans. Inf. Syst."},{"key":"2021090612514257100_ref7","first-page":"60","volume-title":"Proceedings of ICT-EurAsia 2013","author":"Shimakawa","year":"2013"},{"key":"2021090612514257100_ref8","doi-asserted-by":"crossref","first-page":"1746","DOI":"10.1587\/transinf.E97.D.1746","article-title":"Bounded strong satisfiability checking of reactive system specifications","volume":"E97.D","author":"Shimakawa","year":"2014","journal-title":"IEICE Trans. Inf. Syst."},{"key":"2021090612514257100_ref9","first-page":"629","volume-title":"Proceedings of ASE 2014","author":"Hagihara","year":"2014"},{"key":"2021090612514257100_ref10","first-page":"15","volume-title":"Proceedings of FormaliSE 2016","author":"Hagihara","year":"2016"},{"key":"2021090612514257100_ref11","first-page":"1","article-title":"Safraless LTL synthesis considering maximal realizability","volume":"54","author":"Tomita","year":"2016","journal-title":"Acta Inf."},{"key":"2021090612514257100_ref12","first-page":"5","volume-title":"Proceedings of BIOINFORMATICS 2014","author":"Ito","year":"2014"},{"key":"2021090612514257100_ref13","first-page":"93","volume-title":"Proceedings of BIOINFORMATICS 2015","author":"Ito","year":"2015"},{"key":"2021090612514257100_ref14","first-page":"117","volume-title":"Proceedings of CAV 2006","author":"Jobstmann","year":"2006"},{"key":"2021090612514257100_ref15","first-page":"652","volume-title":"Proceedings of CAV 2012","author":"Bohy","year":"2012"},{"key":"2021090612514257100_ref16","first-page":"272","volume-title":"Proceedings of TACAS 2011","author":"Ehlers","year":"2011"},{"volume-title":"Modular Synthesis of Reactive Systems","year":"1992","author":"Rosner","key":"2021090612514257100_ref17"},{"key":"2021090612514257100_ref18","first-page":"112","volume-title":"Proceedings of ATVA 2010","author":"Filiot","year":"2010"},{"key":"2021090612514257100_ref19","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","article-title":"Antichains and compositional algorithms for LTL synthesis","volume":"39","author":"Filiot","year":"2011","journal-title":"Formal Methods Sys. Des."},{"key":"2021090612514257100_ref20","first-page":"263","volume-title":"Proceedings of CAV 2009","author":"Filiot","year":"2009"},{"key":"2021090612514257100_ref21","first-page":"248","volume-title":"Proceedings of CAV 2000","author":"Somenzi","year":"2000"},{"volume-title":"Proceedings of CAV 2001","author":"Gastin","first-page":"53","key":"2021090612514257100_ref22"},{"key":"2021090612514257100_ref23","first-page":"17","volume-title":"Proceedings of BIOINFORMATICS 2017","author":"Ito","year":"2017"},{"key":"2021090612514257100_ref24","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1145\/3056662.3056702","volume-title":"Proceedings of ICSCA 2017","author":"Shimakawa","year":"2017"},{"key":"2021090612514257100_ref25","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Proceedings of Logics and Models of Concurrent Systems","author":"Pnueli","year":"1985"},{"key":"2021090612514257100_ref26","first-page":"331","volume-title":"Proceedings of TACAS 2003","author":"Cobleigh","year":"2003"},{"key":"2021090612514257100_ref27","first-page":"135","volume-title":"Proceedings of CAV 2008","author":"Bobaru","year":"2008"},{"volume-title":"Proceedings of LICS\u201989","author":"Clarke","first-page":"353","key":"2021090612514257100_ref28"},{"volume-title":"Proceedings of SYNT 2015","author":"Brenguier","first-page":"98","key":"2021090612514257100_ref29"},{"key":"2021090612514257100_ref30","first-page":"251","volume-title":"Proceedings of CAV 2016","author":"Alur","year":"2016"},{"key":"2021090612514257100_ref31","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1515\/jib-2013-216","article-title":"Modular analysis of gene networks by linear temporal logic","volume":"10","author":"Ito","year":"2013","journal-title":"J. Integr. Bioinform."},{"key":"2021090612514257100_ref32","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/j.tcs.2015.06.017","article-title":"Qualitative analysis of gene regulatory networks by temporal logic","volume":"594","author":"Ito","year":"2015","journal-title":"Theoret. Comput. Sci."},{"volume-title":"Proceedings of ACC 2018","author":"Kulkarni","first-page":"2356","key":"2021090612514257100_ref33"},{"key":"2021090612514257100_ref34","first-page":"46","volume-title":"Proceedings of FOCS 1977","author":"Pnueli","year":"1977"},{"key":"2021090612514257100_ref35","first-page":"3","volume-title":"Proceedings of PSTV 1995","author":"Gerth","year":"1995"},{"key":"2021090612514257100_ref36","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Proceedings of Logics for Concurrency","author":"Vardi","year":"1996"},{"volume-title":"Proceedings of SODA 2007","author":"Arthur","first-page":"1027","key":"2021090612514257100_ref37"},{"key":"2021090612514257100_ref38","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1080\/01621459.1963.10500845","article-title":"Hierarchical grouping to optimize an objective function","volume":"58","author":"Ward","year":"1963","journal-title":"J. Am. Stat. Assoc."},{"key":"2021090612514257100_ref39","first-page":"195","volume-title":"Proceedings of ISPSE 2000","author":"Aoshima","year":"2000"},{"key":"2021090612514257100_ref40","first-page":"94","volume-title":"Proceedings of WCTP 2013","author":"Osari","year":"2013"},{"key":"2021090612514257100_ref41","first-page":"61","volume-title":"Proceedings of ICSEA 2019","author":"Kanso","year":"2019"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxab116\/40301065\/bxab116.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxab116\/40301065\/bxab116.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T23:12:18Z","timestamp":1699312338000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/advance-article\/doi\/10.1093\/comjnl\/bxab116\/6363569"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,3]]},"references-count":41,"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxab116","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"type":"print","value":"0010-4620"},{"type":"electronic","value":"1460-2067"}],"subject":[],"published":{"date-parts":[[2021,9,3]]},"article-number":"bxab116"}}