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

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

研究課題

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

特定領域研究

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

研究代表者

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

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

抽象モデル検査で用いられるグラフ探索アルゴリズムを証明検証系で形式化するための準備として、平成14年度は以下の点に関する研究を行った。
1.平成13年度に引き続き、時間付き多重集合書き換えの性質の解析
時間を含むシステムの代表例である時間オートマトンと時間ペトリネットの両方を包含するシステムとして平成13年度に導入した時間付き多重集合書き換えについて、基本的性質である到達可能性・有界性・被覆性の決定可能性に関する考察をより進めた。特に、有界性・被覆性が決定可能であるクラスをより詳細に特徴づけることにより、決定可能性の結果が時間オートマトンの決定可能性の一般化になるようにした。
2.グラフの時相論理式による抽象化
高橋・萩谷によるリンク構造の正則表現による抽象化を用いた抽象モデル検査の考え方を発展させ、リンク構造の一般化であるグラフを時相論理式によって抽象化する方法を与えた。これにより、一般には有限でないグラフ書き換えの結果を有限的に捕えることが可能となり、安全性に関するモデル検査が可能となる。
上の2つの成果は次のように関連している。まず、多重集合に構造を導入することによりグラフが得られるため、時間付き多重集合書き換えの拡張として時間付きグラフ書き換えが考えられる。また、リンク構造の変化もやはりグラフ上の書き換えと捕えることができる。時間付きグラフ書き換えのとその抽象化を合わせて考えることにより、将来的に時間と空間の両方を扱うシステムの検証を行うことを目指している。

報告書

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

    (2件)

すべて その他

すべて 文献書誌 (2件)

  • [文献書誌] Mitsuharu Yamamoto et al.: "Decidability of Safety Properties of Timed Multiset Rewriting"FTRTFT 2002,LNCS 2469. 165-183 (2002)

    • 関連する報告書
      2002 実績報告書
  • [文献書誌] Koichi Takahashi, Masami Hagiya: "Formal Proof of Abstract Model Checking of Concurrent Garbage Collection"Thirty Five years of Automath. 115-126 (2002)

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

URL: 

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

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

Powered by NII kakenhi