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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15017212
• Research Institution: Chiba University
• Principal Investigator: 山本 光晴 千葉大学, 理学部, 助教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): 高橋 孝一 産業技術総合研究所, 情報科学連携研究体, 副研究ラボ長 ; 辻 尚史 千葉大学, 理学部, 教授 (70016666) ; 萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
• Keywords: 形式的手法 / 証明検証系 / 抽象モデル検査 / 時相論理 / セルオートマトン / グラフ書き換え

Research Abstract

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

Research Products

• [Publications] Koichi Takahashi, Masami Hagiya: "Abstraction of Graph Transformation Using Temporal Formulas"Workshop on Model-Checking for Dependable Software-Intensive Systems 2003. 65-66 (2003)
• [Publications] 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)