{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T05:14:59Z","timestamp":1662182099330},"reference-count":8,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"9","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2022,9,1]]},"DOI":"10.1587\/transinf.2022edl8030","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T22:23:00Z","timestamp":1661984580000},"page":"1620-1623","source":"Crossref","is-referenced-by-count":0,"title":["Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking"],"prefix":"10.1587","volume":"E105.D","author":[{"given":"Yoshiaki","family":"TAKATA","sequence":"first","affiliation":[{"name":"School of Information, Kochi University of Technology"}]},{"given":"Ryoma","family":"SENDA","sequence":"additional","affiliation":[{"name":"Graduate School of Informatics, Nagoya University"}]},{"given":"Hiroyuki","family":"SEKI","sequence":"additional","affiliation":[{"name":"Graduate School of Informatics, Nagoya University"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] M. Kaminski and N. Francez, \u201cFinite-memory automata,\u201d Theor. Comput. Sci., vol.134, no.2, pp.329-363, 1994. 10.1016\/0304-3975(94)90242-9","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] A.S. Murawski, S.J. Ramsay, and N. Tzevelekos, \u201cReachability in pushdown register automata,\u201d J. Comput. Syst. Sci., vol.87, pp.58-83, 2017. 10.1016\/j.jcss.2017.02.008","DOI":"10.1016\/j.jcss.2017.02.008"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] R. Senda, Y. Takata, and H. Seki, \u201cLTL model checking for register pushdown systems,\u201d IEICE Trans. Inf. &amp; Syst., vol.E104-D, no.12, pp.2131-2144, Dec. 2021. 10.1587\/transinf.2020edp7265","DOI":"10.1587\/transinf.2020EDP7265"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] J. Esparza, A. Ku\u010dera, and S. Schwoon, \u201cModel checking LTL with regular valuations for pushdown systems,\u201d Inf. Comput., vol.186, no.2, pp.355-376, 2003. 10.1016\/s0890-5401(03)00139-1","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] R. Senda, Y. Takata, and H. Seki, \u201cReactive synthesis from visibly register pushdown automata,\u201d ICTAC 2021, Lecture Notes in Computer Science, vol.12819, pp.334-353, Springer, Sept. 2021. 10.1007\/978-3-030-85315-0_19","DOI":"10.1007\/978-3-030-85315-0_19"},{"key":"6","doi-asserted-by":"publisher","unstructured":"[6] F. Neven, T. Schwentick, and V. Vianu, \u201cFinite state machines for strings over infinite alphabets,\u201d ACM Trans. Comput. Log., vol.5, no.3, pp.403-435, 2004. 10.1145\/1013560.1013562","DOI":"10.1145\/1013560.1013562"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] B. Bollig, P. Habermehl, M. Leucker, and B. Monmege, \u201cA robust class of data languages and an application to learning,\u201d Log. Methods Comput. Sci., vol.10, no.4, pp.1-23, 2014. 10.2168\/lmcs-10(4:19)2014","DOI":"10.2168\/LMCS-10(4:19)2014"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] N. Tzevelekos, \u201cFresh-register automata,\u201d POPL&apos;11, pp.295-306, ACM, 2011. 10.1145\/1926385.1926420","DOI":"10.1145\/1925844.1926420"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E105.D\/9\/E105.D_2022EDL8030\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T04:55:01Z","timestamp":1662180901000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E105.D\/9\/E105.D_2022EDL8030\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,1]]},"references-count":8,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2022]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2022edl8030","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,1]]},"article-number":"2022EDL8030"}}