| 研究課題/領域番号 |
23K19959
|
|---|
| 研究種目 |
研究活動スタート支援
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
1001:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
DO CanhMinh 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00981143)
|
|---|
| 研究期間 (年度) |
2023-08-31 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
2,860千円 (直接経費: 2,200千円、間接経費: 660千円)
2024年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2023年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | model checking / temporal properties / a tableau-based approach / state space explosion / parallelization / Maude |
|---|
| 研究開始時の研究の概要 |
This research aims to develop a tableau-based approach to effectively model checking temporal properties for large-scale systems. The core idea of our approach is to split the original model checking problem into multiple smaller model checking problems and handle each smaller one independently.
|
| 研究実績の概要 |
I./ Conducted research in accordance with the research plan planned for this fiscal year and achieved the following results:
(1) The applicant has successfully investigated how to construct a tableau for a temporal formula.
(2) Given an infinite sequence and a temporal formula, the applicant has successfully investigated how to divide the sequence into multiple parts based on the result from (1). This paves the road to split the original reachable state space into multiple sub-state spaces using the tableau method.
(3) The applicant has also applied the model checking approach in this research to model check quantum circuits with their desired properties as well.
II./ The applicant presented three papers at FAVPQC 2023 held in Brisbane, Australia that were not planned for this fiscal year.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
This was because, in addition to executing the planned research implementation as scheduled, the applicant could publish the research results as some international workshop papers.
|
| 今後の研究の推進方策 |
The applicant plans to continuously conduct the research as follows:
- Develop a tool that supports the approach.
- Develop a parallel technique/tool based on a master-worker model in which model checking sub-state spaces in the final layer are conducted in parallel.
- Integrate our techniques into some model checkers if time allows.
|
