2020 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 | ソフトウェア検証 / モデル検査 / レジスタオートマトン / 線形時相論理 / 重み付き文脈自由文法 |
|---|
| Outline of Annual Research Achievements |
データ値をもつ計算モデルとそのソフトウェア開発への応用に関して以下の成果を得た．
(1) 再帰プログラムのための簡潔な計算モデルとしてプッシュダウンシステム(Pushdown System, PDSと略)が知られている．本研究ではPDSをレジスタ付きに拡張したレジスタPDS（RPDSと略）を導入し，その高信頼ソフトウェア開発への応用に取り組んだ．レジスタオートマトンによって認識される言語を正則言語とよぶ．本研究ではまず，RPDSが前方正則保存性をもつことを証明した．この成果も踏まえ，RPDSのLTLモデル検査問題が判定可能であることを証明し，その計算複雑さについて明らかにした．
(2) (1)のモデル検査問題ではプログラムのモデルはデータ値を扱えるが仕様（検証項目）を記述するLTL（時相論理）式ではデータ値を直接記述できない．そこで，レジスタオートマトンに変換可能な凍結演算子付き線形時相論理の部分クラスを見出した．
(3) レジスタをもつ計算モデルとして，レジスタオートマトン，レジスタ文脈自由文法，ボトムアップ型レジスタ木オートマトンの表現する言語クラスのそれぞれに対して，いわゆるポンプの補題を証明した．
重み付き計算モデルとその応用：重み付きレジスタオートマトン(WRA)に対する重み最小実行問題の計算複雑さの解析とアルゴリズムの開発を行った成果をまとめた論文が，海外論文誌Theoretical Computer Science に採録された．
また，文脈自由文法の拡張である多重文脈自由文法に重みを導入した重み付き多重文脈自由文法(WMCFG)を提案し，WMCFGに関する基本問題の判定可能性やWMCFGの生成する重み付き言語クラスの閉包性についても考察した．この研究発表に対して，電子情報通信学会ソフトウェアサイエンス研究会研究奨励賞を受賞した．
|
| 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 |
データ値をもつ計算モデルとそのソフトウェア開発への応用：今後は，再帰プログラムのための簡潔な計算モデルプッシュダウンシステム(Pushdown System, PDSと略)にレジスタを加えたRegister PDS(RPDSと略）について引き続き研究を行う．具体的に，RPDSのソフトウェア合成への応用として，プログラムの入出力関係を表す仕様が与えられたとき，それを満たすプログラムが存在するかを判定する実現可能性問題を考察する．具体的に，入力記号と出力記号が交互に並ぶような記号列からなる言語を認識するRPDSによって仕様を表現し，入力記号列を読んで出力記号列を生成するレジスタ付きプッシュダウン変換器（RPDTと略）によってモデル化する．既存研究として，有限オートマトン，レジスタオートマトン，PDSおよびそれらに対応する変換器を用いて定義された実現可能性問題の判定可能性が論じられているので，それらを参考にして理論的研究を進める．
また，今年度の成果として得られた，レジスタオートマトン(RA)に変換可能な凍結演算子付き線形時相論理の部分クラスを拡張し，RAと能力等価な凍結演算子付きmu-計算の部分クラスを見出すことを試みる．
重み付き計算モデルとその応用：今後は，重み付き文脈自由文法（WCFG）の表現能力，例えば，曖昧さの程度（無曖昧，有限曖昧，多項式的曖昧など）が表現能力に及ぼす影響等について考察を行う．関連する既存研究として，重み付きオートマトンおよび重み付き木オートマトンについて，上述のような曖昧さの程度に基づく表現能力の階層性が示されている．階層性の証明には各クラスに対するポンプ補題が用いられる．WMCFGの部分クラスに対してもこの種のポンプ補題を証明することにより，曖昧さの程度に基づく部分クラスの階層性が証明できると予想している．
|
Research Products
(7 results)
