Network of automata with data based on compositional active learning

点击翻译按钮获取中文摘要

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