2022 Fiscal Year Annual Research Report
Cooperative Reactive System Synthesis Based on Necessary Conditions of Realizability
Project/Area Number |
17K17763
|
Research Institution | Japan Advanced Institute of Science and Technology |
Principal Investigator |
冨田 尭 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)
|
Project Period (FY) |
2017-04-01 – 2023-03-31
|
Keywords | ソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リアクティブシステム / 実現可能性 / 自動合成 |
Outline of Annual Research Achievements |
仕様からのリアクティブシステム(RS)の自動合成では,通常,仕様違反させようとする敵対的環境を想定することで,非常に強い信頼性と安全性をもつRSの合成を試みる.しかし現実には,環境とRSの関係は必ずしも敵対的ではなく,協調・共生を前提とすることも多い.本研究では仕様の実現可能性必要条件に基づき協調的RSを自動合成する手法の開発に取り組んだ. 2021年度までに,関連研究の調査を行い,見出した実現可能性必要条件群及び既知の実現可能性必要条件群の厳密な形式的定義を呼び階層定理群を与えた.これらの実現可能性必要条件群は網羅性,保存可能性,安定化可能性及び戦略化可能性の4つの観点から体系的・階層的に分類でき,その観点から協力が発生し得ることを導くことができる.例えば,安定化可能性(相手からの一時的な協力により恒久的な安定状態へ到達し仕様を満たすことができるという性質)の観点からは,RS及び環境のそれぞれの目的(仕様)がそれぞれの立場から安定化可能であり,かつ,それぞれの安定状態へ到達するまでのお互いのふるまいが矛盾しないのであれば,RSを環境が協調することでそれぞれの目的(仕様)を満足することが可能となることが導出できる.また,保存可能性(仕様の充足可能性を保持し続けることができるという性質)の観点からも,類似の協調が発生する可能性を導出できる.そして,実現可能性必要条件群の特性について,判定手続きを構成するサブルーチンの共通性及び類似性からも分析し,また,各実現可能性必要条件判定の計算量を導出した. 2022年度は,必然的あるいは妥協的な協調強調が発生するための必要充分な条件及び協調的RSの合成の確立に向けて,時間的性質の分類・特徴づけを再考し,新たな実現可能性必要条件は見出した.
|
Research Products
(1 results)