2023 Fiscal Year Research-status Report
Software Verification Based on the Theory of Transducers
| Project/Area Number |
19K11899
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2019-04-01 – 2025-03-31
|
| Keywords | ソフトウェア検証 / トランスデューサ / 形式言語 |
|---|
| 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セミナーに招待されているので，これまでの研究成果について海外の多くの研究者と議論し，されなる研究の進展に努める．
|
| Causes of Carryover |
当初の研究期間のうち３年間は，新型コロナウイルスの感染拡大のため，国際会議，国内会議の多くがオンライン開催になり出張の機会が大きく減ったため，少額の次年度使用額が生じた．次年度使用額は主に成果発表の旅費に使用する予定である．
|
