モデル検査を用いた確率ブーリアンネットワークの可到達性解析

摘要

本論文では，確率ブーリアンネットワーク(PBN)の可到達性解析に対し，モデル検査ツールを適用することを考える．PBN とは，ブール関数が各時刻で確率的に選択されるモデルであり，近年盛hに研究されている．しかしながら，既存手法では，n次元の状態に対し，2~n個のノードをもつ状態遷移図（離散時間マルコフ連鎖）を計算する必要がある．本論文では，確率的モデル検査ツールPRISMを用いた，簡便な実装方法を提案する．提案手法ではブール関数を直接用いており，少なくとも設計者が離散時間マルコフ連鎖を計算する必要がない．また，PRISM 上では，確率時間分岐時相論理(PCTL)で記述された仕様が検証できる．本論文では可到達性問題をPCTL で記述し検証する．