2022 Fiscal Year Annual Research Report
データハイブリッドなリアクティブプログラムの解析技術と自動合成・説明抽出への応用
| Project/Area Number |
22H03568
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | 形式言語理論 / レジスタ計算モデル / 重み付き計算モデル / 対話的学習 / あいまいさ階層 |
|---|
| Outline of Annual Research Achievements |
レジスタ計算モデルに関する研究：データ値を扱う計算モデルであるレジスタオートマトン(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の間に，表現能力に関する真の階層関係が存在すること等を証明した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
学術誌に３編，および，当該専門分野の査読付き国際会議に２編フルペーパーが採択されている等，十分な成果が上がっていることから，進捗状況はおおむね順調であるといえる．
|
| Strategy for Future Research Activity |
今後は，計算モデルとしてオートマトンや形式文法を用いると同時に，ゲーム構造を用いてソフトウェア検証，プログラム自動合成およびプライバシー保護に関する基礎的研究を行う．具体的に，リアクティブプログラムの自動合成問題（合成問題と略）に関する二つの課題に取り組む．一つは確率的ゲーム構造に対する非協調的合成問題（合成しようとするシステムに対して，環境が必ずしも協調するとは限らないという現実的設定のもとで，システムが勝利するようなNash均衡が存在するならば，それを構成する問題）である．
もう一つは，レジスタ付き合成問題（頂点にデータ値が関連づけられた有向グラフ上のゲームにおいて，RAで与えられる仕様すなわち勝利目的を満たすレジスタ変換器を構成する問題）である．
また，ゲームにおけるプレイヤーの勝利目的をそのプレイヤー（ユーザ）のプライバシー情報とみなし，ゲームを観測する敵対者がプレイヤーの勝利目的を推測するのをできる限り困難とするような戦略（識別不能戦略）および，どのプレイヤーも単独では推測困難性を大きくすることはできないような戦略の組（勝利目的識別不能均衡）を定義し，それらに関する判定問題の判定可能性や計算量を解析する．
形式言語の周期性に関しては，ある種の周期性をもつ正規言語を，巡回群などを用いて代数的に分解する手法を考察する．
|
| Remarks |
令和5年度電子情報通信学会ソフトウェアサイエンス研究会研究奨励賞, March 2024.（中西凜道，高田喜朗，関浩之）
|
