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

2022 Fiscal Year Annual Research Report

Network of automata with data based on compositional active learning

Research Project

Project/Area Number 21H03415
Allocation TypeSingle-year Grants
Research InstitutionNagoya University

Principal Investigator

結縁 祥治  名古屋大学, 情報学研究科, 教授 (70230612)

Co-Investigator(Kenkyū-buntansha) 小川 瑞史  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
今井 敬吾  岐阜大学, 工学部, 助教 (70456630)
関 浩之  名古屋大学, 情報学研究科, 教授 (80196948)
中澤 巧爾  名古屋大学, 情報学研究科, 准教授 (80362581)
Project Period (FY) 2021-04-01 – 2026-03-31
Keywordsイベントクロックオートマトン / アクティブ学習アルゴリズム / 分割検証 / Assume-Gurantee / SMTソルバー / 到達可能性解析
Outline of Annual Research Achievements

本年度は,時間経過モデルに対して可逆計算の概念を導入したモデルについても検討を開始した.時間経過モデルは,複数のコンポーネントが同期をする際に通信を行わず,互いに持つクロックの差分によって同期を可能にする.しかし,設計の際に時間経過による同期が想定した組み合わせにならない場合は,デッドロックや予定外の振舞いをすることになる.可逆計算を並行計算モデルに適用した場合には,実行時の依存関係を記録して,不具合が発生したときにどの依存関係が設計時に想定した正しさに適合しないかをチェックすることができる.この概念に基づいて時間経過モデルを拡張し,並行計算の基本モデルを提案した.このモデルの導入は当初の研究計画にはないが,より精密に振舞い解析を可能にするモデルの候補として研究を行うこととした.可逆モデルの導入は,より詳細な意味論の展開を可能とするものであるが時間経過に可逆性を取り込む場合の検証方法については十分でなく,ソフトウェアの検証へ応用するためにはより研究が必要であることがわかった.
海外の時間経過モデルおよび可逆計算モデルの研究者と共同して国際会議発表を行い,基本的なモデルについて通信プロセスの枠組みで新たな形式モデルを提案することができた.これに関連して,可逆計算モデルに基づくデバッグ手法に関する研究を行い,試験的な実現について研究を実施し,国際会議に発表を行った.
この他,従来から継続している時間経過モデルについて,イベントクロックモデル,プッシュダウンオートマトンによるモデルについて研究を行うとともに,分担者によって木オートマトンのアクティブ学習についての研究を実施した.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本年度は,可逆計算の概念を導入したモデルについて研究を実施した.このモデルでは並行システムが実行環境に応じて非決定的に動作することによって動的に変化する依存関係を計算の意味として保存する.本研究の振舞い合成において時間による相互採用は動的に変化する依存関係そのものであることから,可逆計算モデルを導入することによってより精密な解析が可能となることの知見を得た.このアイデアに基づいて,当初計画をより拡張してすすめることが可能になることが予想できる.並行システムにおいて最も複雑となる依存関係を定式化することで,新たなデバッグ手法を提案することでソフトウェアの信頼性を向上させる技法について見通しが得られた.
ゾーン解析による時間経過による振舞いの離散的モデル化による到達可能性解析について,シミュレーション関係にも基づいた決定可能性について検討を行っている.ここでは,ソフトウェアモデルとして入れ子構造を持つ計算モデル(Nested Timed Automata)を対象とし,新たな観点で決定可能性について証明を与えるとともに,アクティブ学習への応用についての基本的な調査を行っている.

Strategy for Future Research Activity

今後は,当初の計画のなかでアクティブ学習の枠組みについて重点をおいて研究をすすめる計画である.可逆計算に基づく実行意味は非常に有用であることから,誤差解析への応用を検討するとともに,アクティブ学習への応用手法について研究をすすめる.時間経過に関する振舞いにおけるタイマーについての対称性を導入するために,イベントクロックオートマトンでイベント予測クロックによる振舞いのアクティブ学習について研究する.イベント記録クロックにたいするアクティブ学習についてはすでに研究されているが,イベント予測クロックについては,右合同性がナイーブには成り立たないことからその学習は直感的でない.イベント予測クロックは無限の同値類を導入することが知られており,一定の仮定を新たに設定することでアクティブ学習を可能にする方法について研究を進める.イベント予測クロックは可逆通信プロセスにおいても重要な役割をすることが予測され,可逆通信プロセス計算の研究に対しても有用である.この他,時間プッシュオートマトンの拡張体系であるNeTAの到達可能性についても研究を進める.

  • Research Products

    (7 results)

All 2022 Other

All Int'l Joint Research (1 results) Journal Article (4 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 4 results) Presentation (2 results) (of which Int'l Joint Research: 2 results)

  • [Int'l Joint Research] University of Urbino(イタリア)

    • Country Name
      ITALY
    • Counterpart Institution
      University of Urbino
  • [Journal Article] The Reversible Temporal Process Language2022

    • Author(s)
      Bocchi Laura、Lanese Ivan、Mezzina Claudio Antares、Yuen Shoji
    • Journal Title

      FORTE 2022, Lecture Notes in Computer Science

      Volume: 13273 Pages: 31~49

    • DOI

      10.1007/978-3-031-08679-3_3

    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Reversible Debugger for Imperative Parallel Programs with Contracts2022

    • Author(s)
      Ikeda Takashi、Yuen Shoji
    • Journal Title

      RC2022, Lecture Notes in Computer Science

      Volume: 13354 Pages: 204~212

    • DOI

      10.1007/978-3-031-09005-9_14

    • Peer Reviewed
  • [Journal Article] Active Learning for Deterministic Bottom-Up Nominal Tree Automata2022

    • Author(s)
      Nakanishi Rindo、Takata Yoshiaki、Seki Hiroyuki
    • Journal Title

      ICTAC 2022, Lecture Notes in Computer Science

      Volume: 13572 Pages: 342~359

    • DOI

      10.1007/978-3-031-17715-6_22

    • Peer Reviewed
  • [Journal Article] On the?Determinization of?Event-Clock Input-Driven Pushdown Automata2022

    • Author(s)
      Ogawa Mizuhito、Okhotin Alexander
    • Journal Title

      CSR 2022. Lecture Notes in Computer Science

      Volume: 13296 Pages: 256~268

    • DOI

      10.1007/978-3-031-09574-0_16

    • Peer Reviewed / Int'l Joint Research
  • [Presentation] The Reversible Temporal Process Language2022

    • Author(s)
      Bocchi Laura、Lanese Ivan、Mezzina Claudio Antares、Yuen Shoji
    • Organizer
      FORTE 2022
    • Int'l Joint Research
  • [Presentation] A Reversible Debugger for Imperative Parallel Programs with Contracts2022

    • Author(s)
      Ikeda Takashi、Yuen Shoji
    • Organizer
      Reversibile Computation 2022
    • Int'l Joint Research

URL: 

Published: 2023-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi