| 研究課題/領域番号 |
15K15969
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
島川 昌也 東京工業大学, 大学院情報理工学研究科, 情報理工学研究科研究員 (00749161)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | リアクティブシステム仕様 / 実現可能性 / ω-オートマトン |
|---|
| 研究実績の概要 |
リアクティブシステム仕様の実現可能性に関する検証は，仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが，一般に煩雑で計算コストの高い処理を伴う．本研究では，リアクティブシステム仕様の実現可能性検証の高速化を目的とする．平成２７年度は以下に取り組んだ．
＜セミ・シンボリック手法を用いた決定性ωオートマトン構成の効率化＞：リアクティブシステム仕様の実現可能性検証においては，仕様から決定性ωオートマトン（無限長の語を扱うオートマトン）を構成する必要がある．近似を行わない場合，その手続きは煩雑である．それが原因で，他の検証手続きの効率化においてしばしば用いられるシンボリック手法の適用は難しい．そこで本研究では，我々が過去に提案したセミ・シンボリック手法を適用する．この手法では，部分的にBDD(Binary Decision Diagram)を利用する．具体的には，各状態からの遷移の集合をひとつのBDDで表現する（シンボリック手法では，オートマトン全体の遷移関係をひとつのBDDで表現する）．本年度は，この手法を用いた決定性ωオートマトン構成手続きの実装を行った．そして，その実装が多くの場合，他の決定性ωオートマトン構成ツールよりも高速であることを確認した．
＜有界実現可能性の新たな検査法＞：近似を行う実現可能性の有界検査法についても取り組んだ．有界実現可能性判定が他の問題(到達可能性判定問題)に帰着できることを明らかにした上で，それを利用した既存手法よりも高速なSATベースの検査法を提案した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の計画通り，セミ・シンボリック手法を用いた決定性ωオートマトン構成手続きの実装を行い，一定の成果を得た．それゆえ，現在までの達成度はおおむね順調であると判断した．
|
| 今後の研究の推進方策 |
当初の予定通り，リアクティブシステム仕様の実現可能性検証の効率化について以下に取り組む予定である．
＜on-the-fly簡約手法＞：模倣関係や強連結成分情報を利用し，ωオートマトンを簡約する手法について多く研究されている．それらの多くは，構成後のオートマトンに対して適用されるものである．本研究では，構成途中に簡約を適用することで扱う状態やエッジを減らし，構成自体のコストも低減させるon-the-fly簡約手法について検討する．我々は，他の検証分野で，セミ・シンボリック手法を用いるアプローチにおいて同様の簡約が有効であることを既に示している．今後は，それをベースに決定性ωオートマトン構成におけるon-the-fly簡約手法の検討を行う予定である．
|
| 次年度使用額が生じた理由 |
平成２７年度に購入予定であったPCの購入を延期したため，次年度使用額が生じた．
|
| 次年度使用額の使用計画 |
平成２８年度にはPCを購入する．残りは当初の計画通り，国際会議・国内学会での研究発表に伴う旅費，学会参加費，英文校正費用等にあてる予定である．
|
