{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T02:30:58Z","timestamp":1719801058300},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T00:00:00Z","timestamp":1422403200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"PiCoq","award":["ANR-10-BLAN-0305"]},{"name":"PACE","award":["ANR-12IS02001"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2015,1,28]]},"abstract":"\n We introduce\n bisimulation up to congruence<\/jats:italic>\n as a technique for proving language equivalence of nondeterministic finite automata. Exploiting this technique, we devise an optimization of the classic algorithm by Hopcroft and Karp. We compare our approach to the recently introduced antichain algorithms and we give concrete examples where we exponentially improve over antichains. Experimental results show significant improvements.\n <\/jats:p>","DOI":"10.1145\/2713167","type":"journal-article","created":{"date-parts":[[2015,2,3]],"date-time":"2015-02-03T13:39:49Z","timestamp":1422970789000},"page":"87-95","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Hacking nondeterminism with induction and coinduction"],"prefix":"10.1145","volume":"58","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lyon, France"}]},{"given":"Damien","family":"Pous","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lyon, France"}]}],"member":"320","published-online":{"date-parts":[[2015,1,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646820.706585"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003900"},{"key":"e_1_2_1_4_1","unstructured":"Bonchi F. and Pous D. Extended version of this abstract with omitted proofs and web appendix for this work. http:\/\/hal.inria.fr\/hal-00639716\/ and http:\/\/perso.ens-lyon.fr\/damien.pous\/hknt 2012. Bonchi F. and Pous D. Extended version of this abstract with omitted proofs and web appendix for this work. http:\/\/hal.inria.fr\/hal-00639716\/ and http:\/\/perso.ens-lyon.fr\/damien.pous\/hknt 2012."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Bouajjani A. Habermehl P. and \n \n \n Vojnar T\n \n \n . \n Abstract regular model checking\n . In CAV R. Alur and D. Peled eds. Volume \n 3114\n of \n Lecture Notes in Computer Science (2004)\n . \n Springer\n . Bouajjani A. Habermehl P. and Vojnar T. Abstract regular model checking. In CAV R. Alur and D. Peled eds. Volume 3114 of Lecture Notes in Computer Science (2004). Springer.","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"e_1_2_1_6_1","first-page":"339","article-title":"Graphes canoniques de graphes alg\u00e9briques","volume":"24","author":"Caucal D","year":"1990","journal-title":"ITA"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121127"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/795662.796255"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00064-X"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"e_1_2_1_15_1","first-page":"2","article-title":"From set-theoretic coinduction to coalgebraic coinduction: Some results, some problems","volume":"19","author":"Lenisa M","year":"1999","journal-title":"ENTCS"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/800125.804029"},{"key":"e_1_2_1_17_1","volume-title":"Prentice Hall","author":"Milner R.","year":"1989"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Pous D.\n \n \n \n Complete lattices and up-to techniques\n . In APLAS Z. Shao ed. Volume \n 4807\n of \n Lecture Notes in Computer Science (2007)\n . \n Springer 351--366. Pous D. Complete lattices and up-to techniques. In APLAS Z. Shao ed. Volume 4807 of Lecture Notes in Computer Science (2007). Springer 351--366.","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Rutten J.\n \n \n \n Automata and coinduction (an exercise in coalgebra)\n . In CONCUR D. Sangiorgi and R. de Simone eds. Volume \n 1466\n of \n Lecture Notes in Computer Science (1998)\n . \n Springer 194--218. Rutten J. Automata and coinduction (an exercise in coalgebra). In CONCUR D. Sangiorgi and R. de Simone eds. Volume 1466 of Lecture Notes in Computer Science (1998). Springer 194--218.","DOI":"10.1007\/BFb0055624"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2103603"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_28"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_5"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2713167","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T18:38:06Z","timestamp":1672425486000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2713167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,28]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,1,28]]}},"alternative-id":["10.1145\/2713167"],"URL":"https:\/\/doi.org\/10.1145\/2713167","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,28]]},"assertion":[{"value":"2015-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}