凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
スポンサーリンク
概要
- 論文の詳細を見る
加算をもつ有理数の理論(有理数変数, 有理数定数, +, -, =, <, ∧, ∨, ∀, ∃からなる理論)の上の閉論理式(RP文)の真偽判定ルーチンは通信プロトコルのテスト, ハードウェアのタイミング検証などに利用できる。筆者らは以前, 計算幾何学の手法を利用し, 時間計算量を改善したRP文真偽判定アルゴリズムを提案した。本論文では, まずそのアルゴリズムに対する凹多面体併合を用いた高速化法について述べる。次に, その手法を実装した真偽判定ルーチンをMC68030バス上で非同期バスマスタ転送を行う時間オートマトンの適合性試験系列生成に適用し, 評価した結果について述べる。高速化により, 比較的簡単な時間制約をもつ時間オートマトンの実行可能性判定の例に対し, 実際の検証で現れる変数の数が16個, 不等式の数が20個程度のRP文をCPU時間数秒程度(Pentium III600MHz)で判定できるようになった。
- 2001-07-01
著者
関連論文
- 2-III-19 B_補酵素関与エタノールアミンアンモニアリアーゼの立体構造と変異導入に基づく触媒機構の解析(一般演題,日本ビタミン学会第62回大会発表要旨)
- 移動センサノードを用いたデータ収集型WSNでのk重被覆時間の最大化手法
- 指向性アンテナおよび車車間通信を用いた歩行者位置追跡手法とその評価(セッション2)
- Strutsフレームワークにおけるメタモデルを用いた追跡可能性実現手法の提案(アスペクト指向・Web)
- 12.B_補酵素関与エタノールアミンアンモニアリアーゼの性質とタンパク質工学的改変および結晶構造解析(第415回研究協議会研究発表要旨,ビタミンB研究委員会)
- 車車間通信による交差点鳥瞰映像ストリーミング手法の提案(セッション2)
- 各車両の予定経路情報を利用した車車間通信による情報取得手法の提案(セッション1)
- 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
- 被災地におけるDTNに基づいた情報収集・共有方式の提案(セッション1-C:マルチメディアシステム)
- 2-II-32 エタノールアミンアンモニアリアーゼのタンパク質工学的改変と結晶構造解析および変異導入(一般研究発表,日本ビタミン学会第61回大会研究発表要旨)
- 確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
- UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
- SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
- UML/OCLに記述された時間QoSの階層的検証手法の提案
- 確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
- SPINによるStrutsアプリケーションの動作検証を目的としたモデル生成手法の提案
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
- 携帯電話端末への低コスト動画広告配信を目的としたWiFi併用協調ダウンロード方式
- 都市や観光地における混雑状況を考慮した多数ユーザ同時巡回スケジューリング手法
- 拡張時間オートマトン群による実時間システムの記述および検証
- 無線センサネットワーク長寿命化のためのノード集合の分割に基づくスリープスケジューリング手法
- 無線センサネットワーク長寿命化のためのノード集合の分割に基づくスリープスケジューリング手法
- 天気変化を考慮した観光スケジュール群の探索アルゴリズム
- 利用者の状況に応じて画面レイアウトが変更可能な遠隔教育支援システムの提案
- 時間システムを対象とした到達可能性解析の高速化手法の提案
- 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
- OCLのJMLへの変換ツールの実装と評価
- OCLのJMLへの変換ツールの実装について
- 実時間システムを対象としたCEGARによる抽象洗練の並列化手法
- Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
- 上位設計におけるシステムの振る舞い検証技術(システム設計のための形式手法の基礎と応用)
- B-001 Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール(ソフトウェア,一般論文)
- JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証
- 制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,フォーマルアプローチ論文)
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- Daikonの限定利用によるJavaメソッドの事後条件の自動導出
- UMLモデルに対するXPathとXMI-differenceを用いた不整合検出と解消
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装
- 関数型言語ML向け形式的検証支援システムの試作
- 関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
- D-3-8 分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案(D-3. ソフトウェアサイエンス)
- マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出
- ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案
- ワークフロー記述向きの時間付きカラーペトリネット
- 時間制約付きカラーペトリネットで記述されたワークフローからのスケジュール導出
- 時間制約を持つGUI制御部の仕様記述の一手法
- 凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
- 入力値のみ保持する変数をもつEFSM群に対する動的性質の検証
- CPU設計導入教育への形式的設計検証手法の適用
- 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
- 1G-6 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
- 組合わせ幾何を用いた有理数プレスブルガー文真偽判定アルゴリズムにおける投影操作の高速化
- Tarski算術における冠頭標準形の閉論理式の真偽判定アルゴリズムの提案
- モバイルアンカノードを用いた低コストな水中センサノードの位置推定法
- 移動センサノードを用いたデータ収集型WSNでのk重被覆時間の最大化手法
- 水面を移動可能なアンカーノードを用いた水中センサネットワークのノード位置推定手法の提案
- 天気変化を考慮した観光スケジュール群の探索アルゴリズム
- リクエストに応じた交差点映像配信を目的とした車車間通信プロトコルの提案と評価
- VANET における車両の経路情報を利用した情報伝播プロトコルの提案と評価
- すべての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定の高速化手法
- プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明
- プレスブルガー文真僞判定手続きを用いた算術演算回路の正しさの証明
- プレスブルガー文真偽判定手続きにおける多元連立1次合同式の求解処理の高速化
- 交差点鳥瞰映像の協調撮影と共有を目的とした車車間通信プロトコル
- 3D仮想空間を用いた情報家電のためのリモコンフレームワーク
- プログラムの処理速度調整に基づいたデータセンタ向け省電力タスクスケジューリング法
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 出庫予測に基づき入店所要時間を最小化する駐車場ナビゲーションの提案
- ユーザのアクティビティと体重変化履歴に基づいた継続性の高い健康支援手法の提案
- ユーザのアクティビティと体重変化履歴に基づいた継続性の高い健康支援手法の提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 13.B_補酵素関与エタノールアミンアンモニアリアーゼの精密触媒機構と立体化学経路(第423回研究協議会研究発表要旨,ビタミンB研究委員会)
- SumiTag :あまり目立たないARマーカーとGPGPUを利用した読み取り方法
- 過去に観測された品質からのオーバレイリンク品質の推定手法(モバイルコンピューティング,モバイルアプリケーション,ユビキタス通信,モバイルマルチメディア通信及び一般)
- 3Da01 アミド化合物の酵素合成 : 高効率触媒の形成要件(酵素学・酵素工学,一般講演)
- 3Da12 6-アミノヘキサン酸環状二量体加水分解酵素(NylA)の基質結合部位の解析(酵素学・酵素工学,一般講演)
- 2Dp14 ナイロンオリゴマー分解酵素(NylC)の高度耐熱化(酵素学・酵素工学,一般講演)
- 2Dp13 ナイロンオリゴマー加水分解酵素(NylC)の自己分断機構(酵素学・酵素工学,一般講演)
- 穿孔部封鎖処置における歯科用コーンビームCTとマイクロスコープの応用
- ターボブースト・ハイパースレッディングを考慮したマルチコアプロセッサ向けタスクスケジューリング
- 歯内療法領域における歯科用CTを用いた画像診断に関するクリニカルパスの構築
- 12.B_補酵素関与ジオールデヒドラターゼのグリセロールによる不活性化の機構と不活性化抵抗性酵素の再設計(第427回研究協議会研究発表要旨,ビタミンB研究委員会)
- 照明点灯パターンの切り替えによる高精度な屋内位置推定法とその評価(モバイルアドホックネットワーク,モバイル時代を支える次世代無線技術,フィールドセンシング及び一般)
- 4Ca02 ナイロン加水分解酵素(NylC)の耐熱化機構(酵素学,酵素工学/タンパク質工学,一般講演)
- 運転者に対する交通安全支援のための指向性アンテナおよび車車間通信を用いた歩行者の位置推定手法
- 4Ca01 ナイロン加水分解酵素(NylC)前駆体の自己分断に及ぼすアミノ酸置換効果(酵素学,酵素工学/タンパク質工学,一般講演)
- 移動アンカノードを用いた三辺測量による水中センサノードの低コスト位置推定手法
- 2P-045 高解像度X線結晶構造解析を基盤としたナイロン加水分解酵素(NylC)の耐熱化機構の解明(酵素学,酵素工学,一般講演)
- 2P-044 分子動力学シミュレーションによるナイロン加水分解酵素(NylC)の自己分断機構の解析(酵素学,酵素工学,一般講演)
- BalloonNet:無線ネットワークノードを用いた建物包囲型三次元配置手法