{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T07:24:07Z","timestamp":1763018647189,"version":"3.41.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2023,9,30]],"date-time":"2023-09-30T00:00:00Z","timestamp":1696032000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS KAKENHI","award":["JP19H04082"],"award-info":[{"award-number":["JP19H04082"]}]},{"name":"MICIN","award":["PID2019-108528RB-C22"],"award-info":[{"award-number":["PID2019-108528RB-C22"]}]},{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"crossref","award":["S2018\/TCS-4339"],"award-info":[{"award-number":["S2018\/TCS-4339"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2023,11,30]]},"abstract":"<jats:p>\n            We devised the\n            <jats:italic>L<\/jats:italic>\n            +1-layer divide &amp; conquer approach to leads-to model checking (\n            <jats:italic>L<\/jats:italic>\n            +1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for\n            <jats:italic>L<\/jats:italic>\n            +1-DCA2L2MC. In a temporal logic called\n            <jats:italic>UNITY<\/jats:italic>\n            , designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to these properties. Counterexample generation is one of the main tasks in the\n            <jats:italic>L<\/jats:italic>\n            +1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the\n            <jats:italic>L<\/jats:italic>\n            +1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.\n          <\/jats:p>","DOI":"10.1145\/3604610","type":"journal-article","created":{"date-parts":[[2023,6,17]],"date-time":"2023-06-17T09:14:56Z","timestamp":1686993296000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way"],"prefix":"10.1145","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh Minh","family":"Do","sequence":"first","affiliation":[{"name":"Japan Advanced Institute of Science and Technology"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8388-0004","authenticated-orcid":false,"given":"Yati","family":"Phyo","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-4612","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Riesco","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology"}]}],"member":"320","published-online":{"date-parts":[[2023,9,30]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/71.80120"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2398877"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_11"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_5"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63516-3_12"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3652"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_2"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/59087"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/BDCloud.2018.00018"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80051-6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028741"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_16"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00576-x"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3382734.3405739"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/363958.364002"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSSR53171.2021.00011"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_29_2","unstructured":"Steven Eker Jos\u00e9 Meseguer and Ambarish Sridharanarayanan. 2002. The Maude LTL model checker. In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications (WRLA\u201902) ."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_22"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00051-X"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_18"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19242-5_22"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441608"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368094"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-415950-1.00017-3"},{"key":"e_1_3_2_39_2","first-page":"23","article-title":"On nested depth first search","author":"Holzmann Gerard","year":"1999","unstructured":"Gerard Holzmann, Doron Peled, and Mihalis Yannakakis. 1999. On nested depth first search. In The Spin Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 32. American Mathematical Society, Providence, RI, 23\u201332.","journal-title":"The Spin Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 32. American Mathematical Society, Providence, RI"},{"key":"e_1_3_2_40_2","volume-title":"The SPIN Model Checker\u2014Primer and Reference Manual","author":"Holzmann Gerald J.","year":"2004","unstructured":"Gerald J. Holzmann. 2004. The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_12"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70724"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.110"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374529"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2016.08.001"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxu127"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062526"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_23"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48234-2_3"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1807167.1807184"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.040"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2012.04.026"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"Pel\u00e1nek Radek","year":"2007","unstructured":"Radek Pel\u00e1nek. 2007. BEEM: Benchmarks for explicit model checkers. In Model Checking Software, Dragan Bo\u0161na\u010dki and Stefan Edelkamp (Eds.). Springer, Berlin, Germany, 263\u2013267."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxaa183"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC51774.2021.00118"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(81)90008-0"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_26"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.07.007"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194021400210"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2014.07.009"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3604610","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3604610","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:03Z","timestamp":1750178763000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3604610"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,30]]},"references-count":66,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,11,30]]}},"alternative-id":["10.1145\/3604610"],"URL":"https:\/\/doi.org\/10.1145\/3604610","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2023,9,30]]},"assertion":[{"value":"2022-11-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-28","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}