MF Researcher Database

Researchers Database

Advance

Hashimoto Kenji

  • Faculty of Engineering and Design
  • Department of Engineering and Design
  • Associate Professor
Last Updated :2026/06/24

Researcher Information

J-Global ID

Research Interests

  • SAT   model counting   formal language theory   

Research Areas

  • Informatics / Software
  • Informatics / Information theory

Academic & Professional Experience

  • 2024/04 - Today  Kagawa UniversityFaculty of Engineering and DesignAssociate professor
  • 2017/04 - 2024/03  Nagoya University大学院情報学研究科情報システム学専攻Assistant Professor
  • 2013/10 - 2017/03  Nagoya University大学院情報科学研究科情報システム学専攻Assistant Professor
  • 2009/04 - 2013/09  Nara Institute of Science and Technology情報科学研究科Assistant Professor

Education

  •        - 2009/03  Osaka University  Graduate School, Division of Information Science
  •        - 2006/03  Osaka University  Graduate School, Division of Information Science
  •        - 2004/03  Osaka University  Faculty of Engineering Science

Association Memberships

  • 電子情報通信学会   情報処理学会   

Published Papers

  • Inoue Y; Hashimoto K; Seki H
    Theoretical Computer Science Theoretical Computer Science 974 0304-3975 2023/09 [Refereed]
  • When Is Context-Freeness Distinguishable from Regularity? an Extension of Parikh’s Theorem
    Yusuke Inoue; Kenji Hashimoto; Hiroyuki Seki
    27th International Conference on Implementation and Application of Automata (CIAA 2023) , LNCS 14151 166 - 178 2023/09 [Refereed]
  • Hashimoto Kenji; Maneth Sebastian
    Theoretical Computer Science Theoretical Computer Science 963 0304-3975 2023/06 [Refereed]
  • INOUE Yusuke; HASHIMOTO Kenji; SEKI Hiroyuki
    IEICE Transactions on Information and Systems The Institute of Electronics, Information and Communication Engineers E106.D (3) 309 - 318 0916-8532 2023/03 [Refereed]
  • Inoue Yusuke; Hashimoto Kenji; Seki Hiroyuki
    26th International Conference on Implementation and Application of Automata (CIAA 2022) 13266 238 - 250 0302-9743 2022/06 [Refereed]
  • On the Compositionality of Dynamic Leakage and Its Application to the Quantification Problem
    Bao Trung Chu; Kenji Hashimoto; Hiroyuki Seki
    13th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE 2019) 1 - 8 2019/10 [Refereed]
  • Quantifying Dynamic Leakage -- Complexity Analysis and Model Counting-based Calculation
    Trung Bao Chu; Kenji Hashimoto; Hiroyuki Seki
    IEICE Transactions on Information and Systems E102-D (10) 1952 - 1965 2019/10 [Refereed]
  • Graph Compression by Tree Grammars and Direct Evaluation of Regular Path Query
    Takeshi Takeda; Kenji Hashimoto; Hiroyuki Seki
    IEEE 4th International Conference on Computer and Communication Systems (ICCCS 2019) 257 - 262 2019/02 [Refereed]
  • Counting Algorithms for Recognizable and Algebraic Series
    Trung Bao Chu; Kenji Hashimoto; Hiroyuki Seki
    IEICE Transactions on Information and Systems E101-D (6) 1479-1490  2018/06 [Refereed]
  • Direct Update of XML Documents with Data Values Compressed by Tree Grammars
    Kenji Hashimoto; Ryunosuke Takayama; Hiroyuki Seki
    IEICE Transactions on Information and Systems E101-D (6) 1467-1478  2018/06 [Refereed]
  • Direct Evaluation of Selecting Tree Automata on XML Documents Compressed with Top Trees
    Kenji Hashimoto; Suguru Nishimura; Hiroyuki Seki
    Proceedings of the 4th International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2016) 29-36  2016/07 [Refereed]
  • Query Rewriting for Nondeterministic Tree Transducers
    Kazuki Miyahara; Kenji Hashimoto; Hiroyuki Seki
    IEICE Transactions on Information and Systems E99-D (6) 1410-1419  2016/06 [Refereed]
  • Determinacy and Subsumption of Single-valued Bottom-up Tree Transducers
    Kenji Hashimoto; Ryuta Sawada; Yasunori Ishihara; Hiroyuki Seki; Toru Fujiwara
    IEICE Transactions on Information and Systems E99-D (3) 575-587  2016/03 [Refereed]
  • The Consistency and Absolute Consistency Problems of XML Schema Mappings between Restricted DTDs
    Hayato Kuwada; Kenji Hashimoto; Yasunori Ishihara; Toru Fujiwara
    World Wide Web Journal 18 (5) 1443-1461  2015/09 [Refereed]
  • Query-based l-diversity
    Chittaphone Phonharath; Ryonosuke Takayama; Kenji Hashimoto; Hiroyuki Seki
    Proceedings of the 7th International Conference on Advances in Databases, Knowledge, and Data Applications (DBKDA 2015) 15-20  2015/05 [Refereed]
  • Node Query Preservation for Deterministic Linear Top-Down Tree Transducers
    Kazuki Miyahara; Kenji Hashimoto; Hiroyuki Seki
    IEICE Transactions on Information and Systems E98-D (3) 512-523  2015/03 [Refereed]
  • Node Query Preservation for Deterministic Linear Top-Down Tree Transducers
    Kazuki Miyahara; Kenji Hashimoto; Hiroyuki Seki
    2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Electronic Proceedings in Theoretical Computer Science 134 27-37  2013/10 [Refereed]
  • XPath Satisfiability with Parent Axes or Qualifiers Is Tractable under Many of Real-World DTDs
    Yasunori Ishihara; Nobutaka Suzuki; Kenji Hashimoto; Shogo Shimizu; Toru Fujiwara
    Proceedings of the 14th International Symposium on Database Programming Languages 1-10  2013/08 [Refereed]
  • Decidability of k-secrecy against Inference Attacks Using Functional Dependencies on XML Databases
    Nobuaki Yamazoe; Kenji Hashimoto; Yasunori Ishihara; Toru Fujiwara
    Proceedings of the 2013 International Conference on Parallel and Distributed Processing Techniques and Applications 182-188  2013/07 [Refereed]
  • Deciding Schema k-Secrecy for XML Databases
    Chittaphone Phonharath; Kenji Hashimoto; Hiroyuki Seki
    IEICE Transactions on Information and Systems E96-D (6) 1268-1277  2013/06 [Refereed]
  • The Consistency and Absolute Consistency Problems of XML Schema Mappings between Restricted DTDs
    Hayato Kuwada; Kenji Hashimoto; Yasunori Ishihara; Toru Fujiwara
    Proceedings of the 15th International Asia-Pacific Web Conference 228-239  2013/04 [Refereed]
  • Determinacy and Subsumption for Single-valued Bottom-up Tree Transducers
    Kenji Hashimoto; Ryuta Sawada; Yasunori Ishihara; Hiroyuki Seki; Toru Fujiwara
    Proceedings of the 7th International Conference on Language and Automata Theory and Applications 335-346  2013/04 [Refereed]
  • Typing XPath Subexpressions With Respect to an XML Schema
    Yasunori Ishihara; Kenji Hashimoto; Atsushi Ohno; Takuji Morimoto; Toru Fujiwara
    Proceedings of the 5th International Conference on Advances in Databases, Knowledge, and Data Applications 128-133  2013/01 [Refereed]
  • XPath Satisfiability with Downward and Sibling Axes Is Tractable under Most of Real-world DTDs
    Yasunori Ishihara; Kenji Hashimoto; Shougo Shimizu; Toru Fujiwara
    Proceedings of the 12th International Workshop on Web Information and Data Management 11-18  2012/11 [Refereed]
  • Verification of the Security against Inference Attacks on XML Databases
    Chittaphone Phonharath; Kenji Hashimoto; Hiroyuki Seki
    The 1st International Workshop on Trends in Tree Automata and Tree Transducers 11-22  2012/06 [Refereed]
  • Decidability of the Security against Inference Attacks using a Functional Dependency on XML Databases
    Kenji Hashimoto; Hiroto Kawai; Yasunori Ishihara; Toru Fujiwara
    IEICE Transactions on Information and Systems E95-D (5) 1365-1374  2012/05 [Refereed]
  • Validity of Positive XPath Queries with Wildcard in the Presence of DTDs
    Kenji Hashimoto; Yohei Kusunoki; Yasunori Ishihara; Toru Fujiwara
    The 13th International Symposium on Database Programming Languages 1-8  2011/08 [Refereed]
  • A Tractable Subclass of DTDs for XPath Satisfiability with Sibling Axes
    Yasunori Ishihara; Takuji Morimoto; Shougo Shimizu; Kenji Hashimoto Toru Fujiwara
    Proceedings of the 12th International Symposium on Database Programming Languages 68-83  2009/08 [Refereed]
  • Verification of the Security against Inference Attacks on XML Databases
    Kenji Hashimoto; Kimihide Sakano; Fumikazu Takasuka; Yasunori Ishihara; Toru Fujiwara
    IEICE Transactions on Information and Systems E92-D (5) 1022-1032  2009/05 [Refereed]
  • Verification of the Security against Inference Attacks on XML Databases
    Kenji Hashimoto; Fumikazu Takasuka; Kimihide Sakano; Yasunori Ishihara; Toru Fujiwara
    Proceedings of the 10th Asia Pacific Web Conference 359-370  2008/04 [Refereed]
  • XMLデータベースにおけるスキーマ進化のための更新操作群とそれらのスキーマ表現能力保存に関する性質
    橋本 健二; 石原 靖哲; 藤原 融
    電子情報通信学会論文誌(D) J90-D (4) 990-1004  2007/04 [Refereed]
  • XMLデータベースへの推論攻撃による機密情報特定可能性の形式化とある前提条件のもとでの特定可能性検証法の提案
    高須賀 史和; 橋本 健二; 石原 靖哲; 藤原 融
    日本データベース学会Letters 5 (2) 21-24  2006/09 [Refereed]
  • Schema Update Operations Preserving the Expressive Power in XML Databases
    Kenji Hashimoto; Yasunori Ishihara; Toru Fujiwara
    Proceedings of the International Special Workshop on Databases for Next Generation Researchers in Memoriam Prof. Yahiko Kambayashi 38-41  2005/04 [Refereed]

Books etc

  • 理論計算機科学事典
    (Contributor5.2 木オートマトン，木トランスデューサ)朝倉書店 2022/01 807 456-471

Conference Activities & Talks

  • An Ambiguity Hierarchy of Weighted Context-free Grammars  [Not invited]
    Yusuke Inoue; Kenji Hashimoto; Hiroyuki Seki
    第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）  2023/03
  • 重み付き文脈自由文法の曖昧さ階層について  [Not invited]
    井上 裕介; 橋本 健二; 関 浩之
    2022年度 夏のLAシンポジウム  2022/07
  • Solving Rep-tile by Computers
    Mutsunori Banbara; Kenji Hashimoto; Takashi, Horiyama; Shin-ichi Minato; Kakeru Nakamura; Masaaki Nishino; Masahiko Sakai; Ryuhei Uehara; Yushi Uno; Norihito Yasuda
    The 14th Gathering 4 Gardner Conference (2022)  2022/04
  • 重み付き文脈自由文法の曖昧さ階層について
    井上 裕介; 橋本 健二; 関 浩之
    電子情報通信学会コンピュテーション研究会  2022/03
  • レプ・タイルの定式化を用いた各種ソルバの性能比較  [Not invited]
    番原 睦則; 橋本 健二; 堀山 貴史; 湊 真一; 中村 駆; 西野 正彬; 酒井 正彦; 上原 隆平; 宇野 裕之; 安田 宜仁
    人工知能学会 第119回人工知能基本問題研究会  2022/01
  • 命題論理式の全ての投射モデルを表現するBDDの構成法  [Not invited]
    磯貝孝明; 橋本健二; 酒井正彦
    第116回人工知能基本問題研究会  2021/03  オンライン
  • 擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化
    岸潤一郎; 酒井正彦; 西田直樹; 橋本健二
    ソフトウェアサイエンス研究会  2021/01  オンライン  電子情報通信学会
  • 組合せ最適化問題の記述からSMTソルバの入力式を生成するSQL問合せ
    坂梨元軌; 酒井正彦; 西田直樹; 橋本健二
    ソフトウェアサイエンス研究会  2019/03  那覇
  • 組合せ最適化問題を記述するための関係代数の集合上への拡張  [Not invited]
    坂梨 元軌; 酒井 正彦; 西田 直樹; 橋本 健二
    第20回プログラミングおよびプログラミング言語ワークショップ PPL2018  2018/03
  • 配列を含むC言語サブセットから難解言語Malbolgeへのコンパイラ  [Not invited]
    岩金 カナン; 坂梨 元軌; 酒井 正彦; 西田 直樹; 橋本 健二
    第20回プログラミングおよびプログラミング言語ワークショップ PPL2018  2018/03
  • 有向グラフに対する圧縮法および圧縮グラフに対する頂点選択問合せ評価法の提案  [Not invited]
    武田 健志; 橋本 健二; 関 浩之
    第10回データ工学と情報マネジメントに関するフォーラム（DEIM 2018）  2018/03
  • 線形マルチボトムアップ木変換器の関数性の決定可能性  [Not invited]
    田端 浩明; 橋本 健二
    第118回情報処理学会プログラミング研究会  2018/03
  • 非決定性選択木オートマトンの決定化
    川本 将也; 橋本 健二; 関 浩之
    第117回情報処理学会プログラミング研究会  2018/01
  • トップ木に基づく圧縮データに対する直接更新法
    西村 卓; 橋本 健二; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2017/10
  • 再帰呼び出しを持つC言語サブセットからMalbolgeへのコンパイラ
    坂梨 元軌; 河邉 翔平; 酒井 正彦; 西田 直樹; 橋本 健二
    電子情報通信学会ソフトウェアサイエンス研究会  2017/07
  • 木文法に基づくグラフ圧縮法および圧縮グラフに対する頂点選択問合せ評価法
    武田 健志; 関 浩之; 橋本 健二
    電子情報通信学会ソフトウェアサイエンス研究会  2017/07
  • 成分分割を用いる投射モデル計数ソルバにおける成分単位でのSAT判定を利用した性能改善
    鈴木 涼介; 橋本 健二; 酒井 正彦
    人工知能学会人工知能基本問題研究会  2017/03
  • モデル計数を用いた量的情報流解析のための論理式簡約と静的解析
    中島 聖斗; 橋本 健二; 酒井 正彦; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2017/03
  • 非線形トップダウン木変換器において問合せ保存が決定可能であるための十分条件
    石原 鷹; 橋本 健二; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2017/03
  • 木文法に基づき圧縮されたXML文書に対するデータ値を考慮した直接更新法
    高山 隆之介; 橋本 健二; 関 浩之
    第9回データ工学と情報マネジメントに関するフォーラム（DEIM 2017）  2017/03
  • Counting for Recognizable and Algebraic Series
    関 浩之; 橋本 健二; Trung Chu Bao
    情報処理学会 第113回プログラミング研究発表会  2017/03
  • あるクラスのXPath式から先読み付き決定性選択木オートマトンへのスキーマを用いた変換
    川本 将也; 橋本 健二; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2017/01
  • #SMTツールを用いた量的情報流解析手法の高速化
    中島 聖斗; Trung Chu Bao; 橋本 健二; 酒井 正彦; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2016/10
  • 木文法に基づく圧縮XML文書に対するデータ値を考慮した直接更新手法
    高山 隆之介; 橋本 健二; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2016/10
  • Determinacy and Query Preservation of Tree Transducers  [Invited]
    Kenji Hashimoto
    The 4th International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2016)
  • トップ木に基づく木圧縮法の実装と問い合わせ処理法の提案
    西村 卓; 橋本 健二; 関 浩之
    電子情報通信学会ソフトウェアサイエンス研究会  2016/07

MISC

Awards & Honors

  • 2023/09 International Competition on Graph Counting Algorithms The Inspiring Idea Track The First Place
     NaPS+GPMC international_society 
    受賞者: Kosuke Oguri;Kenji Hashimoto;Masakhiko Sakai
  • 2023/07 Model Counting Competition 2023 Projected Weighted Model Counting Track Ranking A the 1st place
     GPMC international_society 
    受賞者: Kenji Hashimoto
  • 2022/08 Model Counting Competition 2022 Projected Weighted Model Counting Track Ranking B 1st place
     international_society 
    受賞者: Kenji Hashimoto;Shota Yap
  • 2022/08 Model Counting Competition 2022 Projected Model Counting Track Ranking A 1st place
     GPMC international_society 
    受賞者: Kenji Hashimoto;Shota Yap
  • 2018/07 電子情報通信学会ソフトウェアサイエンス研究会 平成29年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞
     トップ木に基づく圧縮データに対する直接更新法 JPN japan_society 
    受賞者: 西村卓;橋本健二;関浩之
  • 2013/05 電子情報通信学会ソフトウェアサイエンス研究会 平成24年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞
     決定性線形下降木変換器における頂点問合せ保存 JPN japan_society 
    受賞者: 宮原 一喜;橋本 健二;関 浩之
  • 2008/12 数理モデル化と問題解決研究会 第72回数理モデル化と問題解決研究会プレゼンテーション賞
     XML Schema Evolution Preserving Information Based on the User-specified Relationship japan_society 
    受賞者: Kenji Hashimoto

Research Grants & Projects

  • 投射モデル計数のためのグラフ表現を用いた問題分類と計数戦略
    科学研究費助成事業
    Date (from‐to) : 2023/04 -2026/03 
    Author : 橋本 健二
     
    確率や量的な安全尺度の計算への応用を背景にして、論理式の解（モデル）の個数を高速に数える技術の必要性が高まっている。命題論理式のための既存の投射モデル計数ソルバやその計数戦略には一長一短があるが、それらを入力問題ごとに適切に切り替えるための有効な問題分類方法は知られていない。本研究では、論理式のグラフ表現に着目し、その特徴量を用いた投射モデル計数のための問題分類と計数戦略決定を試みる。機械学習を用いたモデル学習を通して、投射モデル計数問題の分類に役立つグラフ表現の特徴量を見いだすことで、高速に解くことができる適切なソルバや計数戦略を問題ごとに決定するシステムを構築する。
  • データハイブリッドなリアクティブプログラムの解析技術と自動合成・説明抽出への応用
    日本学術振興会：科学研究費助成事業
    Date (from‐to) : 2022/04 -2025/03 
    Author : 関 浩之; 小川 瑞史; 結縁 祥治; 橋本 健二
     
    レジスタ計算モデルに関する研究：データ値を扱う計算モデルであるレジスタオートマトン(RA), レジスタ文脈自由文法(RCFG), レジスタ木オートマトン(RTA)の能力を考察するため，それらの表現する言語クラスに対するポンプ補題を証明した．本補題を用い，RA, RCFG, RTAでは表現できない言語の具体例を示した． RAに対応する論理として，凍結演算子付きμ-計算（μ↓-計算）が知られている．しかしμ↓-計算は表現能力が大きすぎて自動検証への応用は難しい．本研究では，論理積に関する制約（高々一方のオペランドにしか凍結演算子，X以外の時相演算子を含まない）を満たす部分クラスμd↑-計算を定義し，RAとμd↑-計算の表現能力が同一であることを証明した． ノミナル集合はデータ値の無限集合を群論的に拡張した概念である．本研究では，決定性上昇型ノミナル木オートマトン(DBNTA)を定義し，DBNTAに対する対話型学習アルゴリズムを提案した．ノミナル集合上の適切な半順序を定義し，２つの軌道有限集合間にこの半順序に関する無限鎖が存在しないことを示すことで，提案アルゴリズムの停止性を証明した． 重み付きモデルに関する研究：多重文脈自由文法（mcfg）は文脈自由文法(cfg)の自然な拡張である．本研究では，mcfgに重みを導入したwmcfgを定義した．wmcfgは語の組を重みに対応づける関数を表現する．続いて，wmcfgに対する２つの基本問題が多項式時間判定可能であること，wmcfgによって表現される関数のクラスが，基本的な4つの演算に対して閉じていること等を証明した． 重み付きcfg(wcfg)は，cfgに重みを導入した計算モデルである．本研究では，トロピカル半環上の無あいまいwcfg, 有限あいまいwcfg, 多項式あいまいwcfg, および，一般のwcfgの間に，表現能力に関する真の階層関係が存在すること等を証明した．
  • データハイブリッドなリアクティブプログラムの解析技術と自動合成・説明抽出への応用
    日本学術振興会：科学研究費助成事業
    Date (from‐to) : 2022/04 -2025/03 
    Author : 関 浩之; 小川 瑞史; 結縁 祥治; 橋本 健二
     
    組込み制御ソフトウェアに代表されるリアクティブプログラムの信頼性を担保するための数理的手法を実用システムに適用可能にするためには，データ値，時間，確率等の量的概念を考慮した計算モデルの設定が鍵となる．本研究ではこのような問題意識のもとに，以下の課題に取り組む． データ値を扱うモデルであるレジスタ計算モデルについて，表現能力の同定，基本問題の計算量解析，特にリアクティブ合成問題とそれに関連するゲーム構造の数理的解析を行う． 重みとは，コスト等，計算に従って発生する付随量を表す．重み付き計算モデルの表現能力を明らかにし，重み付き計算モデルの対話的学習アルゴリズムを開発して，説明可能AIへ応用する．
  • ソフトウェアモデルへの量的尺度の導入とプログラム解析への応用
    日本学術振興会：科学研究費助成事業
    Date (from‐to) : 2019/04 -2023/03 
    Author : 関 浩之; 小川 瑞史; 結縁 祥治; 橋本 健二
     
    ソフトウェアの信頼性を担保するための数理的解析・検証技術を実用システムに適用可能にするためには，対象とする系をデータ値，時間，確率，情報量等の量的概念を考慮した数理的モデルに拡張する必要がある．本研究ではこのような問題意識のもとに，量的情報流の動的解析，データ値をもつ計算モデルとその構造化文書処理への応用，および，重みをもつ計算モデルとそのソフトウェアコスト解析への応用の３つの課題に取り組む．それぞれの課題において，オートマトンや形式文法に基づく適切な計算モデルを設定し，基本問題の計算量の解析，効率のよいアルゴリズムの開発，および，ツールの試作と実験に基づく提案手法の有効性の評価を行う． データ値をもつ計算モデルとそのソフトウェア開発への応用に関して以下の成果を得た． (1) 再帰プログラムのための簡潔な計算モデルとしてプッシュダウンシステム(Pushdown System, PDSと略)が知られている．本研究ではPDSをレジスタ付きに拡張したレジスタPDS（RPDSと略）を導入し，その高信頼ソフトウェア開発への応用に取り組んだ．レジスタオートマトンによって認識される言語を正則言語とよぶ．本研究ではまず，RPDSが前方正則保存性をもつことを証明した．この成果も踏まえ，RPDSのLTLモデル検査問題が判定可能であることを証明し，その計算複雑さについて明らかにした． (2) (1)のモデル検査問題ではプログラムのモデルはデータ値を扱えるが仕様（検証項目）を記述するLTL（時相論理）式ではデータ値を直接記述できない．そこで，レジスタオートマトンに変換可能な凍結演算子付き線形時相論理の部分クラスを見出した． (3) レジスタをもつ計算モデルとして，レジスタオートマトン，レジスタ文脈自由文法，ボトムアップ型レジスタ木オートマトンの表現する言語クラスのそれぞれに対して，いわゆるポンプの補題を証明した． 重み付き計算モデルとその応用：重み付きレジスタオートマトン(WRA)に対する重み最小実行問題の計算複雑さの解析とアルゴリズムの開発を行った成果をまとめた論文が，海外論文誌Theoretical Computer Science に採録された． また，文脈自由文法の拡張である多重文脈自由文法に重みを導入した重み付き多重文脈自由文法(WMCFG)を提案し，WMCFGに関する基本問題の判定可能性やWMCFGの生成する重み付き言語クラスの閉包性についても考察した．この研究発表に対して，電子情報通信学会ソフトウェアサイエンス研究会研究奨励賞を受賞した． 研究課題について，学術誌掲載論文３編，国内口頭発表４件の成果を挙げており，順調に進展していると自己評価できる． データ値をもつ計算モデルとそのソフトウェア開発への応用：今後は，再帰プログラムのための簡潔な計算モデルプッシュダウンシステム(Pushdown System, PDSと略)にレジスタを加えたRegister PDS(RPDSと略）について引き続き研究を行う．具体的に，RPDSのソフトウェア合成への応用として，プログラムの入出力関係を表す仕様が与えられたとき，それを満たすプログラムが存在するかを判定する実現可能性問題を考察する．具体的に，入力記号と出力記号が交互に並ぶような記号列からなる言語を認識するRPDSによって仕様を表現し，入力記号列を読んで出力記号列を生成するレジスタ付きプッシュダウン変換器（RPDTと略）によってモデル化する．既存研究として，有限オートマトン，レジスタオートマトン，PDSおよびそれらに対応する変換器を用いて定義された実現可能性問題の判定可能性が論じられているので，それらを参考にして理論的研究を進める． また，今年度の成果として得られた，レジスタオートマトン(RA)に変換可能な凍結演算子付き線形時相論理の部分クラスを拡張し，RAと能力等価な凍結演算子付きmu-計算の部分クラスを見出すことを試みる． 重み付き計算モデルとその応用：今後は，重み付き文脈自由文法（WCFG）の表現能力，例えば，曖昧さの程度（無曖昧，有限曖昧，多項式的曖昧など）が表現能力に及ぼす影響等について考察を行う．関連する既存研究として，重み付きオートマトンおよび重み付き木オートマトンについて，上述のような曖昧さの程度に基づく表現能力の階層性が示されている．階層性の証明には各クラスに対するポンプ補題が用いられる．WMCFGの部分クラスに対してもこの種のポンプ補題を証明することにより，曖昧さの程度に基づく部分クラスの階層性が証明できると予想している．
  • 量的情報流解析のための投射モデル計数ソルバの開発
    科学研究費補助金
    Date (from‐to) : 2017/04 -2020/03
  • Static Analysis and Dynamic Monitoring Methods for Software Security and Privacy
    Japan Society for the Promotion of Science：Grants-in-Aid for Scientific Research
    Date (from‐to) : 2015/04 -2019/03 
    Author : Seki Hiroyuki
     
    We investigated query preservation of nondeterministic tree transducers. We proposed methods of compressing large trees and graphs based on tree grammars or top trees and directly evaluating a query on them without decompressing the compressed data. Register context-free grammar (RCFG) is an extension of CFG by adding limited power of manipulating data values. We showed that both the membership and emptiness problems for RCFG are EXPTIME-complete. We analyzed the computational complexity of basic problems for weighted register automata (WRA) and proposed an algorithm that computes a minimum-weight run of a given WRA. We also conducted a fundamental study on SMT solvers and an empirical study on understanding the semantics of malware.
  • Formal models for quantitative analysis of software security
    Japan Society for the Promotion of Science：Grants-in-Aid for Scientific Research
    Date (from‐to) : 2014/04 -2018/03 
    Author : Seki Hiroyuki; HASHIMOTO KENJI
     
    A few quantitative notions for security and privacy of software such as quantitative information flow (QIF) and differential privacy have been proposed. In this research, we developed methods that analyze given programs or systems based on such notions. Specifically, we proposed an approximation algorithm that computes leakage by timing attack against an RSA decoder, a verification algorithm of k-secrecy of XML databases. Furthermore, as a theoretical basis for QIF analysis of programs that dynamically generate strings, we propose algorithms that counts, for a given recognizable or algebraic series S and a natural number d, the summation of the coefficients (or weights) of words of length d in S efficiently. The proposed methods were shown to be effective either by computer simulation or by experiments based on the implemented tools.
  • 木およびグラフ変換における問合せ保存の自動検証
    科学研究費補助金
    Date (from‐to) : 2014/04 -2017/03
  • Software Analysis based on Formaly Language Theory and Its Application to Security Verification
    Japan Society for the Promotion of Science：Grants-in-Aid for Scientific Research
    Date (from‐to) : 2011/04 -2016/03 
    Author : Seki Hiroyuki; OGAWA MIZUHITO; KAJI YUICHI; HASHIMOTO KENJI
     
    We obtained the following research results on information preservation and security of structured data, especially XML documents, based on tree language theory. A translation v is said to preserve a query q if there is a query q’ that can obtain from v(t) the same result when q is applied to t. We obtained decidability and complexity results on the problem of deciding preservation based on tree transducers and n-ary node queries. An inference attack is a behavior that tries to obtain the result of an unauthorized query by combining the result of authorized queries and other public information. We focused on k-secrecy and l-diversity as security notions against inference attacks. We discussed the decidability of schema k-secrecy problem and also compared the effectiveness of our two proposed methods of deciding l-diversity.
  • Derivation and update of XML schemas using conceptual model and query set
    Japan Society for the Promotion of Science：Grants-in-Aid for Scientific Research
    Date (from‐to) : 2010/04 -2013/03 
    Author : HASHIMOTO Kenji
     
    This research aims to propose a framework for XML schema update and XML document transformation considering information preservation. Wefocused on query preservation, which is a formalization of information preservation. We showed that, for some transformation and query classes modeled by tree transducers and tree automata, the problem of deciding the query preservation is decidable and a query that works directly over the transformed data can be constructed.

Committee Membership

  • 2019/05 -2019/08   23rd International Conference on Developments in Language Theory (DLT 2019)   PC member
  • 2018/05 -2018/09   22nd International Conference on Developments in Language Theory (DLT 2018)   PC member

Other link

researchmap


Copyright © MEDIA FUSION Co.,Ltd. All rights reserved.