Computational complexity and practice of verified and efficient algorithms for dynamical systems
| Project/Area Number |
20K19744
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
THIES HOLGER 九州大学, システム情報科学研究院, 助教 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2020)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 / Computable analysis / Differential equations / Verification / Formal proofs / Complexity Theory |
|---|
| Outline of Research at the Start |
The research project aims to get insights into the computational complexity of problems in the physical world and to provide efficient and formally verified algorithms for computations that involve real numbers. Such algorithms lead to better, more reliable and reusable software.
|
| Outline of Annual Research Achievements |
The goal of this project is to work towards the verification of efficient algorithms for solving ordinary differential equations based on the computational model of computable analysis. This year's focus was on using the Coq proof assistant to develop the underlying theory.
Several new results could be obtained. Previous theoretical results on the formalziation of the model have been extended and summarized in a journal publication to appear in LMCS. Additional theoretical results regarding descriptions of partial functions and machine models could be obtained and published in the conference proceedings of MFCS.Progress was also made with regards to more practical work on the formalization of algorithms for exact real computation in Coq.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Several new theoretical and practical results could be obtained. In particular, progress on the formalization of exact real computation went more smoothly than originally expected. The work has lead to one journal publication and two conference publications in highly rated venues. Additionally, some results were presented as talks in smaller conferences and workshops.
Still, some difficulties arose because of the spread of the novel corona virus and the resulting challenges for international collaboration. While many things could be organized online, time differences and technical limitations made long and thoroughful discussions difficult.
|
| Strategy for Future Research Activity |
The results obtained in the current year will be extended to solving ordinary differential equations with analytic right hand side. This makes it necessary to also formalize some classical mathematical results about power series and ODEs. Further, some recent progress has been made on complexity theoretical results for partial differential equations. It is planned to use these results as basis for an implementation in exact real computation for certain types of PDEs and to further extend the results to other types of PDEs. Finally, it is also planned to compare the formalization results in Coq with work in other proof assistants such as the Minlog and IFP proof assistants.
|
Report
(1 results)
Research Products
(6 results)
