| 研究概要 |
[項目1a:N∞値モデル検査法]2値の様相μ計算と同様に,充足可能性判定を行う手法は,モデル検査法がベースとなる可能性が高いため,この解明に取り組んでいる.前年度に得た部分的な結果である,正しい結果を必ず与えるモデル検査アルゴリズムのcomplexityの確定を目標として研究を進めた.残念ながら確定には至らなかったが,いくつかの関連する補題を証明した
[項目1b:N∞値充足可能性判定法]前年度の成果である意味論のゲーム表現に基づき,判定法の開発に着手した.全体の方針としては,(A)2値の論理式に変換して,既存の判定手続きを用いる(B)N∞値用のオートマトンを定義し,既存判定手続きを参照しつつも新たなアルゴリズムを構築する,の2つが考えられる.本年度は,考察しやすい(A)の方針をまず採用した.このアルゴリズム,およびその正当性証明をWOLLIC2010において発表した,(B)については,次年度の検討とする
[項目2a:2値の判定手続きの改良]現在の判定手続きにおける性能上のネックは特定できていたが,さらに調査した結果,案として持っていた方法がnominalを含む論理に対するタブロー法を様相μ計算に対して単純には適用できないことが明らかになった.このためため,いくつかの別の方法を検討した.(1)現在の手続きにおけるBDDの使用方法を見直し,より効率的なエンコーディング方法を検討した.いくつかの補助関数の性能において改良は得られたものの,依然として目標からは遠いのが現状である.このため,(2)Boolean SAT solverの適用の検討を開始した
[項目3a:検証対象の調査・検討]モデル検査において頻繁に用いられる強連結成分の確定を行うアルゴリズム,および,強公平性のもとでの活性検証を行うアルゴリズム等を対象として,本研究における充足可能性判定手続きが得られたとの前提のもとで、アルゴリズムの検証を行う枠組みを検討した
|
