2021 Fiscal Year Annual Research Report
ソフトウェアモデルへの量的尺度の導入とプログラム解析への応用
| Project/Area Number |
19H04083
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / レジスタオートマトン / ゲーム構造 / アクティブ学習 / 重み付き文脈自由文法 / mu-計算 / プログラム合成 |
|---|
| Outline of Annual Research Achievements |
データ値をもつ計算モデルとそのソフトウェア開発への応用に関して以下の成果を得た．
(1) 文脈自由文法をレジスタ付きに拡張したレジスタ文脈自由文法とそれに関連する計算モデルについて，所属問題と空問題の計算複雑さを明らかにした論文が，海外論文誌Theoretical Computer Science に採録された．(2) 再帰プログラムのための計算モデルであるプッシュダウンシステム(Pushdown System, PDSと略)をレジスタ付きに拡張したレジスタPDS（RPDSと略）のLTLモデル検査問題が判定可能であることを証明し，その計算複雑さについて明らかにした．さらにフレッシュ性と呼ばれる条件を満たすRPDSのLTLモデル検査問題を通常のPDSの同問題に還元する手法を提案した．これらはいずれも学術論文誌に掲載された．(3) 昨年度はレジスタオートマトン(RA)に変換可能な凍結演算子付き線形時相論理の部分クラスを見出したが，今年度はこの研究を進展させ，RAと能力等価な凍結演算子付きmu-計算の部分クラスを見出した．この研究発表に対して，電子情報通信学会ソフトウェアサイエンス研究会研究奨励賞および電子情報通信学会ディペンダブルコンピューティング研究会若手優秀講演賞を同時受賞した．(4) レジスタモデルを群論的に抽象化したノミナルモデルを用い，決定性上昇型ノミナル木オートマトンを定義し，それに対するアクティブ学習アルゴリズムを提案した．(5) データ木書換え系を定義しその正則保存性およびセキュリティ検証への応用について考察した．
ゲーム構造：確率的多プレイヤー非ゼロサムゲームの非協調的合成問題を定義し，いくつかの部分クラスに対する本問題の計算複雑さを解析した．
重み付き計算モデル：重み付き文脈自由文法における曖昧さの度合いに基づく表現能力の変化や階層性について考察した．
|
| Research Progress Status |
令和3年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和3年度が最終年度であるため、記入しない。
|
