{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:07:22Z","timestamp":1750306042253,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T00:00:00Z","timestamp":1499904000000},"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":[[2017,7,13]]},"DOI":"10.1145\/3092282.3092288","type":"proceedings-article","created":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T13:45:49Z","timestamp":1499953549000},"page":"50-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Explicit state model checking with generalized B\u00fcchi and Rabin automata"],"prefix":"10.1145","author":[{"given":"Vincent","family":"Bloemen","sequence":"first","affiliation":[{"name":"University of Twente, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[{"name":"LRDE, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaco van de","family":"Pol","sequence":"additional","affiliation":[{"name":"University of Twente, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","first-page":"486","volume-title":"Proc. of CAV\u201915","author":"Babiak T.","unstructured":"T. Babiak , F. Blahoudek , A. Duret-Lutz , J. Klein , J. K\u0159et\u00ednsk\u00fd , D. M\u00fcller , D. Parker , and J. Strej\u010dek . The Hanoi Omega-Automata Format . In Proc. of CAV\u201915 , vol. 9206 of LNCS , pp. 479\u2013 486 . Springer, 2015. T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. K\u0159et\u00ednsk\u00fd, D. M\u00fcller, D. Parker, and J. Strej\u010dek. The Hanoi Omega-Automata Format. In Proc. of CAV\u201915, vol. 9206 of LNCS, pp. 479\u2013486. Springer, 2015."},{"key":"e_1_3_2_1_2_1","first-page":"39","volume-title":"Proc. of ATVA\u201913","author":"Babiak T.","unstructured":"T. Babiak , F. Blahoudek , M. K\u0159et\u00ednsk\u00fd , and J. Strej\u010dek . Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment . In Proc. of ATVA\u201913 , pp. 24\u2013 39 . Springer, 2013. T. Babiak, F. Blahoudek, M. K\u0159et\u00ednsk\u00fd, and J. Strej\u010dek. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment. In Proc. of ATVA\u201913, pp. 24\u201339. Springer, 2013."},{"key":"e_1_3_2_1_3_1","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen . Principles of Model Checking . The MIT Press , 2008 . SPIN\u201917, July 2017, Santa Barbara, CA, USA Vincent Bloemen, Alexandre Duret-Lutz, and Jaco van de Pol C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008. SPIN\u201917, July 2017, Santa Barbara, CA, USA Vincent Bloemen, Alexandre Duret-Lutz, and Jaco van de Pol"},{"key":"e_1_3_2_1_4_1","first-page":"164","author":"Blahoudek F.","year":"2013","unstructured":"F. Blahoudek , M. K\u0159et\u00ednsk\u00fd , and J. Strej\u010dek . Comparison of LTL to Deterministic Rabin Automata Translators. In Proc. of LPAR-19 , pp. 164 \u2013 172 . Springer, 2013 . F. Blahoudek, M. K\u0159et\u00ednsk\u00fd, and J. Strej\u010dek. Comparison of LTL to Deterministic Rabin Automata Translators. In Proc. of LPAR-19, pp. 164\u2013172. Springer, 2013.","journal-title":"Comparison of LTL to Deterministic Rabin Automata Translators. In Proc. of LPAR-19"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851141.2851161"},{"key":"e_1_3_2_1_6_1","first-page":"33","volume-title":"Multi-core SCC-Based LTL Model Checking. In Proc. of HVC\u201916","author":"Bloemen V.","unstructured":"V. Bloemen and J. van de Pol . Multi-core SCC-Based LTL Model Checking. In Proc. of HVC\u201916 , pp. 18\u2013 33 . Springer, 2016. V. Bloemen and J. van de Pol. Multi-core SCC-Based LTL Model Checking. In Proc. of HVC\u201916, pp. 18\u201333. Springer, 2016."},{"key":"e_1_3_2_1_7_1","first-page":"575","volume-title":"Proc. of CAV\u201913","author":"Chatterjee K.","unstructured":"K. Chatterjee , A. Gaiser , and J. K\u0159et\u00ednsk\u00fd . Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis . In Proc. of CAV\u201913 , pp. 559\u2013 575 . Springer, 2013. K. Chatterjee, A. Gaiser, and J. K\u0159et\u00ednsk\u00fd. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In Proc. of CAV\u201913, pp. 559\u2013575. Springer, 2013."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_15"},{"key":"e_1_3_2_1_9_1","first-page":"30","volume-title":"Selected Writings on Computing: A personal Perspective, Texts and Monographs in Computer Science","author":"Dijkstra E. W.","unstructured":"E. W. Dijkstra . Finding the Maximum Strong Components in a Directed Graph . In Selected Writings on Computing: A personal Perspective, Texts and Monographs in Computer Science , pp. 22\u2013 30 . Springer, 1982. E. W. Dijkstra. Finding the Maximum Strong Components in a Directed Graph. In Selected Writings on Computing: A personal Perspective, Texts and Monographs in Computer Science, pp. 22\u201330. Springer, 1982."},{"key":"e_1_3_2_1_10_1","series-title":"LNCS","first-page":"129","volume-title":"Proc. of ATVA\u201916","author":"Duret-Lutz A.","unstructured":"A. Duret-Lutz , A. Lewkowicz , A. Fauchille , T. Michaud , E. Renault , and L. Xu . Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation . In Proc. of ATVA\u201916 , vol. 9938 of LNCS , pp. 122\u2013 129 . Springer, 2016. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation. In Proc. of ATVA\u201916, vol. 9938 of LNCS, pp. 122\u2013129. Springer, 2016."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_17"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318620"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0259-2"},{"key":"e_1_3_2_1_14_1","series-title":"LNCS","first-page":"283","volume-title":"Proc. of ATVA\u201912","author":"Evangelista S.","unstructured":"S. Evangelista , A. Laarman , L. Petrucci , and J. van de pol. Improved Multi-Core Nested Depth-First Search . In Proc. of ATVA\u201912 , vol. 7561 of LNCS , pp. 269\u2013 283 . Springer, 2012. S. Evangelista, A. Laarman, L. Petrucci, and J. van de pol. Improved Multi-Core Nested Depth-First Search. In Proc. of ATVA\u201912, vol. 7561 of LNCS, pp. 269\u2013283. Springer, 2012."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632375"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.110"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_12"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"e_1_3_2_1_19_1","first-page":"241","volume-title":"Proc. of ATVA\u201914","author":"Kom\u00e1rkov\u00e1 Z.","unstructured":"Z. Kom\u00e1rkov\u00e1 and J. K\u0159et\u00ednsk\u00fd . Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata . In Proc. of ATVA\u201914 , pp. 235\u2013 241 . Springer, 2014. Z. Kom\u00e1rkov\u00e1 and J. K\u0159et\u00ednsk\u00fd. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In Proc. of ATVA\u201914, pp. 235\u2013241. Springer, 2014."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"F. Kordon H. Garavel L. M. Hillah F. Hulin-Hubard A. Linard M. Beccuti A. Hamez E. Lopez-Bobeda L. Jezequel J. Meijer E. Paviot-Adet C. Rodriguez C. Rohr J. Srba Y. Thierry-Mieg and K. Wolf. Complete Results for the 2015 Edition of the Model Checking Contest. http:\/\/mcc.lip6.fr\/2015\/results.php 2015.  F. Kordon H. Garavel L. M. Hillah F. Hulin-Hubard A. Linard M. Beccuti A. Hamez E. Lopez-Bobeda L. Jezequel J. Meijer E. Paviot-Adet C. Rodriguez C. Rohr J. Srba Y. Thierry-Mieg and K. Wolf. Complete Results for the 2015 Edition of the Model Checking Contest. http:\/\/mcc.lip6.fr\/2015\/results.php 2015.","DOI":"10.1007\/978-3-662-53401-4_12"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"511","volume-title":"Proc. of NFM\u201911","author":"Laarman A.","unstructured":"A. Laarman , J. van de Pol , and M. Weber . Multi-Core LTSmin: Marrying Modularity and Scalability . In Proc. of NFM\u201911 , Lecture Notes in Computer Science , pp. 506\u2013 511 . Springer, 2011. A. Laarman, J. van de Pol, and M. Weber. Multi-Core LTSmin: Marrying Modularity and Scalability. In Proc. of NFM\u201911, Lecture Notes in Computer Science, pp. 506\u2013511. Springer, 2011."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_22"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0382-1"},{"key":"e_1_3_2_1_24_1","volume-title":"Master\u2019s thesis","author":"Major J.","year":"2017","unstructured":"J. Major . Translation of LTL into nondeterministic automata with generic acceptance condition. Master\u2019s thesis , Masaryk University , Faculty of Informatics, Brno, 2017 . http:\/\/is.muni.cz\/th\/396325\/fi_m. J. Major. Translation of LTL into nondeterministic automata with generic acceptance condition. Master\u2019s thesis, Masaryk University, Faculty of Informatics, Brno, 2017. http:\/\/is.muni.cz\/th\/396325\/fi_m."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41857"},{"key":"e_1_3_2_1_26_1","first-page":"1","author":"Renault E.","year":"2016","unstructured":"E. Renault , A. Duret-Lutz , F. Kordon , and D. Poitrenaud . Variations on parallel explicit emptiness checks for generalized B\u00fcchi automata. International Journal on Software Tools for Technology Transfer , pp. 1 \u2013 21 , 2016 . E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Variations on parallel explicit emptiness checks for generalized B\u00fcchi automata. International Journal on Software Tools for Technology Transfer, pp. 1\u201321, 2016.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"e_1_3_2_1_28_1","first-page":"331","volume-title":"Proc. of LICS\u201986","author":"Vardi M. Y.","unstructured":"M. Y. Vardi and P. Wolper . An automata-theoretic approach to automatic program verification . In Proc. of LICS\u201986 , pp. 322\u2013 331 . IEEE Computer Society, 1986. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. of LICS\u201986, pp. 322\u2013331. IEEE Computer Society, 1986."},{"key":"e_1_3_2_1_29_1","first-page":"493","volume-title":"Proc. of CAV\u201916","author":"Wijs A.","unstructured":"A. Wijs . BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs . In Proc. of CAV\u201916 , pp. 472\u2013 493 . Springer, 2016. A. Wijs. BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs. In Proc. of CAV\u201916, pp. 472\u2013493. Springer, 2016."}],"event":{"name":"ISSTA '17: International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Santa Barbara CA USA","acronym":"ISSTA '17"},"container-title":["Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3092288","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092282.3092288","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:08Z","timestamp":1750215788000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3092288"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,13]]},"references-count":29,"alternative-id":["10.1145\/3092282.3092288","10.1145\/3092282"],"URL":"https:\/\/doi.org\/10.1145\/3092282.3092288","relation":{},"subject":[],"published":{"date-parts":[[2017,7,13]]},"assertion":[{"value":"2017-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}