活性と同時に保証可能な安全性特定のためのゲーム分析アルゴリズム

DOI IPSJ

Search this article

Abstract

イベントベースなシステムにおいて，「起こるべき事象がつねにいつかは起こる」という活性や「起こるべきでない事象はけっして起こらない」という安全性が保証可能かは動作環境に依存する．システムの動作環境のモデルと振舞いに対する要求を入力として，要求が保証された仕様を自動合成する離散制御器合成が研究されてきた．離散制御器合成では環境と要求からゲームを構築し，そのゲームに勝利できるような戦略を仕様として出力するが，保証可能な要求が入力されなければ勝利戦略が立てられず仕様は合成できない．このため開発者には保証可能な要求を特定することが求められた．与えられた環境と要求から保証可能な要求を特定する研究は行われているが，対象のドメインを絞ったり扱う要求を安全性のみに限定したうえでの実現であった．そこで本研究では活性と同時に保証可能な安全性を特定するためのゲーム定義と特定のためのアルゴリズムを提案する．また，提案アルゴリズムが活性と同時に保証可能な安全性を特定できることを証明し，そしてアルゴリズムの計算量が構築されるゲーム空間の状態数m，遷移数n，扱う安全性の数rに対してO(2nmr)と現実的な計算時間となりうることを確認した．

Requirements of the event-based systems are guaranteed under environmental assumptions. Our target requirements are safety properties, which means “bad things do not happen”, and liveness properties, which means “good things do always happen eventually”. Discrete controller synthesis is one of the technique acquiring the behavior specification which guarantees the given requirements in the given environment. This technique requires developers to identify the requirements guaranteeable in the environment. Several works identified such requirements, but they limit target requirements or target systems. In this paper, we use a two player game and identify guaranteeable safety properties while satisfying a liveness property. We also proposed an algorithm and proved that the algorithm can identify the guaranteeable safety properties. In addition we confirmed that the time complexity of the algorithm is O(2nmr), where n is the number of states, m is the number of transitions and r is the number of treated safety properties in the game.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top