| 研究課題/領域番号 |
21H03415
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| 研究分担者 |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2026-03-31
|
| キーワード | イベントクロックオートマトン / アクティブ学習アルゴリズム / 分割検証 / Assume-Gurantee / SMTソルバー / 到達可能性解析 |
|---|
| 研究実績の概要 |
本年度は，時間経過モデルに対して可逆計算の概念を導入したモデルについても検討を開始した．時間経過モデルは，複数のコンポーネントが同期をする際に通信を行わず，互いに持つクロックの差分によって同期を可能にする．しかし，設計の際に時間経過による同期が想定した組み合わせにならない場合は，デッドロックや予定外の振舞いをすることになる．可逆計算を並行計算モデルに適用した場合には，実行時の依存関係を記録して，不具合が発生したときにどの依存関係が設計時に想定した正しさに適合しないかをチェックすることができる．この概念に基づいて時間経過モデルを拡張し，並行計算の基本モデルを提案した．このモデルの導入は当初の研究計画にはないが，より精密に振舞い解析を可能にするモデルの候補として研究を行うこととした．可逆モデルの導入は，より詳細な意味論の展開を可能とするものであるが時間経過に可逆性を取り込む場合の検証方法については十分でなく，ソフトウェアの検証へ応用するためにはより研究が必要であることがわかった．
海外の時間経過モデルおよび可逆計算モデルの研究者と共同して国際会議発表を行い，基本的なモデルについて通信プロセスの枠組みで新たな形式モデルを提案することができた．これに関連して，可逆計算モデルに基づくデバッグ手法に関する研究を行い，試験的な実現について研究を実施し，国際会議に発表を行った．
この他，従来から継続している時間経過モデルについて，イベントクロックモデル，プッシュダウンオートマトンによるモデルについて研究を行うとともに，分担者によって木オートマトンのアクティブ学習についての研究を実施した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度は，可逆計算の概念を導入したモデルについて研究を実施した．このモデルでは並行システムが実行環境に応じて非決定的に動作することによって動的に変化する依存関係を計算の意味として保存する．本研究の振舞い合成において時間による相互採用は動的に変化する依存関係そのものであることから，可逆計算モデルを導入することによってより精密な解析が可能となることの知見を得た．このアイデアに基づいて，当初計画をより拡張してすすめることが可能になることが予想できる．並行システムにおいて最も複雑となる依存関係を定式化することで，新たなデバッグ手法を提案することでソフトウェアの信頼性を向上させる技法について見通しが得られた．
ゾーン解析による時間経過による振舞いの離散的モデル化による到達可能性解析について，シミュレーション関係にも基づいた決定可能性について検討を行っている．ここでは，ソフトウェアモデルとして入れ子構造を持つ計算モデル(Nested Timed Automata)を対象とし，新たな観点で決定可能性について証明を与えるとともに，アクティブ学習への応用についての基本的な調査を行っている．
|
| 今後の研究の推進方策 |
今後は，当初の計画のなかでアクティブ学習の枠組みについて重点をおいて研究をすすめる計画である．可逆計算に基づく実行意味は非常に有用であることから，誤差解析への応用を検討するとともに，アクティブ学習への応用手法について研究をすすめる．時間経過に関する振舞いにおけるタイマーについての対称性を導入するために，イベントクロックオートマトンでイベント予測クロックによる振舞いのアクティブ学習について研究する．イベント記録クロックにたいするアクティブ学習についてはすでに研究されているが，イベント予測クロックについては，右合同性がナイーブには成り立たないことからその学習は直感的でない．イベント予測クロックは無限の同値類を導入することが知られており，一定の仮定を新たに設定することでアクティブ学習を可能にする方法について研究を進める．イベント予測クロックは可逆通信プロセスにおいても重要な役割をすることが予測され，可逆通信プロセス計算の研究に対しても有用である．この他，時間プッシュオートマトンの拡張体系であるNeTAの到達可能性についても研究を進める．
|
