|
リアクティブシステム仕様の実現可能性に関する検証は，仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが，一般に煩雑で計算コストの高い処理を伴う．本研究ではリアクティブシステム仕様の実現可能性検証の効率化を目的とし，本年度は以下について取り組んだ．
＜実現可能性判定器の実装＞：実現可能性判定やモデル検査など，オートマトンや状態遷移系を扱う検証手続きの実装においてはしばしばシンボリック技法が用いられる．シンボリック技法では，オートマトンや状態遷移系の遷移関係を一つの論理式としてとらえる．そして，論理式を高速に処理することができるBDDやSATソルバを用いて効率的に判定を行う．本研究では，新たな実装技法：「部分シンボリック技法」について検討した．この部分シンボリック技法では，オートマトンの各状態ごとの遷移集合（その状態を起点とする遷移の集合）をひとつのBDD（Multi-terminal BDDという種類のBDDを用いる）で表現する．各状態は明示的に扱う．この技法は，シンボリック技法と同様，BDDを利用して効率的にオートマトンの遷移を処理できるというメリットを持つ．さらに，他の効率化技法と併用させやすいというメリットも持つ（通常のシンボリック技法においては，不必要な状態の除去などの他の効率化技法を併用させると，遷移関係の論理式表現が複雑になるため，逆にパフォーマンスが落ちることがある）．本年度は，このような部分シンボリック技法を用いて実現可能性判定を実装し，その効率を実験により確かめた．
|
