| 研究課題/領域番号 |
20K03718
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| 研究分担者 |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
中途終了 (2022年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2023年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2022年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2021年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2020年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 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 |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
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.
|
