2021 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 – 2023-03-31
|
| Keywords | ソフトウェア検証 / トランスデューサ / 形式言語 / 文字列制約 |
|---|
| Outline of Annual Research Achievements |
本年度には，以下の研究を行なった．
＊文字列を操作するプログラムの検証の基盤となる直線形式文字列制約の充足可能性判定の応用に関する研究を行なった．前年度までの研究成果で整数引数を持つ文字列演算，文字列から整数への演算などを制約で扱えるようになっており，ポンプ補題を用いた言語の非正規性の半自動判定への応用を考えた．ポンプする形の言語を文字列制約として与え，補題の適用に必要となる条件の確認を文字列制約の充足可能性判定で行う．ポンプ補題の中に現れる文字列の分割などは，整数引数を用いた文字列演算で素直に表すことができたが，ポンプする形の言語の無限性判定には自然数に関する全称限量子が先頭に現れる文字列制約の充足可能性判定が必要となり，充足可能性判定器の拡張を行なった．
＊ 拡張正規表現マッチングの計算量解析の研究を継続した．後方参照を含む正規表現の解析の精度を改善するため，集合と木のモナドを組み合わせたモナドを用いるアプローチについて研究を進め，解析の後半部分に非決定性文字列-木トランスデューサの出力増加率解析が適用できることが分かった．
＊ 先読み付き文脈自由文法は文脈自由文法と解析表現文法（PEG）の両方を拡張したものであり，否定先読みが重要な役割を果たす．前年度の研究では，空集合からの極限をとることで言語を定義してたが，意味が未定義になる場合があり，標準形への変換などが難しいという問題があった．この問題を解決するため，否定を含む論理プログラムにおいて Fitting Semantics と呼ばれる意味論を参考にし，未定義を表す値を持つ３値論理に基づく意味論を構築した．
|
| 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 |
文字列制約の充足可能性判定については一定の成果が得られたため，リスト（無限アルファベット上の文字列），無限長の文字列，木などの制約への拡張を検討する．正規表現マッチングの計算量解析については，非決定性文字列-木トランスデューサの既存の増加率判定手続きを整理し，より実装に向いた手続きの構築を目指す．
|
| Causes of Carryover |
新型コロナウイルスの感染拡大のため，9月に予定していた国際会議での発表がオンライン開催になり，国内の研究集会もオンライン開催になったため，次年度使用額が生じた．コロナの状況の改善が見込めるため，次年度使用額は国内外の研究者との交流を促進するために使用する予定である．
|
Research Products
(7 results)
