Development of a model-checking method for actor-based multi-threaded recursive programs

Research Project

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機械と等価となってしまう．本研究では，オートマトンと形式文法に関する知見を活用し，検証可能性を失わずに並行再帰プログラムのためのモデルを構築することを目指す．