{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T08:07:34Z","timestamp":1790496454567,"version":"4.1.0"},"reference-count":29,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"12","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2021,12,1]]},"DOI":"10.1587\/transinf.2020edp7265","type":"journal-article","created":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T22:38:37Z","timestamp":1638311917000},"page":"2131-2144","source":"Crossref","is-referenced-by-count":4,"title":["LTL Model Checking for Register Pushdown Systems"],"prefix":"10.1587","volume":"E104.D","author":[{"given":"Ryoma","family":"SENDA","sequence":"first","affiliation":[{"name":"Graduate School of Informatics, Nagoya University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yoshiaki","family":"TAKATA","sequence":"additional","affiliation":[{"name":"Graduate School of Engineering, Kochi University of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hiroyuki","family":"SEKI","sequence":"additional","affiliation":[{"name":"Graduate School of Informatics, Nagoya University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] P.A. Abdulla, C. Aiswarya, and M.F. Atig, \u201cData multi-pushdown automata,\u201d CONCUR 2017, pp.38:1-38:7, 2017. 10.4230\/LIPIcs.CONCUR.2017.38"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] P.A. Abdulla, M.F. Atig, G. Delzanno, and A. Podelski, \u201cPush-down automata with gap-order constraints,\u201d FSEN 2013, pp.199-216, 2013. 10.1007\/978-3-642-40213-5_13","DOI":"10.1007\/978-3-642-40213-5_13"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] A. Bouajjani, S. Fratani, and S. Qadeer, \u201cContext-bounded analysis of multithreaded programs with dynamic linked structures,\u201d CAV 2007, pp.207-220, 2007. 10.1007\/978-3-540-73368-3_24","DOI":"10.1007\/978-3-540-73368-3_24"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] M. Boja\u0144czyk, B. Klin, and S. Lasota, \u201cAutomata theory in nominal sets,\u201d Logical Methods in Computer Science, vol.10, no.3:4, pp.1-44, Aug. 2014. 10.2168\/LMCS-10(3:4)2014","DOI":"10.2168\/LMCS-10(3:4)2014"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] B. Bollig, A. Cyriac, P. Gastin, and K.N. Kumar, \u201cModel checking languages of data words,\u201d FoSSaCS 2012, LNCS, vol.7213, pp.391-405, 2012. 10.1007\/978-3-642-28729-9_26","DOI":"10.1007\/978-3-642-28729-9_26"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] A. Bouajjani, J. Esparza, and O. Maler, \u201cReachability analysis of pushdown automata: Application to model-checking,\u201d CONCUR 1997, LNCS, vol.1243, pp.135-150, 1997. 10.1007\/3-540-63141-0_10","DOI":"10.1007\/3-540-63141-0_10"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] P. Bouyer, \u201cA logical characterization of data languages,\u201d Inf. Process. Lett. vol.84, no.2, pp.75-85, Oct. 2002. 10.1016\/S0020-0190(02)00229-6","DOI":"10.1016\/S0020-0190(02)00229-6"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] Y-F. Chen, O. Leng\u00e1l, T. Tan, and Z. Wu, \u201cRegister automata with linear arithmetic,\u201d 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, 2017. 10.1109\/LICS.2017.8005111","DOI":"10.1109\/LICS.2017.8005111"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] E.Y.C. Cheng and M. Kaminski, \u201cContext-free languages over infinite alphabets,\u201d Acta Informatica 35, pp.245-267, 1998. 10.1007\/s002360050120","DOI":"10.1007\/s002360050120"},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] E.M. Clarke, O. Grumberg, and D.A. Peled, Model checking, MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"11","unstructured":"[11] L. Clemente and S Lasota, \u201cReachability analysis of first-order definable pushdown systems,\u201d CSL 2015, pp.244-259, 2015. 10.4230\/LIPIcs.CSL.2015.244"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] L. D'Antoni, T. Ferreira, M. Sammartino, and A. Silva, \u201cSymbolic register automata,\u201d 31th Int. Conf. Computer Aided Verification, LNCS, vol.11561, 2019. 10.1007\/978-3-030-25540-4_1","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] S. Demri and R. Lazi\u0107, \u201cLTL with the freeze quantifier and register automata,\u201d ACM TOCS, vol.10, no.3, pp.1-30, April 2009. 10.1145\/1507244.1507246","DOI":"10.1145\/1507244.1507246"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] S. Demri, R. Lazi\u0107 and D. Nowak, \u201cOn the freeze quantifier in constraint LTL: Decidability and complexity,\u201d Inf. Comput. vol.205, no.1, pp.2-24, Jan. 2007. 10.1016\/j.ic.2006.08.003","DOI":"10.1016\/j.ic.2006.08.003"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, \u201cEfficient algorithms for model checking pushdown systems,\u201d CAV 2000, LNCS, vol.1855, pp.232-247, 2000. 10.1007\/10722167_20","DOI":"10.1007\/10722167_20"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] J. Esparza, A. Ku\u010dera, and S. Schwoon, \u201cModel checking LTL with regular valuations for pushdown systems,\u201d Inform. and Comput, vol.186, no.2, pp.355-376, Nov. 2003. 10.1016\/S0890-5401(03)00139-1","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] S.A. Greibach, \u201cA note on pushdown store automata and regular systems,\u201d Proc. the American Mathematical Society, vol.18, pp.263-268, 1967. 10.1090\/S0002-9939-1967-0209086-1","DOI":"10.1090\/S0002-9939-1967-0209086-1"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] M. Kaminski and N. Francez, \u201cFinite-memory automata,\u201d TCS, vol.134, pp.322-363, Nov. 1994. 10.1016\/0304-3975(94)90242-9","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"19","doi-asserted-by":"crossref","unstructured":"[19] L. Libkin and D. Vrgo\u010d, \u201cRegular path queries on graphs with data,\u201d 15th Int. Conf. Database Theory, pp.74-85, March 2012. 10.1145\/2274576.2274585","DOI":"10.1145\/2274576.2274585"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] A.S. Murawski, S.J. Ramsay, and N. Tzevelekos, \u201cReachability in pushdown register automata,\u201d JCSS, vol.87, pp.58-83, Aug. 2017. 10.1016\/j.jcss.2017.02.008","DOI":"10.1016\/j.jcss.2017.02.008"},{"key":"21","doi-asserted-by":"publisher","unstructured":"[21] F. Neven, T. Schwentick, and V. Vianu, \u201cFinite state machines for strings over infinite alphabets,\u201d ACM Trans. Computational Logic vol.5, no.3, pp.403-435, July 2004. 10.1145\/1013560.1013562","DOI":"10.1145\/1013560.1013562"},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] N. Nitta, Y. Takata, and H. Seki, \u201cAn efficient security verification method for programs with stack inspection,\u201d ACM CCS, pp.68-77, Nov. 2001. 10.1145\/501983.501994","DOI":"10.1145\/373256.373260"},{"key":"23","unstructured":"[23] J. Rot, F. de Boer, and M. Bonsangue, \u201cPushdown system representation for unbounded object creation,\u201d Tech. Rep. KIT-13, Karlsruhe Institute of Technology, 38-52, 2010."},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] R. Senda, Y. Takata, and H. Seki, \u201cComplexity results on register context-free grammars and register tree automata,\u201d ICTAC 2018, LNCS, vol.11187, pp.415-434, 2018. 10.1007\/978-3-030-02508-3_22","DOI":"10.1007\/978-3-030-02508-3_22"},{"key":"25","doi-asserted-by":"publisher","unstructured":"[25] R. Senda, Y. Takata, and H. Seki, \u201cGeneralized register context-free grammars,\u201d LATA 2019, LNCS, vol.11417, pp.259-271, revised version: IEICE Trans. Inf. & Syst., vol.E103-D, no.3, pp.540-548, March 2020. 10.1587\/transinf.2019FCP0010","DOI":"10.1587\/transinf.2019FCP0010"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] R. Senda, Y. Takata, and H. Seki, \u201cForward regularity preservation property of register pushdown systems,\u201d IEICE Trans. Inf. & Syst., vol.E104-D, no.3, pp.370-380, March 2021 (to appear). 10.1587\/transinf.2020FCP0008","DOI":"10.1587\/transinf.2020FCP0008"},{"key":"27","doi-asserted-by":"publisher","unstructured":"[27] F. Song and T. Touili, \u201cPushdown model checking for malware detection,\u201d TACAS 2012, extended version, IJSTTT, vol.16, pp.147-173, 2014. 10.1007\/s10009-013-0290-1","DOI":"10.1007\/s10009-013-0290-1"},{"key":"28","doi-asserted-by":"crossref","unstructured":"[28] I. Walukiewicz, \u201cPushdown processes: Games and model checking,\u201d CAV 1996, LNCS, vol.1102, pp.62-74, 1996. 10.1007\/3-540-61474-5_58","DOI":"10.1007\/3-540-61474-5_58"},{"key":"29","doi-asserted-by":"publisher","unstructured":"[29] C. Xiaojuan and M. Ogawa, \u201cWell-structured extensions of pushdown systems,\u201d CONCUR 2013, pp.121-136, 2013. 10.1007\/978-3-642-40184-8_10","DOI":"10.1007\/978-3-642-40184-8_10"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/12\/E104.D_2020EDP7265\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,4]],"date-time":"2021-12-04T03:46:45Z","timestamp":1638589605000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/12\/E104.D_2020EDP7265\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,1]]},"references-count":29,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2021]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2020edp7265","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,1]]},"article-number":"2020EDP7265"}}