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

用于抽象模型检查的图搜索算法的形式化和验证

• 批准号: 14019014
• 负责人: 山本 光晴
• 金额: $ 1.47万
• 依托单位: Chiba University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14019014/
• 关键词: 形式的手法; 証明検証系; 抽象モデル検査; 時間付き多重集合書き換え; 時間付きオートマトン; 時間ペトリネット; グラフ書き換え

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

The research on the formalization and preparation of the proof system for abstract test results was carried out in the following areas in 2014. 1. A representative example of the analysis time of the properties of multiple sets of text in Heisei 13 is the inclusion time of multiple sets of text in Heisei 13, and the investigation of the basic properties of multiple sets of text in Heisei 13 is the possibility of arrival, boundedness, and coverage. Speciality, boundedness, coverage, determination of probability, determination of result, determination of probability, generalization of result, determination of probability, determination of result, determination of probability, determination of result, determination of result, determination of probability, determination of result, determination of possibility, determination of result, determination of possibility, determination of result, determination of possibility, determination of result, determination of possibility, determination of result, determination 2. Abstraction of time-phase logical expressions of structures and methods of abstractions and generalizations of time-phase logical expressions. This is generally limited, and the results are limited. This is possible, and this is safety related. The results of the above 2 are related to each other. Multiple sets are constructed in such a way that they can be transformed into multiple sets.また、リンク构造の変化もやはりグラフ上の书き换えと捕えることができる。Time, space, and time are the most important aspects of the process.

项目成果

Koichi Takahashi, Masami Hagiya: "Formal Proof of Abstract Model Checking of Concurrent Garbage Collection"Thirty Five years of Automath. 115-126 (2002)

Koichi Takahashi、Masami Hagiya：“并发垃圾收集抽象模型检查的形式化证明”自动化三十五年。

Mitsuharu Yamamoto et al.: "Decidability of Safety Properties of Timed Multiset Rewriting"FTRTFT 2002,LNCS 2469. 165-183 (2002)

Mitsuharu Yamamoto 等人：“定时多集重写的安全属性的可判定性”FTRTFT 2002，LNCS 2469. 165-183 (2002)