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

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

研究課題

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

特定領域研究

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

研究代表者

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

研究分担者 高橋 孝一  産業技術総合研究所, 情報科学連携研究体, 副研究ラボ長
辻 尚史  千葉大学, 理学部, 教授 (70016666)
萩谷 昌己  東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
研究期間 (年度) 2003
研究課題ステータス 完了 (2003年度)
配分額 *注記
2,000千円 (直接経費: 2,000千円)
2003年度: 2,000千円 (直接経費: 2,000千円)
キーワード形式的手法 / 証明検証系 / 抽象モデル検査 / 時相論理 / セルオートマトン / グラフ書き換え
研究概要

平成13年度から継続して行っている課題「抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証」において、平成15年度は「2方向計算木論理(2CTL)を用いたグラフ遷移系の抽象化」に関する研究を行った。
「2方向計算木論理を用いたグラフ遷移系の抽象化」は、平成14年度に行ったグラフとその上の書き換えによるシステムの抽象化の議論をより一般化な形で展開したものであり、セルをリンクによって繋いでできる構造からなるシステムにおいて、隣接あるいは関連するセルの状態に応じてセルの状態が同期的あるいは非同期的に変化するような状況を抽象化するためのものである。グラフ上の書き換えはプログラム中で頻繁に用いられるリンク構造に対する操作を含んでおり、一般には状態空間が無限となるため、モデル検査等の有限的探索手法を用いる場合には抽象化が必要となる。
従来研究と比較して、本研究は以下のような特徴を有している。
・セルオートマトンの解析
セルの状態が同期的あるいは非同期的に変化する場合の両方について扱っている。
・2CTLの利用
セルの抽象的状態を記述するために、通常の計算木論理(CTL)に逆方向の様相を追加した2方向計算木論理(2CTL)を使用している。抽象化の計算においては2CTLの充足可能性判定が大きな役割を果たしている。
・抽象化の自動計算
抽象化を特徴付ける2CTL論理式の集合を与えると、抽象化を自動的に計算することができる。これを可能にするため、2CTLの充足可能性判定手続きの定式化を行った。

報告書

(1件)
  • 2003 実績報告書
  • 研究成果

    (2件)

すべて その他

すべて 文献書誌 (2件)

  • [文献書誌] Koichi Takahashi, Masami Hagiya: "Abstraction of Graph Transformation Using Temporal Formulas"Workshop on Model-Checking for Dependable Software-Intensive Systems 2003. 65-66 (2003)

    • 関連する報告書
      2003 実績報告書
  • [文献書誌] Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto, et al.: "Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic"Functional and Logic Programming (FLOPS 2004), LNCS 2998. 7-21 (2004)

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

URL: 

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

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

Powered by NII kakenhi