Mathematical foundations for the reconfiguration paradigm
| 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 2022)
|
| 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 | reconfiguration paradigm / hybrid logics / dynamic logics / stratified institutions / interpolation / Robinson Consistency / omitting types theorem / hybrid logic / dynamic logic / institution / forcing / 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 Annual Research Achievements |
In the final year of the present project, we proved a Robinson Consistency Property for a large class of hybrid-dynamic logics. In classical first-order logic, Robinson's Consistency Theorem was a historical forerunner of Craig's celebrated Interpolation Theorem, to which it is equivalent. In the context of first-order logic, it is known since Lindstrom's work that in the presence of compactness, the Robinson Consistency Property is a consequence of the Omitting Types Theorem. Following in Lindstrom's footsteps, we used an Omitting Types Theorem for many-sorted hybrid-dynamic first-order logics established in the previous year of the present project to obtain a Robinson Consistency Theorem. An important corollary of this result is interpolation, which is a logical property that mostly deal with combining and decomposing theories. The reason for the interest in interpolation is the fact that it is the source of many other results. For structured specifications and formal methods, interpolation ensures a good compositional behavior of module semantics.
Throughout the entire research period dedicated to the present project, we set the foundations for the formal specification and verification of reconfigurable systems. The knowledge on hybrid-dynamic logics -- recognized as suitable for describing and reasoning about systems with reconfigurable features -- was developed uniformly at an abstract level provided by the category-based definition of stratified institution.
|
Report
(3 results)
Research Products
(18 results)
