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

2009 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 21500006
Research InstitutionThe University of Tokyo

Principal Investigator

田辺 良則  The University of Tokyo, 大学院・情報理工学系研究科, 特任助教 (60443199)

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

われわれは,これまで,様相μ計算を用いた抽象化を基礎としたソフトウェア検証技法を研究してきた.その枠組みでは,主に安全性に分類される性質の検証を行えるようになったが,本研究では,それをさらに発展させ,より広い性質の検証をめざしたもので,具体的には,活性に分類される性質が対象となっている.
本年度は,まず,抽象化技法の適用に関する理論的な基礎を整備した.具体的には,クリプキ構造に関する基本的な変換操作を定義し,様相μ計算の論理式で表現される条件について,これらの変換操作に関する,最弱事前条件と最強事後条件が,ふたたび,様相μ計算の論理式で表現されることを証明し,その計算方法をを確立した.このことを用いて,これらの変換に関し,後向きおよび前向きの推論を行うことが可能となった.Hoare論理と組み合わせることで,アルゴリズムの検証ができる.
つづいて,N∞値クリプキ構造における様相μ計算のモデル検査法を開発した.検査法は従来も知られていたが,まず,従来法にあった「含意を含まない」という制限を撤廃し,適用範囲を広げ,さらに,従来法の適用可能な範囲についても,計算量を削減した.また,検査法の正当性証明を改良して,見通しの良いものとした.
本研究全体としては,同じ設定における充足可能性判定手続きを見いだすことが目標である.2値の様相μ計算に関する理論がそうであるように,充足可能性判定を行う手法は,モデル検査法がそのベースとなる可能性が高いと考えられる.その観点から,今回の検査法は重要な一歩である.しかし,現在の検査法には,(今回拡張した範囲について)計算量の評価ができていないという問題がある.今後,この解明が可能なように,アルゴリズム自体を改良する研究をすすめる計画である.

  • Research Products

    (4 results)

All 2009

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

  • [Journal Article] Pre- and Post-conditions Expressed in Variants of the Modal μ-calculus2009

    • Author(s)
      Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, Koichi Takahashi
    • Journal Title

      IEICE Transactions on Information and Systems Vol.E92-D

      Pages: 995-1002

    • Peer Reviewed
  • [Presentation] Games and Natural Number-valued Semantics of the Modal μ-calculus2009

    • Author(s)
      Masami Hagiya, Yoshinori Tanabe(登壇)
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学
    • Year and Date
      2009-09-16
  • [Presentation] Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus2009

    • Author(s)
      Masami Hagiya, Yoshinori Tanabe(登壇)
    • Organizer
      6th Workshop on Fixed Points in Computer Science (FICS 2009)
    • Place of Presentation
      University of Coimbra, Portugal
    • Year and Date
      2009-09-13
  • [Presentation] Decidability and Undecidability Results of Modal μ-calculi with N-infinity Semantics2009

    • Author(s)
      Alexis Goyet, Masami Hagiya, Yoshinori Tanabe(登壇)
    • Organizer
      情報処理学会プログラミング研究会(PRO)
    • Place of Presentation
      東京工業大学
    • Year and Date
      2009-06-08

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi