頻度オペレータを導入したProbabilictic CTLとそのモデル検査アルゴリズム

• 冨田尭

• 萩原茂樹

• 樋浦信

• 伊藤宗平

• 米崎直樹

抄録

確率的なシステムの性質の記述にはしばしば確率計算木論理Probabilistic Computation Tree Logic (PCTL)が用いられている。PCTLでは、「いつかイベントが生起する」や「ずっとイベントが生起し続けている」などの性質を満たすパスの生起確率に言及できる。しかし、「80% 以上の頻度でイベントが生起する」などのイベントの生起頻度に関する性質を記述することはできない。本稿では、イベントの生起頻度を記述できるようにPCTLを拡張した確率-頻度計算木論理を提案し、そのモデル検査アルゴリズムの概略を示す。

収録刊行物

• 第73回全国大会講演論文集

  第73回全国大会講演論文集 2011 (1), 235-236, 2011-03-02

キーワード

• ソフトウェア科学・工学

詳細情報

• CRID: 1050292572136945152
• NII論文ID: 170000088287
• NII書誌ID: AN00349328
• Web Site: http://id.nii.ac.jp/1001/00107719/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles