| Project/Area Number |
19K11899
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2019-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2022: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | ソフトウェア検証 / トランスデューサ / 形式言語 / 文字列制約 / オートマトン / 形式言語理論 |
|---|
| Outline of Research at the Start |
ソフトウェア検証の基盤となる理論として，これまで主に出力を持たないオートマトンなどの計算モデルが用いられてきたが，ソフトウェア検証において出力を持つ計算モデルすなわちトランスデューサの理論が重要になってきている. 本研究はトランスデューサとその拡張のソフトウェア検証への応用を進め，検証精度の向上，検証で扱えるプログラムの性質の拡張などにおいてソフトウェア検証の深化を目指す．特に，以下の３つの課題に取り組む：トランスデューサを含む文字列制約の充足可能性判定手続き，木トランスデューサ理論に基づくプログラムの時間計算量解析，ウェブブラウザにおけるセキュリティ対策機構のトランスデューサを用いた検証．
|
| Outline of Annual Research Achievements |
本年度には，トランスデューサ理論に基づく正規表現マッチングの計算量解析の研究を継続するとともに，関連する理論の研究を行なった．
＊ 後方参照を含む拡張正規表現マッチングの計算量解析の研究を継続し，二つの方向性の研究を行なった．a）捕捉する正規表現の言語が有限な場合についての研究を行い，正規表現の微分を拡張することで正確な解析が可能であることを示した．また，既存の手法がどのような場合に過大近似になっているか示したことも重要な成果である．b）後方参照が使われる典型的な場合の一つに対するバックトラックに基づくマッチングの計算量が本質的に非線形であることを示した．この問題に対して，文字列照合のための KMP法 とバックトラックに基づくマッチングアルゴリズムを組み合わせたアルゴリズムを提案・実装し，計算量のオーダが改善することを実験で示した．
＊ 後方参照で拡張された正規表現が表す言語を表示的意味論のスタイルで与えた．また，ストリーミング変換器の像としての定義も与え，その等価性を示した．その結果から後方参照で拡張された正規表現の言語クラスがDT0Lの言語クラスの部分クラスであるという結果を得た．
＊ ポストの対応問題の解法を文字列制約に還元する研究を行ってきたが，本年度には，ソフトウェア検証における到達可能性判定を適用する研究を行い，タイルの長さが4，個数を3に制限した場合，難しい数個の場合を除き，判定することに成功した．
＊ トランスデューサ理論によるソフトウェア検証技術の確率的モデル・プログラムへの展開を見据え，確率的高階プログラムの検証の基盤となる理論を証明支援系Isabelle/HOLで形式化する研究を行なった．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
拡張正規表現マッチングの計算量解析においては，2021年度までの研究で先読み付き決定性トランスデューサの出力増加率解析を用いた計算量解析手続きの構築と判定器の実装ができており一定の成果が得られていた．また，2022年度の研究では，後方参照を含む正規表現のについて，非決定性トランスデューサの出力増加率解析を用いることで精度が改善できることを示した．さらに，本年度には，補足する正規表現の言語が有限の場合の研究を行い，更なる精度改善の方向性を示している．
また本年度は，後方参照を含む正規表現が表す言語がDT0L であることを示している．これは，2023年に野上と寺内が示したインデックス言語であるという結果を改善しており，形式言語の理論分野における興味深い結果と言える．
|
| Strategy for Future Research Activity |
延長した2024年度には，これまでの研究成果のうち未発表の部分を論文にまとめる．また，2024年秋に開催される正規表現に関連するDagstuhlセミナーに招待されているので，これまでの研究成果について海外の多くの研究者と議論し，されなる研究の進展に努める．
|
