{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:22Z","timestamp":1780994482442,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_59","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"658-674","source":"Crossref","is-referenced-by-count":9,"title":["Nested Antichains for WS1S"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Fiedor","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"59_CR1","unstructured":"Meyer, A.R.: Weak monadic second order theory of successor is not elementary-recursive. In: Proc. of Logic Colloquium\u2014Symposium on Logic Held at Boston. LNCS, vol. 453. Springer (1972)"},{"key":"59_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification","author":"J. Elgaard","year":"1998","unstructured":"Elgaard, J., Klarlund, N., M\u00f8ller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 516\u2013520. Springer, Heidelberg (1998)"},{"key":"59_CR3","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Ver. 1.4 Manual. \n                      \n                        http:\/\/www.brics.dk\/mona\/"},{"key":"59_CR4","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proc. of POPL 2011. ACM (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"59_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-642-23702-7_8","volume-title":"Static Analysis","author":"P. Madhusudan","year":"2011","unstructured":"Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 43\u201359. Springer, Heidelberg (2011)"},{"key":"59_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"59_CR7","doi-asserted-by":"crossref","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. Science of Computer Programing 77(9) (2012)","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"59_CR8","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Proc. of POPL 2008. ACM (2008)","DOI":"10.1145\/1375581.1375624"},{"key":"59_CR9","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: Proc. of FMCAD 2010. IEEE (2010)"},{"key":"59_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/11691617_18","volume-title":"Model Checking Software","author":"C. Topnik","year":"2006","unstructured":"Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: A stand-alone tool and jABC plugin for M2L(Str). In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 293\u2013298. Springer, Heidelberg (2006)"},{"key":"59_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/978-3-642-15205-4_29","volume-title":"Computer Science Logic","author":"T. Ganzow","year":"2010","unstructured":"Ganzow, T., Kaiser, L.: New algorithm for weak monadic second-order logic on inductive structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 366\u2013380. Springer, Heidelberg (2010)"},{"key":"59_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T. Wies","year":"2011","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.) CADE 2011. LNCS, vol.\u00a06803, pp. 476\u2013491. Springer, Heidelberg (2011)"},{"key":"59_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 2\u201322. Springer, Heidelberg (2010)"},{"key":"59_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M. Wulf De","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.\u00a04144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"key":"59_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains (on checking language inclusion of NFAs). In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 158\u2013174. Springer, Heidelberg (2010)"},{"key":"59_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/10721959_20","volume-title":"Automated Deduction - CADE-17","author":"D. Bustan","year":"2000","unstructured":"Bustan, D., Grumberg, O.: Simulation based minimization. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 255\u2013270. Springer, Heidelberg (2000)"},{"key":"59_CR17","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proc. of POPL 2013. ACM (2013)","DOI":"10.1145\/2429069.2429124"},{"key":"59_CR18","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":"59_CR19","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Technical report, The University of Michigan (1959, 2010), \n                      \n                        http:\/\/hdl.handle.net\/2027.42\/3930"},{"key":"59_CR20","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: dWiNA (2014). \n                      \n                        http:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/dWiNA\/"},{"key":"59_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-642-28756-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Leng\u00e1l","year":"2012","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: A library for efficient manipulation of non-deterministic tree automata. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 79\u201394. Springer, Heidelberg (2012)"},{"key":"59_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-78800-3_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2008","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: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 93\u2013108. Springer, Heidelberg (2008)"},{"key":"59_CR23","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods in System Design 41(1) (2012)","DOI":"10.1007\/s10703-012-0150-8"},{"key":"59_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-540-70844-5_7","volume-title":"Implementation and Applications of Automata","author":"A. Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol.\u00a05148, pp. 57\u201367. Springer, Heidelberg (2008)"},{"key":"59_CR25","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested Antichains for WS1S. Technical report FIT-TR-2014-06, \n                      \n                        http:\/\/www.fit.vutbr.cz\/~ilengal\/pub\/FIT-TR-2014-06.pdf"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_59","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:22:37Z","timestamp":1559139757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}