{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:20Z","timestamp":1772163980665,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429079","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"63-74","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Advanced automata minimization"],"prefix":"10.1145","author":[{"given":"Richard","family":"Mayr","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"given":"Lorenzo","family":"Clemente","sequence":"additional","affiliation":[{"name":"LaBRI, University of Bordeaux I, Bordeaux, France"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"RABIT tool: www.languageinclusion.org\/doku.php?id=tools.  RABIT tool: www.languageinclusion.org\/doku.php?id=tools."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_14"},{"key":"e_1_3_2_1_4_1","first-page":"187","volume-title":"International Conference on Concurrency Theory","volume":"6901","author":"Abdulla P.","year":"2011","unstructured":"P. Abdulla , Y.-F. Chen , L. Clemente , L. Holik , C.-D. Hong , R. Mayr , and T. Vojnar . Advanced Ramsey-based Buchi Automata Inclusion Testing. In J.-P. Katoen and B. Konig, editors , International Conference on Concurrency Theory , volume 6901 of LNCS, pages 187 -- 202 , Sept. 2011 . P. Abdulla, Y.-F. Chen, L. Clemente, L. Holik, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Buchi Automata Inclusion Testing. In J.-P. Katoen and B. Konig, editors, International Conference on Concurrency Theory, volume 6901 of LNCS, pages 187--202, Sept. 2011."},{"key":"e_1_3_2_1_5_1","series-title":"LIPIcs","first-page":"1","volume-title":"FSTTCS","author":"Abdulla P. A.","year":"2009","unstructured":"P. A. Abdulla , Y.-F. Chen , L. Hol1k, and T. Vojnar . Mediating for reduction (on minimizing alternating Buchi automata) . In FSTTCS , volume 4 of LIPIcs , pages 1 -- 12 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2009 . P. A. Abdulla, Y.-F. Chen, L. Hol1k, and T. Vojnar. Mediating for reduction (on minimizing alternating Buchi automata). In FSTTCS, volume 4 of LIPIcs, pages 1--12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635502"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"L.\n      Clemente\n    .\n  Buchi Automata Can Have Smaller Quotients\n  . In L. Aceto M. Henzinger and J. Sgall editors ICALP volume \n  6756\n   of \n  LNCS pages \n  258\n  --\n  270\n  . \n  2011\n  . ISBN 978-3-642-22011-1. doi: 10.1007\/978-3-642-22012-8 20. \n  URL\n   http:\/\/arxiv.org\/pdf\/1102.3285.     10.1007\/978-3-642-22012-8\nL. Clemente. Buchi Automata Can Have Smaller Quotients. In L. Aceto M. Henzinger and J. Sgall editors ICALP volume 6756 of LNCS pages 258--270. 2011. ISBN 978-3-642-22011-1. doi: 10.1007\/978-3-642-22012-8 20. URL http:\/\/arxiv.org\/pdf\/1102.3285.","DOI":"10.1007\/978-3-642-22012-8"},{"key":"e_1_3_2_1_10_1","series-title":"LNCS","volume-title":"Computer Aided Verification","author":"Dill D. L.","year":"1991","unstructured":"D. L. Dill , A. J. Hu , and H. Wont-Toi . Checking for Language Inclusion Using Simulation Preorders . In Computer Aided Verification , volume 575 of LNCS . Springer-Verlag , 1991 . doi: 10.1007\/3-540-55179-4 25. URL http:\/\/dx.doi.org\/10.1007\/3-540-55179-4 25. 10.1007\/3-540-55179-4 D. L. Dill, A. J. Hu, and H. Wont-Toi. Checking for Language Inclusion Using Simulation Preorders. In Computer Aided Verification, volume 575 of LNCS. Springer-Verlag, 1991. doi: 10.1007\/3-540-55179-4 25. URL http:\/\/dx.doi.org\/10.1007\/3-540-55179-4 25."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"e_1_3_2_1_12_1","first-page":"131","volume-title":"International Conference on Concurrency Theory","volume":"2421","author":"Etessami K.","year":"2002","unstructured":"K. Etessami . A Hierarchy of Polynomial-Time Computable Simulations for Automata . In International Conference on Concurrency Theory , volume 2421 of LNCS, pages 131 -- 144 . Springer-Verlag , 2002 . doi: 10.1007\/3-540-45694-5 10. URL http:\/\/dx.doi.org\/10.1007\/3-540-45694-5 10. 10.1007\/3-540-45694-5 K. Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In International Conference on Concurrency Theory, volume 2421 of LNCS, pages 131--144. Springer-Verlag, 2002. doi: 10.1007\/3-540-45694-5 10. URL http:\/\/dx.doi.org\/10.1007\/3-540-45694-5 10."},{"key":"e_1_3_2_1_13_1","first-page":"153","volume-title":"Optimizing Buchi Automata. In International Conference on Concurrency Theory","volume":"1877","author":"Etessami K.","year":"2000","unstructured":"K. Etessami and G. Holzmann . Optimizing Buchi Automata. In International Conference on Concurrency Theory , volume 1877 of LNCS, pages 153 -- 168 . Springer-Verlag , 2000 . K. Etessami and G. Holzmann. Optimizing Buchi Automata. In International Conference on Concurrency Theory, volume 1877 of LNCS, pages 153--168. Springer-Verlag, 2000."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703420675"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_17"},{"key":"e_1_3_2_1_17_1","series-title":"LIPIcs","first-page":"248","volume-title":"Computer Science Logic","author":"Fogarty S.","year":"2011","unstructured":"S. Fogarty , O. Kupferman , M. Y. Vardi , and T. Wilke . Unifying Buchi Complementation Constructions . In M. Bezem, editor, Computer Science Logic , volume 12 of LIPIcs , pages 248 -- 263 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik , 2011 . doi: http:\/\/dx.doi.org\/10.4230\/LIPIcs.CSL.2011.248. 10.4230\/LIPIcs.CSL.2011.248 S. Fogarty, O. Kupferman, M. Y. Vardi, and T. Wilke. Unifying Buchi Complementation Constructions. In M. Bezem, editor, Computer Science Logic, volume 12 of LIPIcs, pages 248--263. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011. doi: http:\/\/dx.doi.org\/10.4230\/LIPIcs.CSL.2011.248."},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"53","volume-title":"CAV","author":"Gastin P.","year":"2001","unstructured":"P. Gastin and D. Oddoux . Fast LTL to Buchi automata translation . In CAV , volume 2102 of LNCS , pages 53 -- 65 . Springer , 2001 . P. Gastin and D. Oddoux. Fast LTL to Buchi automata translation. In CAV, volume 2102 of LNCS, pages 53--65. Springer, 2001."},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","first-page":"610","volume-title":"CAV","author":"Gurumurthy S.","year":"2002","unstructured":"S. Gurumurthy , R. Bloem , , and F. Somenzi . Fair simulation minimization . In CAV , volume 2404 of LNCS , pages 610 -- 624 . Springer , 2002 . S. Gurumurthy, R. Bloem, , and F. Somenzi. Fair simulation minimization. In CAV, volume 2404 of LNCS, pages 610--624. Springer, 2002."},{"key":"e_1_3_2_1_20_1","volume-title":"FOCS '95","author":"Henzinger M. R.","year":"1995","unstructured":"M. R. Henzinger , T. A. Henzinger , and P. W. Kopke . Computing simulations on finite and infinite graphs. In Foundations of Computer Science , FOCS '95 , Washington, DC, USA , 1995 . IEEE Computer Society. ISBN 0-8186-7183-1. URL http:\/\/portal.acm.org\/citation.cfm?id=796255. M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In Foundations of Computer Science, FOCS '95, Washington, DC, USA, 1995. IEEE Computer Society. ISBN 0-8186-7183-1. URL http:\/\/portal.acm.org\/citation.cfm?id=796255."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3085"},{"key":"e_1_3_2_1_22_1","volume-title":"The SPIN Model Checker","author":"Holzmann G.","year":"2004","unstructured":"G. Holzmann . The SPIN Model Checker . Addison Wesley , 2004 . G. Holzmann. The SPIN Model Checker. Addison Wesley, 2004."},{"key":"e_1_3_2_1_23_1","first-page":"629","volume":"510","author":"Jiang T.","year":"1991","unstructured":"T. Jiang and B. Ravikumar . Minimal NFA Problems are Hard. In J. Albert, B. Monien, and M. Artalejo, editors, ICALP , volume 510 of LNCS, pages 629 -- 640 . 1991 . doi: 10.1007\/3-540-54233-7 169. 10.1007\/3-540-54233-7 T. Jiang and B. Ravikumar. Minimal NFA Problems are Hard. In J. Albert, B. Monien, and M. Artalejo, editors, ICALP, volume 510 of LNCS, pages 629--640. 1991. doi: 10.1007\/3-540-54233-7 169.","journal-title":"Minimal NFA Problems are Hard. In J. Albert, B. Monien, and M. Artalejo, editors, ICALP"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_7"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735839"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_18"},{"key":"e_1_3_2_1_28_1","volume-title":"Mathematics of Choice","author":"Niven I.","year":"1965","unstructured":"I. Niven . Mathematics of Choice . The Mathematical Association of America , 1965 . I. Niven. Mathematics of Choice. The Mathematical Association of America, 1965."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.28"},{"key":"e_1_3_2_1_30_1","series-title":"LNCS","volume-title":"Correct Hardware Design and Verification Methods","author":"Sebastiani R.","year":"2003","unstructured":"R. Sebastiani and S. Tonetta . More deterministic vs. smaller Buchi automata for efficient LTL model checking . In Correct Hardware Design and Verification Methods , volume 2860 of LNCS , 2003 . R. Sebastiani and S. Tonetta. More deterministic vs. smaller Buchi automata for efficient LTL model checking. In Correct Hardware Design and Verification Methods, volume 2860 of LNCS, 2003."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734097"},{"key":"e_1_3_2_1_33_1","volume-title":"LATA","author":"Tabakov D.","year":"2007","unstructured":"D. Tabakov and M. Vardi . Model Checking Buchi Specifications . In LATA , volume Report 35\/07 . Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Tarragona, 2007 . D. Tabakov and M. Vardi. Model Checking Buchi Specifications. In LATA, volume Report 35\/07. Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Tarragona, 2007."},{"key":"e_1_3_2_1_34_1","series-title":"LNCS","first-page":"346","volume-title":"Tools and Algo- rithms for the Construction and Analysis of Systems","author":"Tsay Y.-K.","year":"2008","unstructured":"Y.-K. Tsay , Y.-F. Chen , M.-H. Tsai , W.-C. Chan , and C.-J. Luo . GOAL extended: Towards a research tool for omega automata and temporal logic . In C. Ramakrishnan and J. Rehof, editors, Tools and Algo- rithms for the Construction and Analysis of Systems , volume 4963 of LNCS , pages 346 -- 350 . 2008 . ISBN 978-3-540-78799-0. URL http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3 26. 10.1007\/978-3-540-78800-3 Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai,W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega automata and temporal logic. In C. Ramakrishnan and J. Rehof, editors, Tools and Algo- rithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 346--350. 2008. ISBN 978-3-540-78799-0. URL http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3 26."},{"key":"e_1_3_2_1_35_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-642-19835-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Tsay Y.-K.","year":"2011","unstructured":"Y.-K. Tsay , M.-H. Tsai , J.-S. Chang , and Y.-W. Chang . Buchi store: An open repository of Buchi automata . In P. Abdulla and K. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 6605 of LNCS , pages 262 -- 266 . 2011 . ISBN 978-3-642-19834-2. URL http:\/\/dx.doi.org\/10.1007\/978-3-642-19835-9 23.10.1007\/978-3-642-19835-9 23. 10.1007\/978-3-642-19835-9 Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. Buchi store: An open repository of Buchi automata. In P. Abdulla and K. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of LNCS, pages 262--266. 2011. ISBN 978-3-642-19834-2. URL http:\/\/dx.doi.org\/10.1007\/978-3-642-19835-9 23.10.1007\/978-3-642-19835-9 23."}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429079","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":33,"alternative-id":["10.1145\/2429069.2429079","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429079","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429079","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}