{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T07:29:32Z","timestamp":1783150172068,"version":"3.54.6"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s00236-018-0331-z","type":"journal-article","created":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:49:23Z","timestamp":1546303763000},"page":"205-228","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Nested antichains for WS1S"],"prefix":"10.1007","volume":"56","author":[{"given":"Tom\u00e1\u0161","family":"Fiedor","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2746-8792","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,1]]},"reference":[{"key":"331_CR1","doi-asserted-by":"crossref","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested antichains for WS1S. In: TACAS\u201915. Volume 9035 of LNCS. Springer, pp. 658\u2013674 (2015)","DOI":"10.1007\/978-3-662-46681-0_59"},{"key":"331_CR2","doi-asserted-by":"crossref","unstructured":"Meyer, A.R.: Weak monadic second order theory of successor is not elementary-recursive. In Parikh, R., (ed.) Proceedings of Logic Colloquium\u2014Symposium on Logic Held at Boston, 1972\u20131973. Volume 453 of Lecture Notes in Mathematics. Springer, pp. 132\u2013154 (1972)","DOI":"10.1007\/BFb0064872"},{"key":"331_CR3","doi-asserted-by":"crossref","unstructured":"Elgaard, J., Klarlund, N., M\u00f8ller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Proceedings of CAV\u201998. Volume 1427 of Lecture Notes in Computer Science. Springer, pp. 516\u2013520 (1998)","DOI":"10.1007\/BFb0028773"},{"key":"331_CR4","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University. Notes Series NS-01-1. \n                    http:\/\/www.brics.dk\/mona\/\n                    \n                   (2001) . Revision of BRICS NS-98-3"},{"key":"331_CR5","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of POPL\u201911. ACM, pp. 611\u2013622 (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"331_CR6","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: Proceedings of SAS\u201911. Volume 6887 of Lecture Notes in Computer Science. Springer, pp. 43\u201359 (2011)","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"331_CR7","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., \u0160im\u00e1\u010dek, J.: The tree width of separation logic with recursive definitions. In: CADE 2013. Volume 7898 of Lecture Notes in Computer Science. Springer, pp. 21\u201338 (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"issue":"9","key":"331_CR8","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W Chin","year":"2012","unstructured":"Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"331_CR9","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Proceedings of POPL\u201908. ACM, pp. 349\u2013361 (2008)","DOI":"10.1145\/1375581.1375624"},{"issue":"4","key":"331_CR10","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s10817-013-9293-6","volume":"52","author":"M Zhou","year":"2014","unstructured":"Zhou, M., He, F., Wang, B., Gu, M., Sun, J.: Array theory of bounded elements and its applications. J. Autom. Reason. 52(4), 379\u2013405 (2014)","journal-title":"J. Autom. Reason."},{"key":"331_CR11","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: Proceedings of FMCAD\u201910. IEEE, pp. 101\u2013109 (2010)"},{"key":"331_CR12","doi-asserted-by":"crossref","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Proceedings of CADE\u201911. Volume 6803 of Lecture Notes in Computer Science. Springer, pp. 476\u2013491 (2011)","DOI":"10.1007\/978-3-642-22438-6_36"},{"key":"331_CR13","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.F.: Antichain algorithms for finite automata. In: Proceedings of TACAS\u201910. Volume 6015 of LNCS. Springer, pp. 2\u201322 (2010)","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"331_CR14","doi-asserted-by":"crossref","unstructured":"Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.F.: Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of CAV\u201906. Volume 4144 of LNCS. Springer, pp. 17\u201330 (2006)","DOI":"10.1007\/11817963_5"},{"key":"331_CR15","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains (on checking language inclusion of nondeterministic finite (tree) automata). In: Esparza, J., Majumdar, R. (eds.) Proceedings of TACAS\u201910. Volume 6015 of Lecture Notes in Computer Science. Springer, pp. 158\u2013174 (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"331_CR16","doi-asserted-by":"crossref","unstructured":"Bustan, D., Grumberg, O.: Simulation based minimization. In: Proceedings of CADE\u201900. Volume 1831 of Lecture Notes in Computer Science. Springer, pp. 255\u2013270 (2000)","DOI":"10.1007\/10721959_20"},{"key":"331_CR17","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Hol\u00edk, L., Kaati, L., Vojnar, T.: Computing simulations over tree automata: efficient techniques for reducing tree automata. In: Proceedings of TACAS\u201908. Volume 4963 of LNCS. Springer, pp. 93\u2013108 (2008)","DOI":"10.1007\/978-3-540-78800-3_8"},{"key":"331_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Proceedings of CIAA\u201908. Volume 5148 of LNCS. Springer, pp. 57\u201367 (2008)","DOI":"10.1007\/978-3-540-70844-5_7"},{"issue":"1","key":"331_CR19","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-012-0150-8","volume":"41","author":"P Habermehl","year":"2012","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., Sim\u00e1cek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Form. Methods Syst. Des. 41(1), 83\u2013106 (2012)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"331_CR20","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. Found. Comput. Sci. 13(4), 571\u2013586 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"331_CR21","doi-asserted-by":"crossref","unstructured":"Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: A stand-alone tool and jABC plugin for M2L(Str). In: Proceedings of SPIN\u201906. Volume 3925 of Lecture Notes in Computer Science. Springer, pp. 293\u2013298 (2006)","DOI":"10.1007\/11691617_18"},{"key":"331_CR22","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of POPL\u201914, pp. 541\u2013554 (2014)","DOI":"10.1145\/2535838.2535849"},{"key":"331_CR23","doi-asserted-by":"crossref","unstructured":"Ganzow, T., Kaiser, L.: New algorithm for weak monadic second-order logic on inductive structures. In: Proceedings of CSL\u201910. Volume 6247 of Lecture Notes in Computer Science. Springer, pp. 366\u2013380 (2010)","DOI":"10.1007\/978-3-642-15205-4_29"},{"key":"331_CR24","unstructured":"Traytel, D.: A coalgebraic decision procedure for WS1S. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 487\u2013503 (2015)"},{"key":"331_CR25","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2008)"},{"key":"331_CR26","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Technical report, The University of Michigan (1959). \n                    http:\/\/hdl.handle.net\/2027.42\/3930\n                    \n                   (2010)"},{"key":"331_CR27","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: dWiNA. \n                    http:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/dWiNA\/\n                    \n                   (2014)"},{"key":"331_CR28","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: a library for efficient manipulation of non-deterministic tree automata. In: Proceedings of TACAS\u201912. Volume 7214 of Lecture Notes in Computer Science. Springer, pp. 79\u201394 (2012)","DOI":"10.1007\/978-3-642-28756-5_7"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0331-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-018-0331-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0331-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T09:46:16Z","timestamp":1585907176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-018-0331-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,1]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["331"],"URL":"https:\/\/doi.org\/10.1007\/s00236-018-0331-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,1]]},"assertion":[{"value":"31 December 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}