凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用

柴田, 直樹; 岡野, 浩三; 谷口, 健一

電子情報通信学会論文誌D, 2001, J84-D1(7), 999-1008

アクセス数:762件（2025-10-26 09:59 集計）

固定URL: https://hdl.handle.net/11094/27415

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
IEICE_J84-D1_7_999 pdf なし 1.33 MB 151 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
A Decision Algorithm for Rational Presburger Sentences Using a Merge Routine for Polyhedra and Its Application to Formal Verification
オウタメンタイ　ヘイゴウ　ヲ　モチイタ　ユウリスウ　プレスブルガーブン　シンギ　ハンテイ　アルゴリズム　ノ　ジッソウ　ト　ケイシキテキ　セッケイ　ケンショウ　ヘノ　テキヨウ
著者
NRID
1000040335477 1000040335477
著者名
柴田, 直樹 ; シバタ, ナオキ ; Shibata, Naoki
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000000029513 1000000029513
著者名
谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
キーワード等
有理数プレスブルガー文
真偽判定
凹多面体
適合性試験
抄録
加算をもつ有理数の理論（有理数変数，有理数定数，+，-，=，<∧, ∨, ∀, ∃からなる理論）の上の閉論理式（RP文）の真偽判定ルーチンは通信プロトコルのテスト，ハードウェアのタイミング検証などに利用できる．筆者らは以前，計算幾何学の手法を利用し，時間計算量を改善したRP文真偽判定アルゴリズムを提案した．本論文では，まずそのアルゴリズムに対する凹多面体併合を用いた高速化法について述べる．次に，その手法を実装した真偽判定ルーチンをMC68030バス上で非同期バスマスタ転送を行う時間オートマトンの適合性試験系列生成に適用し，評価した結果について述べる．高速化により，比較的簡単な時間制約をもつ時間オートマトンの実行可能性判定の例に対し，実際の検証で現れる変数の数が16個，不等式の数が20個程度のRP文をCPU時間数秒程度（Pentium III 600 MHz）で判定できるようになった．
出版者
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名
電子情報通信学会論文誌D
巻(号)
J84-D1(7)
ページ
999-1008
刊行年月
2001-07-01
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/27415
PISSN
09151915
NCID
AA11341020
関連情報 (references)
URI
http://search.ieice.org/
アクセス権
open access
権利情報
Copyright © 2001 IEICE
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article