研究課題
基盤研究(C)
本研究では MRGP における位相型近似における精度保証ならびに状態爆発の問題を解消し,実用面における位相型近似の適用可能性を拡大した.特に,位相近似に対する精度保証として確率順序による上下限値の評価および全変動距離による評価を行った.さらに,状態爆発の問題に対しては位相型近似したマルコフモデルに対する完全サンプリングの開発を行った.完全サンプリングでは上下限値を得るための数理計画問題を定義し,これをSMTソルバで解くことによって,より広いクラスのモデルに対して適用することを可能にした.
情報学
ここで得られた成果は位相型近似で従来から指摘されてきた精度保証と状態爆発の問題をある程度可決し,その適用可能性を大幅に向上させた.確率モデルによるシステム評価は,これからIoT/CPSシステムで利用されるモデルベース開発などでのシステム検証に対して有効である.そのため,ここで得られた成果はシステム全体の高信頼化に対して大きく寄与するものと考えられる.