{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:25:13Z","timestamp":1753885513341,"version":"3.41.2"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"abstract":"<jats:p>\n            We investigate the problem of computing the reachable blocks of the simulation equivalence and its natural counterpart for the simulation preorder, referred to as the\n            <jats:italic>reachable simulation problem<\/jats:italic>\n            . Through a theoretical investigation of this problem, we unveil a sharp contrast with the already settled case of bisimulation equivalence. Then, we design algorithms to solve the reachable simulation problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. Specifically, we propose algorithms achieving different guarantees on the precision of the output, and a symbolic algorithm that operates on state partitions and relations between their blocks, which is particularly well-suited for processing infinite-state systems.\n          <\/jats:p>","DOI":"10.1145\/3723172","type":"journal-article","created":{"date-parts":[[2025,3,17]],"date-time":"2025-03-17T12:18:41Z","timestamp":1742213921000},"update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Reachable Simulation Problem"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3625-6003","authenticated-orcid":false,"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[{"name":"IMDEA Software Insititute, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7561-3763","authenticated-orcid":false,"given":"Nicolas","family":"Manini","sequence":"additional","affiliation":[{"name":"IMDEA Software Insititute, Spain and Universidad Polit\u00e9cnica de Madrid, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0159-0068","authenticated-orcid":false,"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Padova, Italy"}]}],"member":"320","published-online":{"date-parts":[[2025,3,17]]},"reference":[{"unstructured":"Rajeev Alur and Thomas\u00a0A. Henzinger. 1999. Computer-Aided Verification. (1999). Chapter 4: Graph Minimization. (Unpublished manuscript).","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/3-540-56496-9_21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1016\/0167-6423(95)00003-B"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/BFb0023733"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1016\/0167-6423(92)90018-7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/635499.635502"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1109\/LICS.2017.8005069"},{"key":"e_1_2_1_8_1","volume-title":"Handbook of Model Checking","author":"Clarke M.","unstructured":"Edmund\u00a0M. Clarke, Thomas\u00a0A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking (1st ed.). Springer.","edition":"1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.3233\/FI-2011-412"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1023\/A:1016091902809"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-031-72621-7_3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1023\/A:1027328830731"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-540-70545-1_49"},{"volume-title":"Lattice theory: foundation","author":"Gratzer A","unstructured":"George\u00a0A Gratzer. 2011. Lattice theory: foundation. Springer.","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/3060140"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/3-540-54430-5_93"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/177492.177725"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1145\/1181775.1181790"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1109\/SFCS.1995.492576"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/1042038.1042039"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.2168\/LMCS-12(1:6)2016"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1007\/978-3-030-45237-7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1017\/S1471068406002651"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1006\/inco.2001.3122"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/3-540-45694-5_39"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/129712.129738"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/BF01384313"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/3365365.3382219"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.5555\/1095587"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1137\/0216062"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1007\/11513988_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1007\/978-3-642-40313-2_66"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1007\/s00236-014-0195-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1109\/LICS.2007.8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1016\/j.ic.2009.06.002"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/3-540-45319-9_33"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1007\/978-3-540-70844-5_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1023\/A:1008621829508"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3723172","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,17]],"date-time":"2025-03-17T12:18:44Z","timestamp":1742213924000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3723172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,17]]},"references-count":38,"alternative-id":["10.1145\/3723172"],"URL":"https:\/\/doi.org\/10.1145\/3723172","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2025,3,17]]},"assertion":[{"value":"2024-10-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3723172"}}