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

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

研究課題

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

特定領域研究(C)

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

研究代表者

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

研究分担者 萩谷 昌己  東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
研究期間 (年度) 2001
研究課題ステータス 完了 (2001年度)
キーワード形式的手法 / 証明検証系 / モデル検査 / グラフ探索 / 時間付き多重集合書き換え / 時間付きオートマトン / 時間ペトリネット
研究概要

本年度は、抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証へ向けて、特に時間を扱うシステムの解析に関連した研究を行った。時間を扱うシステムを対象としたのは、時間という連続的なものを扱うシステムにおいてモデル検査を行うには、抽象化が不可欠なためである。
主な成果は以下の2点である。
1.抽象到達可能性検査上でのA^*アルゴリズムの定式化と、Linearly Priced Timed Automataへの応用。
抽象モデル検査のためのグラフ探索アルゴリズムの候補として、以前より我々が提案してきた抽象到達可能性検査を拡張し、その上で最適化アルゴリズムの一つであるA^*アルゴリズムを定式化した。抽象アルゴリズムの上で最適化アルゴリズムを考え、その正当性を証明することにより、種々の具体アルゴリズムとその正当性を統一的に得ることを可能にした。さらに、このA^*アルゴリズムを、時間を扱うシステムの一つであるLinearly Priced Timed Automataの解析に応用した。
2.時間付き多重集合書き換えの導入と、その上の解析。
従来、時間を扱うシステムとして、時間付きオートマトンと時間ペトリネットが非常によく研究されてきた。我々はこれらのシステムを包括し、さらに拡張する概念として、時間付き多重集合書き換えというシステムを導入した。また、モデル検査などの解析を行うために必要となる到達可能性・有界性・被覆性といった基本的性質のそれぞれについて、時間付き多重集合書き換えが不変制約・対角線制約と呼ばれる規則を含む場合と含まない場合に関して決定可能性が成り立つかどうかを調べた。さらに時間付き多重集合書き換え上での時間制約に関する帰納的解析の手法を与え、それをプロトコルの解析に応用した。

報告書

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

    (2件)

すべて その他

すべて 文献書誌 (2件)

  • [文献書誌] Mitsuharu Yamamoto: "Abstract A^* Algorithm and Its Application to Linearly Priced Timed Automata"Proceedings of The Second Asian Workshop on Programming Languages and Systems (APLAS 2001). 193-205 (2001)

    • 関連する報告書
      2001 実績報告書
  • [文献書誌] Masami Hagiya: "Symbolic Analysis of Timed Multiset Rewriting and Its Application to Protocol Analysis (Extended Abstract)"Rewriting in Proof and Computation, International Workshop, RPC'01. 34-41 (2001)

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

URL: 

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

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

Powered by NII kakenhi