6A-3
頻度オペレータを導入したProbabilictic CTLとそのモデル検査アルゴリズム
○冨田 尭，萩原茂樹，樋浦 信，伊藤宗平，米崎直樹（東工大）
確率的なシステムの性質の記述にはしばしば確率計算木論理
Probabilistic Computation Tree Logic (PCTL)
が用いられている。
PCTLでは、「いつかイベントが生起する」や「ずっとイベン
トが生起し続けている」などの性質を満たすパスの生起確率
に言及できる。しかし、「80% 以上の頻度でイベントが生起
する」などのイベントの生起頻度に関する性質を記述するこ
とはできない。
本稿では、イベントの生起頻度を記述できるようにPCTLを拡
張した確率-頻度計算木論理を提案し、そのモデル検査アル
ゴリズムの概略を示す。