• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Mathematical foundations for the reconfiguration paradigm

Research Project

Project/Area Number 20K03718
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 12030:Basic mathematics-related
Research InstitutionKyushu 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)
Keywordshybrid 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.

Report

(4 results)
  • 2023 Final Research Report ( PDF )
  • 2022 Annual Research Report
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (18 results)

All 2023 2022 2021 2020 Other

All Int'l Joint Research (3 results) Journal Article (6 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 5 results) Presentation (9 results) (of which Int'l Joint Research: 7 results,  Invited: 1 results)

  • [Int'l Joint Research] The University of Queensland/Historical and Philosophical Inquiry(オーストラリア)

    • Related Report
      2022 Annual Research Report
  • [Int'l Joint Research] Jagiellonian University/Department of Logic(ポーランド)

    • Related Report
      2022 Annual Research Report
  • [Int'l Joint Research] La Trobe University(オーストラリア)

    • Related Report
      2020 Research-status Report
  • [Journal Article] Omitting types theorem in hybrid dynamic first-order logic with rigid symbols2023

    • Author(s)
      GAINA Daniel、BADIA Guillermo、KOWALSKI Tomasz
    • Journal Title

      Annals of Pure and Applied Logic

      Volume: 174 Issue: 3 Pages: 103212-103212

    • DOI

      10.1016/j.apal.2022.103212

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Robinson consistency in many-sorted hybrid first-order logics2022

    • Author(s)
      GAINA Daniel, BADIA Guillermo, KOWALSKI Tomasz
    • Journal Title

      Proceedings of the Advances in Modal Logic, AiML 2022

      Volume: 14 Pages: 407-428

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Lindstrom’s theorem, both syntax and semantics free2021

    • Author(s)
      Gaina Daniel、Kowalski Tomasz
    • Journal Title

      Journal of Logic and Computation

      Volume: First-view Issue: 5 Pages: 1-37

    • DOI

      10.1093/logcom/exab073

    • Related Report
      2021 Research-status Report
  • [Journal Article] Stability of termination and sufficient-completeness under pushouts via amalgamation2020

    • Author(s)
      Gaina Daniel、Nakamura Masaki、Ogata Kazuhiro、Futatsugi Kokichi
    • Journal Title

      Theoretical Computer Science

      Volume: 848 Pages: 82-105

    • DOI

      10.1016/j.tcs.2020.09.024

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Fraisse-Hintikka theorem in institutions2020

    • Author(s)
      Gaina Daniel、Kowalski Tomasz
    • Journal Title

      Journal of Logic and Computation

      Volume: 30 Issue: 7 Pages: 1377-1399

    • DOI

      10.1093/logcom/exaa042

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Forcing and Calculi for Hybrid Logics2020

    • Author(s)
      Gaina Daniel
    • Journal Title

      Journal of the ACM

      Volume: 67 Issue: 4 Pages: 1-55

    • DOI

      10.1145/3400294

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Horn clauses in Hybrid-Dynamic Quantum Logic2023

    • Author(s)
      GAINA Daniel
    • Organizer
      Cracow Logic Conference (CLoCk)
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Stability of termination under pushouts via amalgamation2022

    • Author(s)
      GAINA Daniel
    • Organizer
      Australian and New Zealand Industrial and Applied Mathematics
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Robinson consistency in many-sorted hybrid first-order logics2022

    • Author(s)
      GAINA Daniel
    • Organizer
      Advances in Modal Logic, AiML 2022
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Stability of termination under pushouts via amalgamation2022

    • Author(s)
      Daniel Gaina
    • Organizer
      Australian and New Zealand Industrial and Applied Mathematical Conference (ANZIAM 2022)
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols2021

    • Author(s)
      Daniel Gaina
    • Organizer
      The Australasian Association for Logic Conference
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Stability of termination under pushouts via amalgamation2021

    • Author(s)
      Daniel Gaina
    • Organizer
      31st Seminar on Algebra, Logic and Geometry in Informatics (ALGI 2021)
    • Related Report
      2021 Research-status Report
  • [Presentation] Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols2021

    • Author(s)
      Daniel Gaina
    • Organizer
      Mathematical Society of Japan, Autumn Meeting 2021
    • Related Report
      2021 Research-status Report
  • [Presentation] Forcing and Calculi for Hybrid Logics2020

    • Author(s)
      Daniel Gaina
    • Organizer
      Logic and Geometry in Informatics (ALGI)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Forcing and its applications in hybrid-dynamic logics2020

    • Author(s)
      Daniel Gaina
    • Organizer
      Australasian Logic Group
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2020-04-28   Modified: 2025-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi