{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:29Z","timestamp":1749318089999},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_6","type":"book-chapter","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T22:59:28Z","timestamp":1448060368000},"page":"79-87","source":"Crossref","is-referenced-by-count":7,"title":["SAT-Based Minimization of Deterministic $$\\omega $$ -Automata"],"prefix":"10.1007","author":[{"given":"Souheib","family":"Baarir","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"6_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, pp. 399\u2013404, July 2009"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-662-43613-4_17","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"S Baarir","year":"2014","unstructured":"Baarir, S., Duret-Lutz, A.: Mechanizing the minimization of deterministic generalized B\u00fcchi automata. In: \u00c1brah\u00e1m, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 266\u2013283. Springer, Heidelberg (2014)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-02444-8_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Babiak","year":"2013","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: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 24\u201339. Springer, Heidelberg (2013)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Heidelberg (2015)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559\u2013575. Springer, Heidelberg (2013)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-02444-8_31","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2013","unstructured":"Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442\u2013445. Springer, Heidelberg (2013)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-14186-7_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Minimising deterministic B\u00fcchi automata precisely using SAT solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 326\u2013332. Springer, Heidelberg (2010)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-76336-9_7","volume-title":"Implementation and Application of Automata","author":"J Klein","year":"2007","unstructured":"Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic \n                    \n                      \n                    \n                    $$\\omega $$\n                  -automata. In: Holub, J., \u017dd\u2019\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51\u201361. Springer, Heidelberg (2007)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-319-11936-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"Z Kom\u00e1rkov\u00e1","year":"2014","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235\u2013241. Springer, Heidelberg (2014)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2012","unstructured":"K\u0159et\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7\u201322. Springer, Heidelberg (2012)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-02444-8_32","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2013","unstructured":"K\u0159et\u00ednsk\u00fd, J., Garza, R.L.: Small deterministic automata for LTL\n                    \n                      \n                    \n                    $$_{\\setminus \\text{ GU }}$$\n                  . In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 446\u2013450. Springer, Heidelberg (2013)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"6_CR13","unstructured":"Minato, S.: Fast generation of irredundant sum-of-products forms from binary decision diagrams. In: SASIMI 1992, pp. 64\u201373, April 1992"},{"key":"6_CR14","unstructured":"Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, The Weizmann Institute of Science, Rehovot, Israel, March 1989"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:24:04Z","timestamp":1559316244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}