2015 Fiscal Year Research-status Report
MRSPN/MRGP解析の自動化に向けたスケーラブルアルゴリズムの開発
| Project/Area Number |
26330028
|
|---|
| Research Institution | Hiroshima University |
|---|
Principal Investigator |
岡村 寛之 広島大学, 工学(系)研究科(研究院), 准教授 (10311812)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | システム工学 / 性能評価 / 確率モデル / ペトリネット / モデル検査 |
|---|
| Outline of Annual Research Achievements |
平成27年度はMRGPの過渡解析手法に関する研究を行った．まず，MRGPの過渡解析に対して位相型近似による手法を開発した．位相型近似とは一般分布を位相型分布と呼ばれる分布で近似する手法である．位相型分布が連続時間マルコフ連鎖で定義できることから，一般的な MRGP を連続時間マルコフ連鎖の解析に還元することができる．ここでは，状態数の低減を行うためクロネッカー和・積による位相型近似の表現を行った．また，これらを MRSPN から状態間の依存関係を分析して，自動的に分割するためのアルゴリズムを構築し，有効性の検証をおこなった．探索では，一般分布による推移に基づいた状態分類を効率的に行うことによって，過渡解のみならず MRGP の定常解析にも利用できる表現を得ることができた．
また，位相型近似では近似によって得られた連続時間マルコフ連鎖の状態数が大きくなるため，通常の解析では現実的な時間で結果を得ることが困難な場合がある．そのため，クリロフ部分空間法に基づいた解析手法の検討も行った．クリロフ部分空間法によるマルコフ連鎖の解析はこれまでに知られていたが，連続時間マルコフ連鎖の定常解・準定常解を利用することにより，より高速な解析手法の構築を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
過渡解析に利用可能な MRSPN の分割アルゴリズムが完了している．また過渡解析手法としてはクリロフ部分空間法による手法の検討が終了した．全体の進捗としては問題ない．
|
| Strategy for Future Research Activity |
平成28年度は「モデル検査への拡張」と「ツール作成」を行う．
【モデル検査への拡張】モデル検査では，状態推移モデル上で指定された時間に依存した性質が成立するかどうかを検査する．確定的なモデル検査は BDD や SAT を用いた条件を満たす状態を探索することが主な解析手法となるが，状態が確率的に推移するモデル上での検査は本質的に状態依存モデルの過渡解析に対応する．そのため，ここまでで確立した解析手法を確率的モデル検査に応用することを考える．確率的モデル検査では特定の状態しか注目しないため，確定的なモデルチェッキング手法との組み合わせることにより高速な過渡解析を実現する．
【ツールの作成】ツールの作成では「MRSPN/MRGP を定義する XML スキームの開発」，「解析ツールの実装」を行う．他のツールからの利便性を考慮して MRSPN/MRGP の定義を行うための XML スキーマ開発する．XMLスキーマは XML 文書中のタグなどの意味づけを行うものであり，このような定義はモデルの自動変換などに役立つ．本研究では，既存のペトリネットに対する XML に対して MRSPN を記述できるような拡張を行う．また，MRGP を定義するための XML の開発も行う．さらに，二つのツール（MRSPN構造解析ツール，MRGP 過渡解析ツール）の実装を行う．MRSPN構造解析ツールは MRSPN を入力として，分割された MRGP の XML を出力とする．一方，MRGP 過渡解析ツールでは開発された数値計算アルゴリズムを実装したツールであり，性能評価指標の過渡特性や確率的モデル検査の結果を出力とする．
|
