| Project/Area Number |
20K03718
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
Gaina Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Discontinued (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2023: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,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 | hybrid logic / dynamic logic / institution / forcing / completeness / compactness / omitting types / interpolation / reconfiguration paradigm / hybrid logics / dynamic logics / stratified institutions / Robinson Consistency / omitting types theorem / model theory / proof theory / algebraic specification / universal logic |
|---|
| Outline of Research at the Start |
Very often the operation of reconfigurable systems is safety-critical: any malfunction may result in the serious injury to people. The safety requirements can be fulfilled only by applying formal methods. The purpose of this project is to provide a solid logic-based foundation for developing a formal method to describe reconfigurable systems and to reason formally about their properties.
|
| Outline of Final Research Achievements |
Hybrid-dynamic logics are recognized as suitable for describing systems with reconfigurable features and reasoning about their properties. The project developed a mathematical foundation for the formal specification and verification of reconfigurable systems through a unified study of hybrid-dynamic logics. The results were developed within an abstract framework provided by the category-based definition of stratified institutions. The project centered on two main research directions:
(1) We investigated the model-theoretic properties of relatively unconventional (and therefore not well-studied) hybrid-dynamic logics, and
(2) We provided proof-theoretic results such as completeness for hybrid-dynamic logics.
|
| Academic Significance and Societal Importance of the Research Achievements |
We are witnessing a proliferation of software-driven devices that often exhibit reconfigurable features. The operation of such devices is safety-critical, necessitating rigorous development assisted by formal methods. This project set the foundation for such formal methods.
|
