Mathematical foundations for the reconfiguration paradigm

2023 Fiscal Year Final Research Report

• 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
• Keywords: hybrid logic / dynamic logic / institution / forcing / completeness / compactness / omitting types / interpolation

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.

Free Research Field

logic, category theory, formal methods

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.