• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

研究課題

研究課題/領域番号 16016211
研究種目

特定領域研究

配分区分補助金
審査区分 理工系
研究機関千葉大学

研究代表者

山本 光晴  千葉大学, 理学部, 助教授 (00291295)

研究分担者 萩谷 昌己  東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
辻 尚史  千葉大学, 理学部, 教授 (70016666)
研究期間 (年度) 2004 – 2005
研究課題ステータス 完了 (2005年度)
配分額 *注記
4,400千円 (直接経費: 4,400千円)
2005年度: 2,300千円 (直接経費: 2,300千円)
2004年度: 2,100千円 (直接経費: 2,100千円)
キーワード形式的手法 / 証明検証系 / 抽象モデル検査 / 時相論理 / セルオートマトン / グラフ書き換え
研究概要

平成13年度から継続して行っている課題「抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証」において、平成17年度は「時相論理を用いたグラフ書き換え系の抽象化」に関する研究、および最終年度に際してこれまでの研究のとりまとめを行った。
我々は平成14年度よりグラフ上の書き換え系を時相論理により抽象化し、検証に利用することについて研究を行ってきた。グラフ上の書き換えはプログラム中で頻繁に用いられるリンク構造に対する操作を含んでおり、一般には状態空間が無限となるため、モデル検査等の有限的探索手法を用いる場合には抽象化が必要となる。
我々が時相論理を抽象化に用いているのは、(1)時相論理に対するいくつかの拡張がグラフ構造の抽象化に有用であること(2)決定可能な論理を用いることによって、充足可能性判定を抽象化に利用できることが主要な理由である。
(1)において我々が注目した拡張は2方向性、global modality,およびnominalである。空間的な性質の記述において順方向だけでなく逆方向の記述を要する際、逆様相を持つ時相論理、すなわち2方向の時相論理を用いるのが自然である。global modalityは抽象化によるshape analysisと充足可能性判定において構成されるタブローとを結びつける。nominalはループに関する性質等、グラフ上の空間的性質を記述する能力を強化する。
(1)のような拡張を施しても(2)の決定可能性が崩れないことが時相論理を用いる利点となっている。このことにより、抽象化に用いる時相論理式の集合が与えられれば、充足可能性判定を用いて抽象化が自動的に計算できるような枠組みになっている。平成15年度から継続して行っているBDDを用いた充足可能性判定手続きは、この抽象化の自動計算の部分で利用される。

報告書

(2件)
  • 2005 実績報告書
  • 2004 実績報告書
  • 研究成果

    (5件)

すべて 2005 2004

すべて 雑誌論文 (5件)

  • [雑誌論文] A Decision Procedure for the Alternation-free Two-way Modal mu-calculus2005

    • 著者名/発表者名
      Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya
    • 雑誌名

      Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),LNCS 3702

      ページ: 277-291

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] Model Checking of Multi-Process Applications Using SBUML and GDB2005

    • 著者名/発表者名
      Yoshihiko Nakagawa, Richard Potter, Mitsuharu Yamamoto, Masami Hagiya, Kazuhiko Kato
    • 雑誌名

      Workshop on Dependable Software --Tools and Methods --,International Conference on dependable Systems and Networks

      ページ: 215-220

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005

    • 著者名/発表者名
      田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
    • 雑誌名

      コンピュータソフトウェア 22・3

      ページ: 154-166

    • NAID

      130004892028

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005

    • 著者名/発表者名
      田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
    • 雑誌名

      コンピュータソフトウェア (掲載予定)

    • NAID

      130004892028

    • 関連する報告書
      2004 実績報告書
  • [雑誌論文] Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic2004

    • 著者名/発表者名
      Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto, et al.
    • 雑誌名

      Functional and Logic Programming (FLOPS 2004), LNCS 2998

      ページ: 7-21

    • 関連する報告書
      2004 実績報告書

URL: 

公開日: 2004-04-01   更新日: 2018-03-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi