• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2010 Fiscal Year Annual Research Report

様相論理の決定手続きとソフトウェア検証への応用

Research Project

Project/Area Number 21500006
Research InstitutionNational Institute of Informatics

Principal Investigator

田辺 良則  国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (60443199)

Keywords様相論理 / 決定手続き / ソフトウェア検証 / モデル検査 / 充足可能性 / 様相μ計算 / min-plus代数
Research Abstract

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

  • Research Products

    (1 results)

All 2010

All Journal Article (1 results) (of which Peer Reviewed: 1 results)

  • [Journal Article] Decidability and Undecidability Results of Modal μ-calculi with N-infinity Semantics2010

    • Author(s)
      Alexis Goyet, Masami Hagiya, Yoshinori Tanabe
    • Journal Title

      WOLLIC2010, Lecture Notes in Artificial Intelligence

      Volume: 6188 Pages: 148-160

    • Peer Reviewed

URL: 

Published: 2012-07-19  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi