{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T05:53:28Z","timestamp":1746770008225,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T00:00:00Z","timestamp":1627948800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T00:00:00Z","timestamp":1627948800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10817-021-09597-w","type":"journal-article","created":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T09:03:21Z","timestamp":1627981401000},"page":"971-999","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automata Terms in a Lazy WSkS Decision Procedure"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2746-8792","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,3]]},"reference":[{"key":"9597_CR1","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 NFAs). In: TACAS\u201910, LNCS, vol. 6015, pp. 158\u2013174. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"9597_CR2","unstructured":"Basin, D., Klarlund, N.: Automata based symbolic reasoning in hardware verification. In: CAV\u201998, LNCS, pp. 349\u2013361. Springer (1998)"},{"key":"9597_CR3","doi-asserted-by":"crossref","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S systems to verify parameterized networks. In: TACAS\u201900, LNCS, vol. 1785, pp. 188\u2013203. Springer (2000)","DOI":"10.1007\/3-540-46419-0_14"},{"key":"9597_CR4","doi-asserted-by":"crossref","unstructured":"Bodeveix, J., Filali, M.: FMona: A tool for expressing validation techniques over infinite state systems. In: TACAS\u201900, LNCS, vol. 1785, pp. 204\u2013219. Springer (2000)","DOI":"10.1007\/3-540-46419-0_15"},{"key":"9597_CR5","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: CIAA\u201908, LNCS, vol. 5148, pp. 57\u201367. Springer (2008)","DOI":"10.1007\/978-3-540-70844-5_7"},{"key":"9597_CR6","unstructured":"Bozga, M., Iosif, R., Sifakis, J.: Structural invariants for parametric verification of systems with almost linear architectures. Tech. Rep. arXiv:1902.02696 (2019)"},{"key":"9597_CR7","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"issue":"9","key":"9597_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":"9597_CR9","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":"9597_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL\u201914., pp. 541\u2013554 (2014)","DOI":"10.1145\/2578855.2535849"},{"key":"9597_CR11","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.F.: Antichain algorithms for finite automata. In: TACAS\u201910, LNCS, vol. 6015, pp. 2\u201322. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"9597_CR12","doi-asserted-by":"crossref","unstructured":"Elgaard, J., Klarlund, N., M\u00f8ller, A.: MONA 1.x: New techniques for WS1S and WS2S. In: CAV\u201998. LNCS, vol. 1427, pp. 516\u2013520. Department of Computer Science, Aarhus University, Springer, BRICS (1998)","DOI":"10.1007\/BFb0028773"},{"key":"9597_CR13","doi-asserted-by":"crossref","unstructured":"Fiedor, T., Hol\u00edk, L., Jank\u016f, P., Leng\u00e1l, O., Vojnar, T.: Lazy automata techniques for WS1S. In: TACAS\u201917, LNCS, vol. 10205, pp. 407\u2013425. Springer (2017)","DOI":"10.1007\/978-3-662-54577-5_24"},{"key":"9597_CR14","doi-asserted-by":"crossref","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested antichains for WS1S. In: TACAS\u201915, LNCS, vol. 9035. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_59"},{"key":"9597_CR15","doi-asserted-by":"crossref","unstructured":"Ganzow, T., Kaiser, L.: New Algorithm for weak monadic second-order logic on inductive structures. In: CSL\u201910, LNCS, vol. 6247, pp. 366\u2013380. Springer (2010)","DOI":"10.1007\/978-3-642-15205-4_29"},{"key":"9597_CR16","doi-asserted-by":"crossref","unstructured":"Glenn, J., Gasarch, W.: Implementing WS1S via finite automata. In: Workshop on Implementing Automata, LNCS, vol. 1260, pp. 50\u201363. Springer (1996)","DOI":"10.1007\/3-540-63174-7_5"},{"issue":"1","key":"9597_CR17","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., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods Syst. Des. 41(1), 83\u2013106 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"9597_CR18","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD\u201910, pp. 101\u2013109. IEEE Computer Science (2010)"},{"key":"9597_CR19","doi-asserted-by":"crossref","unstructured":"Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Automata terms in a lazy WS$$k$$S decision procedure. In: Proceedings of of CADE-27, LNCS, vol. 11716, pp. 300\u2013318. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_18"},{"key":"9597_CR20","doi-asserted-by":"crossref","unstructured":"Hune, T., Sandholm, A.: A case study on using automata in control synthesis. In: FASE\u201900, LNCS, vol. 1783, pp. 349\u2013362. Springer (2000)","DOI":"10.1007\/3-540-46428-X_24"},{"key":"9597_CR21","doi-asserted-by":"crossref","unstructured":"Klarlund, N.: A\u00a0theory of restrictions for logics and automata. In: CAV\u201999, LNCS, vol. 1633, pp. 406\u2013417. Springer (1999)","DOI":"10.1007\/3-540-48683-6_35"},{"key":"9597_CR22","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 user manual. BRICS, Department of Computer Science, Aarhus University (2001). Notes Series NS-01-1. Available from http:\/\/www.brics.dk\/mona\/. Revision of BRICS NS-98-3"},{"issue":"4","key":"9597_CR23","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":"9597_CR24","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Nielsen, M., Sunesen, K.: A case study in automated verification based on trace abstractions. In: Formal System Specification, The RPC-Memory Specification Case Study, LNCS, vol. 1169. Springer (1996)","DOI":"10.1007\/BFb0024435"},{"key":"9597_CR25","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL\u201911, pp. 611\u2013622. ACM (2011)","DOI":"10.1145\/1925844.1926455"},{"key":"9597_CR26","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: SAS\u201911, LNCS, vol. 6887, pp. 43\u201359. Springer (2011)","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"9597_CR27","unstructured":"Margaria, T., Steffen, B., Topnik, C.: Second-order value numbering. In: GraMoT\u201910, ECEASST, vol.\u00a030, pp. 1\u201315. EASST (2010)"},{"key":"9597_CR28","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.: The pointer assertion logic engine. In: PLDI\u201901. ACM Press (2001). Also in SIGPLAN Notices 36(5) (2001)","DOI":"10.1145\/381694.378851"},{"key":"9597_CR29","unstructured":"Morawietz, F., Cornell, T.: The logic-automaton connection in linguistics. In: LACL\u201997, LNAI, vol. 1582. Springer (1997)"},{"key":"9597_CR30","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"9597_CR31","doi-asserted-by":"crossref","unstructured":"Sandholm, A., Schwartzbach, M.I.: Distributed safety controllers for web services. In: FASE\u201998, pp. 270\u2013284. Springer (1998)","DOI":"10.1007\/BFb0053596"},{"key":"9597_CR32","doi-asserted-by":"crossref","unstructured":"Smith, M.A., Klarlund, N.: Verification of a sliding window protocol using IOA and MONA. In: FORTE\/PSTV\u201900, IFIP, vol. 183, pp. 19\u201334. Kluwer (2000)","DOI":"10.1007\/978-0-387-35533-7_2"},{"key":"9597_CR33","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Fifth Annual ACM Symposium on Theory of Computing. STOC\u201973, pp. 1\u20139. ACM, New York (1973)","DOI":"10.1145\/800125.804029"},{"key":"9597_CR34","doi-asserted-by":"crossref","unstructured":"Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans. Comput. Log. 22(4), 33:1\u201333:33 (2013)","DOI":"10.1145\/2522920.2522926"},{"issue":"1","key":"9597_CR35","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"JW Thatcher","year":"1968","unstructured":"Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57\u201381 (1968)","journal-title":"Math. Syst. Theory"},{"key":"9597_CR36","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: SPIN\u201906, LNCS, vol. 3925, pp. 293\u2013298. Springer (2006)","DOI":"10.1007\/11691617_18"},{"key":"9597_CR37","unstructured":"Traytel, D.: A coalgebraic decision procedure for WS1S. In: 24th EACSL Annual Conference on Computer Science Logic (CSL\u201915). Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, pp. 487\u2013503. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015)"},{"key":"9597_CR38","doi-asserted-by":"crossref","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: CADE\u201911, LNCS, vol. 6803, pp. 476\u2013491. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_36"},{"key":"9597_CR39","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: CAV\u201906, LNCS, vol. 4144, pp. 17\u201330. Springer (2006)","DOI":"10.1007\/11817963_5"},{"key":"9597_CR40","unstructured":"Wulf, M.D., Doyen, L., Maquet, N., Raskin, J.F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: TACAS\u201908, LNCS, vol. 4693. Springer (2008)"},{"key":"9597_CR41","unstructured":"Wulf, M.D., Doyen, L., Raskin, J.F.: A lattice theory for solving games of imperfect information. In: HSCC\u201906, LNCS, vol. 3927. Springer (2006)"},{"key":"9597_CR42","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: POPL\u201908, pp. 349\u2013361. ACM (2008)","DOI":"10.1145\/1379022.1375624"},{"issue":"4","key":"9597_CR43","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."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09597-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09597-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09597-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:09:28Z","timestamp":1674565768000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09597-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,3]]},"references-count":43,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["9597"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09597-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,8,3]]},"assertion":[{"value":"15 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 August 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}