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

Formalization of the decidability of the reachability problem for vector addition systems

Research Project

Project/Area Number 18K11154
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionChiba University

Principal Investigator

Yamamoto Mitsuharu  千葉大学, 大学院理学研究院, 教授 (00291295)

Project Period (FY) 2018-04-01 – 2024-03-31
Project Status Completed (Fiscal Year 2023)
Budget Amount *help
¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Fiscal Year 2022: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2021: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2020: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2019: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Keywords定理証明支援系 / 形式化 / ベクトル加算系 / 到達可能性 / ペトリネット
Outline of Final Research Achievements

We have formalized several problems around reachability for vector addition systems or their equivalent state transition systems. Concretely, boundedness and termination for Petri nets, and reachability-preserving transformation from a vector addition system with states to a vector addition system are formalized. Although formalization of the decidability of the reachability problem for vector addition systems could not be completed, some insight into promising approach to formalization is obtained by investigating several methods for proving the decidability.

Academic Significance and Societal Importance of the Research Achievements

定理証明支援系を用いた形式化によって、機械的に検査された正しい証明が得られるだけでなく、一旦完了した証明に対する試行錯誤や適切な抽象化の検討がしやすくなる。本研究の成果の一部である状態付きベクトル加算系からベクトル加算系への変換の形式化においても、適切な抽象化を行うことで元の証明に用いられていた変換が改良された。
また、形式化の過程で構築・蓄積された技術やノウハウは、後に別の定理を形式的に証明する際の道具として生かされる。上記の変換の形式化においてもベクトルの回転に関するライブラリが整備された。

Report

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

    (7 results)

All 2024 2023 2019 2018 Other

All Presentation (6 results) Remarks (1 results)

  • [Presentation] Coq/SSReflect/MathCompを用いたVASSからVASへの変換の形式化2024

    • Author(s)
      脇坂 勝大, 山本 光晴
    • Organizer
      第26回プログラミングおよびプログラミング言語ワークショップ(PPL 2024)
    • Related Report
      2023 Annual Research Report
  • [Presentation] VASSからVASへの変換のMathCompによる形式化2023

    • Author(s)
      脇坂 勝大, 山本 光晴
    • Organizer
      日本ソフトウェア科学会第40回大会
    • Related Report
      2023 Annual Research Report
  • [Presentation] VASSからVASへの変換の形式化2023

    • Author(s)
      脇坂 勝大, 山本 光晴
    • Organizer
      The 19th Theorem Proving and Provers meeting (TPP 2023)
    • Related Report
      2023 Annual Research Report
  • [Presentation] ペトリネットにおける停止性判定の形式化2019

    • Author(s)
      稲垣 衛, 山本 光晴
    • Organizer
      The 15th Theorem Proving and Provers meeting (TPP 2019)
    • Related Report
      2019 Research-status Report
  • [Presentation] ペトリネットにおける有界性に関する性質のCoq/SSReflectによる形式化2019

    • Author(s)
      稲垣 衛, 山本 光晴
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019)
    • Related Report
      2018 Research-status Report
  • [Presentation] ペトリネットにおける有界性判定の形式化2018

    • Author(s)
      稲垣 衛, 山本 光晴
    • Organizer
      The 14th Theorem Proving and Provers meeting (TPP 2018)
    • Related Report
      2018 Research-status Report
  • [Remarks] ペトリネット上のKarp-Miller木に関するCoq/SSReflectによる形式化のリポジトリ

    • URL

      https://bitbucket.org/mituharu/karpmiller

    • Related Report
      2019 Research-status Report

URL: 

Published: 2018-04-23   Modified: 2025-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi