- 著者
- 柴田 直樹 岡野 浩三 谷口 健一 シバタ ナオキ オカノ コウゾウ タニグチ ケンイチ Shibata Naoki Okano Kozo Taniguchi Kenichi
- 出版者
- 電子情報通信学会
- 雑誌
- 電子情報通信学会論文誌D (ISSN:09151915)
- 巻号頁・発行日
- vol.J84-, no.7, pp.999-1008, 2001-07-01
加算をもつ有理数の理論(有理数変数,有理数定数,+,-,=,<∧, ∨, ∀, ∃からなる理論)の上の閉論理式(RP文)の真偽判定ルーチンは通信プロトコルのテスト,ハードウェアのタイミング検証などに利用できる.筆者らは以前,計算幾何学の手法を利用し,時間計算量を改善したRP文真偽判定アルゴリズムを提案した.本論文では,まずそのアルゴリズムに対する凹多面体併合を用いた高速化法について述べる.次に,その手法を実装した真偽判定ルーチンをMC68030バス上で非同期バスマスタ転送を行う時間オートマトンの適合性試験系列生成に適用し,評価した結果について述べる.高速化により,比較的簡単な時間制約をもつ時間オートマトンの実行可能性判定の例に対し,実際の検証で現れる変数の数が16個,不等式の数が20個程度のRP文をCPU時間数秒程度(Pentium III 600 MHz)で判定できるようになった.