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

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

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

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

This year, the abstract information system is used to explore the formalization of the information system. This year, it is necessary to analyze and analyze the information system in the current year. The time response is similar to that of the time link, and the abstraction does not need to be lost. The main results are as follows: "2: 00". 1. Abstract to achieve the possibility that you can use it in terms of formatting and Linearly Priced Timed Automata usage. In the past, we proposed that we should abstract to the possibility that the possibility could be reached. We would like to know that the most important thing is to make a decision. In the abstract, it is necessary to make the most comprehensive information on the examination of the information system, the validity of the information system, the validity of the information system, and the integrity of the information system. Please do not know if you are in trouble, and you will not be able to use the Linearly Priced Timed Automata analysis system. two。 Time payment multiple collections are required for import and upload parsing. In recent years, it is very important to study the situation in a timely manner. We do not need to know how to do this, including the concept of communication, the concept of time payment, and the cost of multiple collections. It is necessary to realize that there is a limit on the possibility of covering.It is necessary to realize the possibility of a bounded coverage. the basic performance of a multi-set security agreement is related to the non-compliance system of multiple sets of payments. the rules of the agreement include that the possibility is determined by the agreement. On the basis of the analysis of multi-collection and multi-collection, the analysis method and the analysis method of multi-collection, multi-set, multi-set, multi

项目成果

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)

Mitsuharu Yamamoto：“抽象 A^* 算法及其在线性定价定时自动机中的应用”第二届亚洲编程语言和系统研讨会论文集（APLAS 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)

Masami Hagiya：“定时多重集重写的符号分析及其在协议分析中的应用（扩展摘要）”证明和计算中的重写，国际研讨会，RPC01。