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

2021 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

本年度は,本研究遂行に必要となる従来から時間および論理における証明に関して行ってきた発展を中心に研究を実施した.イベントクロックに対する性質を示した他,論理学におけるカット除去に関する研究を行った.オートマトンに重み付けを導入関する研究など,本研究で対象とする拡張オートマトンについての研究を実施した.新型コロナウィルスによる出張の制限から一部の出張等が制限されたため,共同研究は今後の研究遂行に必要となる分担者個々のテーマを深めることを中心に実施した.
研究概要の観点からの本年の研究実績は以下のとおりである.
①振る舞いの合成に基づく分割検証:時間システムに対する分割検証を自動的に行うための仮説学習アルゴリズムを示した.分割検証手法の一つであるAssume-Guarantee Reasoning(AGR)において複数のコンポーネントが全体として目的の性質を満たすかどうかを, 個々のコンポーネントが性質に違反することなく仮説と正しく相互に作用するかどうかを確認することで検証する. レジスタオートマトンの学習アルゴリズムであるSL*アルゴリズムを時間システムに適用し, Event-recording automata(ERA)をモデルとした仮説学習を実現した.
②振る舞い頑健性:振る舞いの頑健性については,時間オートマトンの到達可能性を論理式によって表現し,到達可能であること論理式が充足可能となることが同値である論理式を構成する.論理式にクロックを表現する変数を導入して,到達可能性をSMTソルバーによってチェックする手法を示した.クロックに対して誤差をあらわす変数を導入して機械的にチェックする方法を示した.

Current Status of Research Progress
Current Status of Research Progress

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

Reason

本年度は新型コロナの影響から出張や学会発表が制限によって,計画どおりの出張,研究打ち合わせの実施が難しかったため,今後の研究に必要な課題を各自で実施することとなった.初年度であることもあり,今後の研究実施のための研究は実施できたと考えている.
本年度の研究は基本的な予備的調査・実験であり,予想されたものである.

Strategy for Future Research Activity

ひきつづいて時間経過を含めたモデルにもとづいたソフトウェア解析について研究を行う。ゾーンに基づく時間モデルの到達可能性解析と可逆計算モデルに時間経過を導入したプログラムのモデル化にとりくむ。さらに、プッシュダウンを持つオートマトンについてActive Learningについての研究をすすめる。これらの研究にもとづいて高い信頼性をもつ実時間並行プログラムのモデル化についての研究をすすめる。得られた知見に基づいてより効率的で新たな手法を提案することを研究の方針とする.

  • Research Products

    (5 results)

All 2022 2021

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

  • [Journal Article] Kmclib: Automated Inference and Verification of Session Types from OCaml Programs2022

    • Author(s)
      Imai Keigo、Lange Julien、Neykova Rumyana
    • Journal Title

      TACAS 2022

      Volume: LNCS 13243 Pages: 379~386

    • DOI

      10.1007/978-3-030-99524-9_20

    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] LTL Model Checking for Register Pushdown Systems2021

    • Author(s)
      SENDA Ryoma、TAKATA Yoshiaki、SEKI Hiroyuki
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E104.D Pages: 2131~2144

    • DOI

      10.1587/transinf.2020EDP7265

    • Peer Reviewed / Open Access
  • [Journal Article] Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions2021

    • Author(s)
      Saotome, Kenji ; Nakazawa, Koji ; Kimura, Daisuke
    • Journal Title

      6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021,

      Volume: LIPIcs 195 Pages: 11:1--11:14

    • DOI

      10.4230/LIPIcs.FSCD.2021.11

    • Peer Reviewed / Open Access
  • [Presentation] ツリークエリを用いた時間システムの分割検証のための仮説学習2022

    • Author(s)
      新美航太郎・結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会
  • [Presentation] 充足可能性判定を利用した実現可能な時間オートマトンの検証2022

    • Author(s)
      城 聖一郎・結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会

URL: 

Published: 2023-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi