{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:44Z","timestamp":1749318104887,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030890506"},{"type":"electronic","value":"9783030890513"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-89051-3_14","type":"book-chapter","created":{"date-parts":[[2021,10,12]],"date-time":"2021-10-12T09:30:38Z","timestamp":1634031038000},"page":"243-264","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Simplifying Alternating Automata for\u00a0Emptiness Testing"],"prefix":"10.1007","author":[{"given":"Pavol","family":"Vargov\u010d\u00edk","sequence":"first","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,12]]},"reference":[{"key":"14_CR1","unstructured":"RegexLib. http:\/\/www.regexlib.com\/, http:\/\/www.regexlib.com\/"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: Efficient handling of string-number conversion. In: PLDI 2020, pp. 943\u2013957. ACM (2020)","DOI":"10.1145\/3385412.3386034"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: CONCUR 2002. LNCS, vol. 2421, pp. 116\u2013130. Springer (2002)","DOI":"10.1007\/3-540-45694-5_9"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45619-8_1","volume-title":"Logic Programming","author":"B Boigelot","year":"2002","unstructured":"Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: an overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1\u201320. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45619-8_1"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45619-8_1","volume-title":"Logic Programming","author":"B Boigelot","year":"2002","unstructured":"Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: an overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1\u201320. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45619-8_1"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_31"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD 2007, pp. 173\u2013180. IEEE Computer Society (2007)","DOI":"10.1109\/FMCAD.2007.4401997"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"14_CR9","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Proceedings of the Symposium of Mathematical Theory of Automata, pp. 529\u2013561 (1962)"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"14_CR11","unstructured":"Cox, A.: Model checking regular expressions. In: Presented at MOSCA 2019 (2019). https:\/\/mosca19.github.io\/slides\/cox.pdf"},{"key":"14_CR12","unstructured":"Cox, A., Leasure, J.: Model checking regular language constraints. CoRR abs\/1708.09073 (2017)"},{"key":"14_CR13","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. CoRR abs\/1610.01722 (2016)"},{"key":"14_CR14","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI 2013, pp. 854\u2013860. ACM (2013)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-78800-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M De Wulf","year":"2008","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63\u201377. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_6"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-662-54577-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Fiedor","year":"2017","unstructured":"Fiedor, T., Hol\u00edk, L., Jank\u016f, P., Leng\u00e1l, O., Vojnar, T.: Lazy automata techniques for WS1S. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 407\u2013425. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_24"},{"issue":"2","key":"14_CR17","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods Syst. Des. 24(2), 101\u2013127 (2004)","journal-title":"Formal Methods Syst. Des."},{"issue":"38\u201339","key":"14_CR18","doi-asserted-by":"publisher","first-page":"3444","DOI":"10.1016\/j.tcs.2010.05.037","volume":"411","author":"P Ganty","year":"2010","unstructured":"Ganty, P., Maquet, N., Raskin, J.: Fixed point guided abstraction refinement for alternating automata. Theor. Comput. Sci. 411(38\u201339), 3444\u20133459 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR19","unstructured":"Harding, A.: Symbolic strategy synthesis for games with LTL winning conditions. Ph.D. thesis, University of Birmingham (2005)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: FMCAD 2013, pp. 157\u2013164. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Janku, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the ACM Programming Language, vol. 2 (POPL) (2018)","DOI":"10.1145\/3158092"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Hurst, A.P., Mishchenko, A., Brayton, R.K.: Fast minimum-register retiming via binary maximum-flow. In: FMCAD 2007, pp. 181\u2013187 (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.31","DOI":"10.1109\/FAMCAD.2007.31"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-89963-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Iosif","year":"2018","unstructured":"Iosif, R., Xu, X.: Abstraction refinement for emptiness checking of alternating data automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 93\u2013111. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_6"},{"issue":"3","key":"14_CR25","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"3","key":"14_CR26","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/S0304-3975(81)80005-9","volume":"13","author":"E Leiss","year":"1981","unstructured":"Leiss, E.: Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci. 13(3), 323\u2013330 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting a fresh look at combinational logic synthesis. In: 2006 43rd ACM\/IEEE Design Automation Conference (DAC 2006), pp. 532\u2013535. ACM (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"14_CR29","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: Integrating logic synthesis, technology mapping, and retiming. In: Proceedings ot the IWLS 2005. Tech. rep., (2006)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Een, N., Brayton, R., Baumgartner, J., Mony, H., Nalla, P.: Gla: gate-level abstraction revisited. In: DATE 2013, pp. 1399\u20131404. EDA Consortium (2013)","DOI":"10.7873\/DATE.2013.286"},{"key":"14_CR31","unstructured":"Robert, Y.S.H.A.M., Een, B.N.: Enhancing PDR\/IC3 with localization abstraction"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"key":"14_CR33","unstructured":"Traytel, D.: A coalgebraic decision procedure for WS1S. In: CSL2015. LIPIcs, vol. 41, pp. 487\u2013503. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"14_CR34","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency - Structure versus Automata, LNCS, vol. 1043, pp. 238\u2013266. Springer, Berlin (1996).https:\/\/doi.org\/10.1007\/3-540-60915-6","DOI":"10.1007\/3-540-60915-6"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-41528-4_13","volume-title":"Computer Aided Verification","author":"H-E Wang","year":"2016","unstructured":"Wang, H.-E., Tsai, T.-L., Lin, C.-H., Yu, F., Jiang, J.-H.R.: String analysis via automata manipulation with logic circuit representation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 241\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_13"},{"key":"14_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-02716-1_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P Wolper","year":"2009","unstructured":"Wolper, P.: On the use of automata for deciding linear arithmetic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 16\u201316. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_2"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: CAV 1998, pp. 88\u201397. Springer,Cham (1998)","DOI":"10.1007\/BFb0028736"},{"key":"14_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_5"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-89051-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,12]],"date-time":"2021-10-12T09:58:49Z","timestamp":1634032729000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-89051-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030890506","9783030890513"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-89051-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}