| 研究課題/領域番号 |
21H03415
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| 研究分担者 |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2026-03-31
|
| キーワード | イベントクロックオートマトン / アクティブ学習アルゴリズム / 分割検証 / Assume-Gurantee / SMTソルバー / 到達可能性解析 |
|---|
| 研究実績の概要 |
本年度は，本研究遂行に必要となる従来から時間および論理における証明に関して行ってきた発展を中心に研究を実施した．イベントクロックに対する性質を示した他，論理学におけるカット除去に関する研究を行った．オートマトンに重み付けを導入関する研究など，本研究で対象とする拡張オートマトンについての研究を実施した．新型コロナウィルスによる出張の制限から一部の出張等が制限されたため，共同研究は今後の研究遂行に必要となる分担者個々のテーマを深めることを中心に実施した．
研究概要の観点からの本年の研究実績は以下のとおりである．
①振る舞いの合成に基づく分割検証：時間システムに対する分割検証を自動的に行うための仮説学習アルゴリズムを示した．分割検証手法の一つであるAssume-Guarantee Reasoning(AGR)において複数のコンポーネントが全体として目的の性質を満たすかどうかを, 個々のコンポーネントが性質に違反することなく仮説と正しく相互に作用するかどうかを確認することで検証する. レジスタオートマトンの学習アルゴリズムであるSL*アルゴリズムを時間システムに適用し, Event-recording automata(ERA)をモデルとした仮説学習を実現した．
②振る舞い頑健性：振る舞いの頑健性については，時間オートマトンの到達可能性を論理式によって表現し，到達可能であること論理式が充足可能となることが同値である論理式を構成する．論理式にクロックを表現する変数を導入して，到達可能性をSMTソルバーによってチェックする手法を示した．クロックに対して誤差をあらわす変数を導入して機械的にチェックする方法を示した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度は新型コロナの影響から出張や学会発表が制限によって，計画どおりの出張，研究打ち合わせの実施が難しかったため，今後の研究に必要な課題を各自で実施することとなった．初年度であることもあり，今後の研究実施のための研究は実施できたと考えている．
本年度の研究は基本的な予備的調査・実験であり，予想されたものである．
|
| 今後の研究の推進方策 |
ひきつづいて時間経過を含めたモデルにもとづいたソフトウェア解析について研究を行う。ゾーンに基づく時間モデルの到達可能性解析と可逆計算モデルに時間経過を導入したプログラムのモデル化にとりくむ。さらに、プッシュダウンを持つオートマトンについてActive Learningについての研究をすすめる。これらの研究にもとづいて高い信頼性をもつ実時間並行プログラムのモデル化についての研究をすすめる。得られた知見に基づいてより効率的で新たな手法を提案することを研究の方針とする．
|
