電子情報通信学会総合大会講演要旨
AI-3-5
ハイブリッドシステムの統計的モデル検査
○石井大輔(福井大)・冨田 尭(北陸先端大)・米崎直樹(放送大)
ハイブリッドシステムは状態が連続変化と離散変化の振る舞いをするシステムである.制御工学,計算生物学,物理学等の問題を直截に記述するためのモデルとして用いられている.ハイブリッドシステムの厳密なモデル検査は計算量が大きかったり決定不能であったりするため,より実用的な手法として統計的モデル検査法が提案されている.統計的モデル検査法は,ハイブリッドオートマトンと時相論式で記述した確率的な検証問題について,無作為に数値シミュレーションを複数回実施した後,統計的に判定を行う.数値計算した軌道に基づき有界線形時相論理式の充足性を判定する方法や,仮説検定による統計的評価の方法について説明する.統計的モデル検査法は現実的・複雑なモデルに対する多様な性質 (例: 安定性や頑健性) の検証を可能にする.