有理数プレスブルガー文真偽判定の高速処理系

用于判断有理普雷斯堡句子真假的高速处理系统

基本信息

批准号：
11780219
负责人：
岡野浩三
金额：
$ 1.41万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

项目摘要

本研究では,実用的な実時間システムの諸性質(安全性,設計の正しさ)を自動判定することを目標に,有理数プレスブルガー文の真偽判定アルゴリズムの実用的高速化方法を考案し,実際にそのような応用システムに使用できる真偽判定プログラムを実装する.昨年までに基本アルゴリズムは完成し,また高速化のためのアルゴリズムの検討が終わっていた.そこで今年度はその高速アルゴリズムの実装と評価を行った.また評価実験の結果をまとめ論文投稿を行った.本研究の基本となるアルゴリズムは,従来の種々提案されてきた判定アルゴリズムとは大きく異なり,計算幾何学上のアルゴリズムに基づくものである.実装にあたり,表現データ構造である凸多面体の数をなるべく少なくする,真偽判定の処理に伴って必要であるデータ構造の変形をなるべく効率よく行う,冠頭標準形ではない,一般の形の式を扱えるようにするなどの工夫を行った.実装した有理数プレスブルガー文の真偽自動判定ルーチンに対して評価実験を行った結果を,非同期バス転送プロトコルの試験系列の自動生成など実用的な検証例題に適用した結果,十分実用時間で試験系列の生成ができることが確かめられた.また,一般のプレスブルガー文に対してアルゴリズムの振る舞いを調べた結果,改良前よりも高速に判定できることがわかった.

在这项研究中，我们设计了一种实用的方法来加速理性 Presburger 句子的真值确定算法，目标是自动确定实际实时系统的各种属性（安全性、设计的正确性）。我们将实现真值/假值。实际可以用于此类应用系统的判断程序。去年完成了基本算法，并且因此，今年，我们实现并评估了高速算法，并总结了评估实验的结果，并提交了构成该算法基础的论文。研究如下。这与过去提出的各种判断算法有显着不同，是基于计算几何的算法。在实现中，我们将最小化作为表示数据结构的凸多面体的数量，使真/假判断过程所需的数据结构的转换尽可能高效，并使用非规范形式的通用形式。我们已经做出了努力，例如可以处理表单的表达。将评估实验的结果应用于实际验证示例（例如异步总线传输协议的测试序列的自动生成）的结果是，通过研究测试序列的行为，可以在足够的实际时间内生成测试序列。对于保加利亚语句子算法，我们发现它可以比改进之前更快地做出决策。