| Project/Area Number |
23K19959
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
1001:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
DO CanhMinh 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00981143)
|
|---|
| Project Period (FY) |
2023-08-31 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2023: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | model checking / temporal properties / a tableau-based approach / state space explosion / parallelization / Maude |
|---|
| Outline of Research at the Start |
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.
|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
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.
|
| Strategy for Future Research Activity |
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.
|
