| Project/Area Number |
24K14901
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kochi University of Technology |
|---|
Principal Investigator |
高田 喜朗 高知工科大学, 情報学群, 教授 (60294279)
|
|---|
| Project Period (FY) |
2024-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | モデル検査 / オートマトン / 形式モデル / 並行再帰プログラム / アクターモデル |
|---|
| Outline of Research at the Start |
プログラミング言語Erlangで採用されているアクターモデル型の並行再帰プログラムの表現に適した形式モデル，及びそのモデル検査法を開発する．プッシュダウンシステム (PDS) 等の無限状態モデルに対するモデル検査法の研究は近年注目されるようになってきたが，複数のスタックを持つPDSはTuring機械と等価となってしまう．本研究では，オートマトンと形式文法に関する知見を活用し，検証可能性を失わずに並行再帰プログラムのためのモデルを構築することを目指す．
|
| Outline of Annual Research Achievements |
並行再帰プログラムの表現に適した形式モデル，及びそのモデル検査法について，主にオートマトン理論に基づいて研究を行っている．
プッシュダウンシステム (PDS) 等の無限状態モデルに対するモデル検査法の研究は近年注目されるようになってきたが，複数のスタックを持つPDSはTuring機械と等価となってしまい，検証可能性が失われる．
検証可能性を保ったまま無限状態を扱える計算モデルの一つとして，レジスタオートマトン，レジスタプッシュダウンシステム等のレジスタ付き計算モデルがある．筆者らは過去にレジスタプッシュダウンシステムのモデル検査法について研究したが，検査項目を記述するための表現方法は通常の線形時相論理式 (Linear Temporal Logic, LTL) としていた．システムモデルだけでなく検査項目も，レジスタ付きモデルに相当する凍結演算子付き時相論理式で表現することで，モデル検査法を拡張できると考えられる．しかし，既存の凍結演算子付き線形時相論理は表現能力が小さい一方，その拡張の凍結演算子付き様相μ計算は表現能力が大き過ぎてモデル検査に応用するのは不向きだった．そこでそれらの中間として，凍結演算子付き選言的様相μ計算を提案し，その表現能力がBuchiレジスタオートマトンと等価であることを証明した．レジスタオートマトンもBuchiレジスタオートマトンも言語の否定演算と積集合演算について閉じていないことからヒントを得て，凍結演算子付き選言的様相μ計算は，否定演算子と積集合演算子の使用を制限した論理体系として設計されている．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究目的はアクターモデル型並行再帰プログラムの検証法の開発であるが，現時点の成果は無限状態モデルに対するオートマトンベースのモデル検査法の基礎研究であり，レジスタ付き計算モデルをどのようにアクターモデル型並行再帰プログラムの検証に当てはめていくかまだ未定である．
|
| Strategy for Future Research Activity |
プログラミング言語Erlangで採用されているアクターモデル型並行再帰機構の形式モデル化を中心に検討する．レジスタ付き計算モデルにこだわらず，第一段階として有限状態モデルによるモデル化や通常のプッシュダウンシステムによるモデル化を経由して，適切な計算モデルの開発につなげたい．
|
