{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:32Z","timestamp":1740107972293,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T00:00:00Z","timestamp":1551052800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001834","name":"University of Twente","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001834","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10009-019-00508-4","type":"journal-article","created":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T03:17:48Z","timestamp":1551064668000},"page":"307-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Model checking with generalized Rabin and Fin-less automata"],"prefix":"10.1007","volume":"21","author":[{"given":"Vincent","family":"Bloemen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,25]]},"reference":[{"key":"508_CR1","doi-asserted-by":"crossref","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, A. K\u0159et\u00ednsk\u00fd, J. M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Proceedings of CAV\u201915, vol. 9206 of LNCS, pp. 479\u2013486. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"508_CR2","doi-asserted-by":"crossref","unstructured":"Babiak, T., Blahoudek, F., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Effective translation of LTL to deterministic Rabin automata: beyond the (F,G)-fragment. In: Proceedings of ATVA\u201913, pp. 24\u201339. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_4"},{"key":"508_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"508_CR4","doi-asserted-by":"crossref","unstructured":"Ben\u00a0Salem, A., Duret-Lutz, A., Kordon, F., Thierry-Mieg, Y.: Symbolic model checking of stutter-invariant properties using generalized testing automata. In: Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, vol. 8413 of LNCS, pp. 440\u2013454. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_38"},{"key":"508_CR5","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Comparison of LTL to deterministic Rabin automata translators. In: Proceedings of LPAR-19, pp. 164\u2013172. Springer (2013)","DOI":"10.1007\/978-3-642-45221-5_12"},{"key":"508_CR6","doi-asserted-by":"crossref","unstructured":"Bloemen, V., Duret-Lutz, A., van\u00a0de Pol, J.: Explicit state model checking with generalized B\u00fcchi and Rabin automata. In: Proceedings of SPIN\u201917, pp. 50\u201359. ACM (2017)","DOI":"10.1145\/3092282.3092288"},{"key":"508_CR7","doi-asserted-by":"crossref","unstructured":"Bloemen, V., Laarman, A., van\u00a0de Pol, J.: Multi-core on-the-fly SCC decomposition. In: Proceedings of PPoPP\u201916, pp. 8:1\u20138:12. ACM (2016)","DOI":"10.1145\/3016078.2851161"},{"key":"508_CR8","doi-asserted-by":"crossref","unstructured":"Bloemen, V., van\u00a0de Pol, J.: Multi-core SCC-based LTL model checking. In: Proceedings of HVC\u201916, pp. 18\u201333. Springer (2016)","DOI":"10.1007\/978-3-319-49052-6_2"},{"key":"508_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Proceedings of CAV\u201913, pp. 559\u2013575. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"508_CR10","doi-asserted-by":"crossref","unstructured":"Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Proceedings of SPIN\u201905, vol. 3639 of LNCS, pp. 143\u2013158. Springer (2005)","DOI":"10.1007\/11537328_15"},{"key":"508_CR11","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: 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)","DOI":"10.1007\/978-1-4612-5695-3_3"},{"key":"508_CR12","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and \n                    \n                      \n                    \n                    $$\\omega $$\n                    \n                      \n                        \u03c9\n                      \n                    \n                  -automata manipulation. In: Proceedings of ATVA\u201916, vol. 9938 of LNCS, pp. 122\u2013129. Springer (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"508_CR13","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D., Couvreur, J.-M.: On-the-fly emptiness check of transition-based Streett automata. In: Proceedings of ATVA\u201909, vol. 5799 of LNCS, pp. 213\u2013227. Springer (2009)","DOI":"10.1007\/978-3-642-04761-9_17"},{"key":"508_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking (extended abstract): branching time strikes back. In: Proceedings of POPL\u201985, pp. 84\u201396. ACM (1985)","DOI":"10.1145\/318593.318620"},{"issue":"3","key":"508_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata. Form. Methods Syst. Des. 49(3), 1\u201353 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"508_CR16","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Laarman, A., Petrucci, L., van\u00a0de pol, J.: Improved multi-core nested depth-first Search. In: Proceedings of ATVA\u201912, vol. 7561 of LNCS, pp. 269\u2013283. Springer (2012)","DOI":"10.1007\/978-3-642-33386-6_22"},{"key":"508_CR17","doi-asserted-by":"crossref","unstructured":"Farag\u00f3, D., Schmitt, P.H.: Improving non-progress cycle checks. In: Proceedings of the 16th International SPIN Workshop, pp. 50\u201367. Springer (2009)","DOI":"10.1007\/978-3-642-02652-2_8"},{"key":"508_CR18","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Holzmann, G.J.: An improvement of the Piggyback algorithm for parallel model checking. In: Proceedings of SPIN\u201914, pp. 48\u201357. ACM (2014)","DOI":"10.1145\/2632362.2632375"},{"issue":"6","key":"508_CR19","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"508_CR20","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Parallelizing the spin model checker. In: Proceedings of SPIN\u201912, vol. 7385 of LNCS, pp. 155\u2013171. Springer (2012)","DOI":"10.1007\/978-3-642-31759-0_12"},{"key":"508_CR21","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Proceedings of TACAS\u201915, vol. 9035 of LNCS, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"508_CR22","doi-asserted-by":"crossref","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: Safraless translation of LTL to small deterministic automata. In: Proceedings of ATVA\u201914, pp. 235\u2013241. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_17"},{"key":"508_CR23","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Hamez, A., Lopez-Bobeda, E., Jezequel, L., Meijer, J., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Wolf, K.: Complete Results for the 2015 Edition of the Model Checking Contest (2015). \n                    http:\/\/mcc.lip6.fr\/2015\/results.php"},{"key":"508_CR24","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Proceedings of CAV\u201918, July 2018. (to appear)","DOI":"10.1007\/978-3-319-96145-3_30"},{"key":"508_CR25","doi-asserted-by":"crossref","unstructured":"Laarman, A., Farag\u00f3, D.: Improved on-the-fly livelock detection. In: Proceedings of the 5th NASA Formal Methods symposium, pp. 32\u201347. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_3"},{"key":"508_CR26","doi-asserted-by":"crossref","unstructured":"Laarman, A., van\u00a0de Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Proceedings of NFM\u201911, Lecture Notes in Computer Science, pp. 506\u2013511. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_40"},{"key":"508_CR27","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.: Scalable multi-core model checking fairness enhanced systems. In: Proceedings of ICFEM\u201909, vol. 5885 of LNCS, pp. 426\u2013445. Springer (2009)","DOI":"10.1007\/978-3-642-10373-5_22"},{"key":"508_CR28","first-page":"1","volume":"18","author":"G Lowe","year":"2015","unstructured":"Lowe, G.: Concurrent depth-first search algorithms based on Tarjan\u2019s algorithm. Int. J. Softw. Tools Technol. Transf. 18, 1\u201319 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"508_CR29","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of PODC\u201987, pp. 205\u2013205. ACM (1987)","DOI":"10.1145\/41840.41857"},{"key":"508_CR30","doi-asserted-by":"crossref","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic Emerson\u2013Lei automata. In: Proceedings of GandALF\u201917, vol. 256 of EPTCS, pp. 180\u2013194, Sept. 2017","DOI":"10.4204\/EPTCS.256.13"},{"key":"508_CR31","first-page":"263","volume-title":"BEEM: Benchmarks for Explicit Model Checkers","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for Explicit Model Checkers, pp. 263\u2013267. Springer, Berlin (2007)"},{"key":"508_CR32","first-page":"1","volume":"19","author":"E Renault","year":"2016","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Variations on parallel explicit emptiness checks for generalized B\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 19, 1\u201321 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"508_CR33","doi-asserted-by":"crossref","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Proceedings of TLTL3HOoACAS\u201905, vol. 3440 of LNCS, pp. 174\u2013190. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"508_CR34","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS\u201986, pp. 322\u2013331. IEEE Computer Society (1986)"},{"key":"508_CR35","doi-asserted-by":"crossref","unstructured":"Wijs, A.: BFS-based model checking of linear-time properties with an application on GPUs. In: Proceedings of CAV\u201916, pp. 472\u2013493. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_26"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00508-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00508-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00508-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,24]],"date-time":"2020-02-24T19:12:58Z","timestamp":1582571578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00508-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,25]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["508"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00508-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2019,2,25]]},"assertion":[{"value":"25 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}