{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00200715","sets":["934:935:9619:9937"]},"path":["9937"],"owner":"44499","recid":"200715","title":["Solving String Constraints with Streaming String Transducers"],"pubdate":{"attribute_name":"公開日","attribute_value":"2019-11-20"},"_buckets":{"deposit":"768e0912-4961-40fb-90dd-a9de98e19978"},"_deposit":{"id":"200715","pid":{"type":"depid","value":"200715","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Solving String Constraints with Streaming String Transducers","author_link":["488677","488680","488681","488679","488678","488682"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Solving String Constraints with Streaming String Transducers"},{"subitem_title":"Solving String Constraints with Streaming String Transducers","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[通常論文] string constraints, streaming string transducers, transducers","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2019-11-20","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology"},{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology"},{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology","subitem_text_language":"en"},{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology","subitem_text_language":"en"},{"subitem_text_value":"Department of Mathematical and Computing Science, Tokyo Institute of Technology","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/200715/files/IPSJ-TPRO1205002.pdf","label":"IPSJ-TPRO1205002.pdf"},"date":[{"dateType":"Available","dateValue":"2021-11-20"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO1205002.pdf","filesize":[{"value":"710.7 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"65fff772-7414-4945-ba28-f515d4b01593","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2019 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Qizhen, Zhu"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hitoshi, Akama"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yasuhiko, Minamide"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Qizhen, Zhu","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hitoshi, Akama","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yasuhiko, Minamide","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"We present a procedure to solve the satisfiability problem of string constraints consisting of (i) string concatenation and rational transductions of string variables restricted to be in the “straight-line” fragment, (ii) regular constraints to string variables, and (iii) integer constraints involving the length of string variables. We represent each atomic string constraint by a streaming string transducer. By the sequential composition of streaming string transducers, we obtain a single streaming string transducer. The input straight-line constraint is satisfiable if and only if the domain of the composed streaming string transducer is not empty. In addition, by calculating the Parikh image of the composed streaming string transducers, we can represent the constraints among the length of string variables as a semi-linear set. Then the integer constraints together with the Parikh image can be solved by existing SMT solvers. We have implemented this procedure and performed experiments on several string constraints. Our implementation is slower than other solvers for general cases but performs better for some special cases.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.27(2019) (online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"We present a procedure to solve the satisfiability problem of string constraints consisting of (i) string concatenation and rational transductions of string variables restricted to be in the “straight-line” fragment, (ii) regular constraints to string variables, and (iii) integer constraints involving the length of string variables. We represent each atomic string constraint by a streaming string transducer. By the sequential composition of streaming string transducers, we obtain a single streaming string transducer. The input straight-line constraint is satisfiable if and only if the domain of the composed streaming string transducer is not empty. In addition, by calculating the Parikh image of the composed streaming string transducers, we can represent the constraints among the length of string variables as a semi-linear set. Then the integer constraints together with the Parikh image can be solved by existing SMT solvers. We have implemented this procedure and performed experiments on several string constraints. Our implementation is slower than other solvers for general cases but performs better for some special cases.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.27(2019) (online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicIssueDates":{"bibliographicIssueDate":"2019-11-20","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"5","bibliographicVolumeNumber":"12"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"id":200715,"updated":"2025-01-19T21:16:12.564450+00:00","links":{},"created":"2025-01-19T01:04:13.240379+00:00"}