実現可能性必要条件に基づいた協調的リアクティブシステム自動合成

2017 Fiscal Year Research-status Report

• Project/Area Number: 17K17763
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 冨田 尭 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 助教 (80749226)
• Project Period (FY): 2017-04-01 – 2020-03-31
• Keywords: 自動合成 / 実現可能性 / 協調的リアクティブシステム / 形式手法

Outline of Annual Research Achievements

仕様からのリアクティブシステムの自動合成では，通常，仕様違反させようとする敵対的環境を想定することで，非常に強い信頼性と安全性をもつリアクティブシステムの合成を試みる．しかし現実には，環境とリアクティブシステムの関係は必ずしも敵対的ではなく，協調・共生を前提とすることも多い．本研究では仕様の実現可能性必要条件に基づき協調的リアクティブシステムを自動合成する手法の開発を目的とし，今年度はまず，関連研究の調査と，既知の実現可能性必要条件の特性の詳細な分析及び分類を行った．
その結果，図らずもいくつかの実現可能性必要条件を新たに発見した．具体的には，仕様の充足可能性を保存するという性質である段階的充足可能性及びそれに類する既知必要条件とは別種の，安定状態への到達可能性に関する必要条件群が存在することがわかった．さらに，それらの安定状態到達可能性群と既知段階的充足可能性群の間の対称性，類似性及び相違を分析・整理し，網羅性，保存可能性，安定化可能性及び戦略化可能性の観点から，実現可能性必要条件を体系的・階層的に分類できることを発見した．その上で，それらの実現可能性必要条件群の各判定手続きも開発した．この各判定手続きを利用することで，仕様が実現不能であった際に，これまでより詳細で体系的な原因分析が可能となる．
新たに発見された必要条件は，環境からのある種の協力により安定状態へ到達し仕様を満たすことが可能なリアクティブシステムの構成可能性を示すものである．従って，この新しい必要条件に基づいて環境とリアクティブシステムの間の協調が発生する条件を特徴付けすることも可能である．また，実現可能性必要条件を体系的・階層的に分類したことで，必然的あるいは妥協的な協調可能性に関してより詳細な分析が可能となった．

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

図らずも新たな実現可能性必要条件群を発見し，その特性の分析及び分類を優先して行なったため，当初の既知実現可能性必要条件群に基づいた協調的リアクティブシステム自動合成手法の開発及びその技術的課題を明らかにすることができなかった．また，当初の予定通りにエフォートを割くことができなかったため，成果を論文にまとめることができなかった．
ただし，新たに発見した実現可能性必要条件群は協調的リアクティブシステム自動合成への活用を見込めるあるため，研究計画後半に予定していた理論の拡張・洗練を先取りしたものともいえる．

Strategy for Future Research Activity

まずは，今年度の研究内容を整理し成果を発表する．
そして，新たに発見したものも含め，実現可能性必要条件に基づいてシステムと環境間で必然的あるいは妥協的に協調が発生する条件を明らかにし，また，その時に不完全/協調的リアクティブシステムを自動合成する手法の開発を目指す．

Causes of Carryover

次年度は，今年度発表できなかった研究成果を国際会議等で発表するために利用する．