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

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13224012
• Research Institution: Chiba University
• Principal Investigator: 山本 光晴 千葉大学, 理学部, 助手 (00291295)
• Co-Investigator(Kenkyū-buntansha): 萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
• Keywords: 形式的手法 / 証明検証系 / モデル検査 / グラフ探索 / 時間付き多重集合書き換え / 時間付きオートマトン / 時間ペトリネット

Research Abstract

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

Research Products

• [Publications] 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)
• [Publications] 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)