| 講演名 | 2022-03-07 ツリークエリを用いた時間システムの分割検証のための仮説学習 新美 航太郎(名大), 結縁 祥治(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本研究では時間システムに対する分割検証を自動的に行うための仮説学習アルゴリズムを示す. 分割検証手法の一つであるAssume-Guarantee Reasoning(AGR)を対象とする. AGRは複数のコンポーネントが全体として目的の性質を満たすかどうかを, 個々のコンポーネントが性質に違反することなく仮説と正しく相互に作用するかどうかを確認することで検証する. AGRのための仮説学習アルゴリズムは, AngluinのL*アルゴリズムを用いてCobleighらによって非時間システムに対して提唱され, その後Linらによって時間システムに対して拡張された. 本研究はレジスタオートマトンの学習アルゴリズムであるSL*アルゴリズムを時間システムに適用し, Event-recording automata(ERA)をモデルとした仮説学習を実現する. 我々の仮説学習アルゴリズムはツリークエリを用いて対象となるERAの観測表を構築する. 本研究では時間システムの分割検証のための仮説学習手法を示す. 我々のアルゴリズムで学習される仮説は, コンポーネントに出現する全てのイベントクロックを含む. 我々のアルゴリズムは時間制約をよりわかりやすく扱うことができる. |
| 抄録(英) | This paper presents an automatic assumption-learning for compositional verification of timed systems. We focus on Assume-Guarantee Reasoning (AGR), one of the compositional verification methods. AGR checks whether multiple components satisfy the property as a whole by checking whether the individual components interact correctly with the assumption without violating the desired property. Assumption learning algorithms for AGR have been proposed by Cobleigh et al. using Angluin’s L* algorithm and further extended to timed systems by Lin et al. We apply the SL* algorithm for register automata to timed systems modelled by Event-recording automata(ERA). Our assumption-learning uses tree queries to construct an observation table for the assumption ERA instead of guarded words. Our assumption includes actions to reset clocks. This enables to learn assumption ERA by a single loop and make the algorithm simpler. |
| キーワード(和) | 分割検証 / 時間システム / ツリークエリ |
| キーワード(英) | Compositional verification / Timed systems / Tree query |
| 資料番号 | SS2021-49 |
| 発行日 | 2022-02-28 (SS) |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2022/3/7(から2日開催) |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | ソフトウェアサイエンスおよび一般 |
| テーマ（英） | Software Science etc. |
| 委員長氏名（和） | 小林 隆志(東工大) |
| 委員長氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) |
| 副委員長氏名（和） | 岡野 浩三(信州大) |
| 副委員長氏名（英） | Kozo Okano(Shinshu Univ.) |
| 幹事氏名（和） | 島 和之(広島市大) / 林 晋平(東工大) |
| 幹事氏名（英） | Kazuyuki Shima(Hiroshima City Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| 幹事補佐氏名（和） | 小形 真平(信州大) |
| 幹事補佐氏名（英） | Shinpei Ogata(Shinshu Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | ツリークエリを用いた時間システムの分割検証のための仮説学習 |
| サブタイトル（和） | |
| タイトル（英） | Learning Assumptions for Compositional Verification of Timed Systems with Tree Queries |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 分割検証 / Compositional verification |
| キーワード(2)（和/英） | 時間システム / Timed systems |
| キーワード(3)（和/英） | ツリークエリ / Tree query |
| 第 1 著者 氏名（和/英） | 新美 航太郎 / Kotaro Niimi |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ) |
| 第 2 著者 氏名（和/英） | 結縁 祥治 / Shoji Yuen |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ) |
| 発表年月日 | 2022-03-07 |
| 資料番号 | SS2021-49 |
| 巻番号（vol） | vol.121 |
| 号番号（no） | SS-416 |
| ページ範囲 | pp.43-48(SS), |
| ページ数 | 6 |
| 発行日 | 2022-02-28 (SS) |