2010 Fiscal Year Annual Research Report
離散ダイナミクスの流体化によるシステムの安全性検証
| Project/Area Number |
21500009
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
平石 邦彦 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40251970)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 孝一 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (50452115)
|
|---|
| Keywords | 形式検証 / 形式手法 / ハイブリッドシステム / 実時間システム / 性能評価 |
|---|
| Research Abstract |
離散ダイナミクスの流体化に関する理論的基盤とシミュレーション手法の確立を目的として,平成22年度は,以下の3つの研究課題について研究を行った。
1.述語抽象化計算の高速化に関する研究:ハイブリッドシステムの保証付き近似計算のアプローチとして,状態空間を与えられた述語集合により分割し,その上の離散的状態遷移で近似する述語抽象化の手法がある.しかし,述語により抽象化された状態空間は述語数の指数関数的な数の離散状態を含むため,計算の効率化が必要である.平成21年度は,2次元の状態空間に対して箱抽象化(Box Abstraction)の高速化に関する研究を行ったが,平成22年度は手法を多次元の場合に一般化し,さらに近似精度に関する理論的裏付けを与えた。手法は計算機プログラムとして実装し,実験的評価を行った。成果は国内研究会で発表し,現在,論文を学術論文誌に投稿中である。
2.確率ペトリネットの流体化に関する理論的考察:一般化確率ペトリネット(GSPN)の流体化モデルとしてRTCPN(Routing Timed Continuous Petri Nets)というモデルをすでに提案しているが,RTCPNがGSPNで計算される状態分布の期待値を正しくシミュレートできるための条件について考察した。また,その条件をペトリネットの構造的制約として表現する方法を与えた。
3.ハイブリッドシステムのソルバーに関する研究:混合整数計画法ソルバーのCPLEXおよび確率モデル検査器のPRISMを利用した確率ハイブリッドシステムの状態空間計算に関する研究を行った。
|
