{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T02:51:59Z","timestamp":1725331919269},"reference-count":20,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2023,3,1]]},"DOI":"10.1587\/transinf.2022fcp0003","type":"journal-article","created":{"date-parts":[[2023,2,28]],"date-time":"2023-02-28T22:20:18Z","timestamp":1677622818000},"page":"294-302","source":"Crossref","is-referenced-by-count":1,"title":["A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata"],"prefix":"10.1587","volume":"E106.D","author":[{"given":"Yoshiaki","family":"TAKATA","sequence":"first","affiliation":[{"name":"School of Information, Kochi University of Technology"}]},{"given":"Akira","family":"ONISHI","sequence":"additional","affiliation":[{"name":"Graduate School of Informatics, Nagoya University"}]},{"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","unstructured":"[1] E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking, second ed., MIT Press, 2018."},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] 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":"3","doi-asserted-by":"publisher","unstructured":"[3] 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":"4","doi-asserted-by":"publisher","unstructured":"[4] E.Y.C. Cheng and M. Kaminski, \u201cContext-free languages over infinite alphabets,\u201d Acta Informatica, vol.35, no.3, pp.245-267, 1998. 10.1007\/s002360050120","DOI":"10.1007\/s002360050120"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] M. Kaminski and T. Tan, \u201cTree automata over infinite alphabets,\u201d Pillars of Computer Science, Lecture Notes in Computer Science, vol.4800, pp.386-423, Springer, 2008. 10.1007\/978-3-540-78127-1_21","DOI":"10.1007\/978-3-540-78127-1_21"},{"key":"6","doi-asserted-by":"publisher","unstructured":"[6] 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":"7","doi-asserted-by":"crossref","unstructured":"[7] L. Libkin and D. Vrgo\u010d, \u201cRegular path queries on graphs with data,\u201d 15th Int. Conf. on Database Theory, ICDT '12, pp.74-85, ACM, 2012. 10.1145\/2274576.2274585","DOI":"10.1145\/2274576.2274585"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] L. Libkin, T. Tan, and D. Vrgo\u010d, \u201cRegular expressions for data words,\u201d J. Comput. Syst. Sci., vol.81, no.7, pp.1278-1297, 2015. 10.1016\/j.jcss.2015.03.005","DOI":"10.1016\/j.jcss.2015.03.005"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] H. Sakamoto and D. Ikeda, \u201cIntractability of decision problems for finite-memory automata,\u201d Theor. Comput. Sci., vol.231, no.2, pp.297-308, 2000. 10.1016\/s0304-3975(99)00105-x","DOI":"10.1016\/S0304-3975(99)00105-X"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] 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":"11","doi-asserted-by":"publisher","unstructured":"[11] M. Boja\u0144czyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin, \u201cTwo-variable logic on data words,\u201d ACM Trans. Comput. Log., vol.12, no.4, pp.27:1-27:26, 2011. 10.1145\/1970398.1970403","DOI":"10.1145\/1970398.1970403"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] S. Demri and R. Lazi\u0107, \u201cLTL with the freeze quantifier and register automata,\u201d ACM Trans. Comput. Log., vol.10, no.3, pp.16:1-16:30, 2009. 10.1145\/1507244.1507246","DOI":"10.1145\/1507244.1507246"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] L. Segoufin, \u201cAutomata and logics for words and trees over an infinite alphabet,\u201d Computer Science Logic, CSL 2006, Lecture Notes in Computer Science, vol.4207, pp.41-57, Springer, 2006. 10.1007\/11874683_3","DOI":"10.1007\/11874683_3"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] 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, 2021. 10.1587\/transinf.2020fcp0008","DOI":"10.1587\/transinf.2020FCP0008"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] R. Senda, Y. Takata, and H. Seki, \u201cLTL model checking for register pushdown systems,\u201d IEICE Trans. Inf. & Syst., vol.E104-D, no.12, pp.2131-2144, 2021. 10.1587\/transinf.2020edp7265","DOI":"10.1587\/transinf.2020EDP7265"},{"key":"16","unstructured":"[16] A. Onishi, R. Senda, Y. Takata, and H. Seki, \u201cA subclass of LTL with the freeze quantifier translatable into register automata,\u201d IEICE Tech. Rep., vol.120, no.407, SS2020-29, pp.7-12, March 2021 (in Japanese)."},{"key":"17","doi-asserted-by":"crossref","unstructured":"[17] M. Jurdzi\u0144ski and R. Lazi\u0107, \u201cAlternation-free modal mu-calculus for data trees,\u201d 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), pp.131-140, IEEE Computer Society, 2007. 10.1109\/lics.2007.11","DOI":"10.1109\/LICS.2007.11"},{"key":"18","unstructured":"[18] A. Onishi, R. Senda, Y. Takata, and H. Seki, \u201cA subclass of mu-calculus with the freeze quantifier equivalent to register automata,\u201d IEICE Tech. Rep., vol.121, no.204, SS2021-17, pp.23-28, Oct. 2021 (in Japanese)."},{"key":"19","unstructured":"[19] L. Exibard, E. Filiot, and P. Reynier, \u201cSynthesis of data word transducers,\u201d Log. Methods Comput. Sci., vol.17, no.1, pp.22:1-22:25, 2021. 10.23638\/LMCS-17(1:22)2021"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] H. Seki, R. Yoshimura, and Y. Takata, \u201cOptimal run problem for weighted register automata,\u201d Theor. Comput. Sci., vol.850, pp.185-201, 2021. 10.1016\/j.tcs.2020.11.003","DOI":"10.1016\/j.tcs.2020.11.003"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E106.D\/3\/E106.D_2022FCP0003\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,4]],"date-time":"2023-03-04T04:15:54Z","timestamp":1677903354000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E106.D\/3\/E106.D_2022FCP0003\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,1]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2022fcp0003","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,1]]},"article-number":"2022FCP0003"}}