形式的設計検証のための分岐時間正則時相論理
スポンサーリンク
概要
- 論文の詳細を見る
論理設計の多様化,複雑化にともない,設計が正しいことを示すための検証手法の確立が重要な課題となっている.対象を順序機械などの有限状態の機械ととらえたとき,設計が仕様を満足するかどうかを厳密に示すために,命題時相論理によって仕棟を記述し,モデル検査アルゴリズムを適用する手法が提案されている.命題時相論理には種々の体系が存在するが,このうちClarkeらによって提唱されたCTL(Computational Tree Logic)では,有限状態機械の動作を反映するKripke構造Sの大きさ(Size(S))と時相論理式fの長さ(Len(f))の積に対し線形時間でモデル検査を行うことができ,順序機械,通信プロトコルなどの検証に応用されてきている.しかし,本輪文で示すように,CTLは事象の繰り返しなどの性質を記述できないといった問題点があり,有限状態機械の仕様の記述に用いることを考えた場合,十分な表現力を持つとは言えない.そこで本論文ではCTLと比べ真に高い表現能力を持つ分岐時間正則時相論理(Branching time RegularTemporal Logic,BRTL)を提案する.またそのモデル検査アルゴリズムを示し,その時間計算量がCTLの場合と同じく,Size(S)とLen(f)の積に比例することを証明する.
- 一般社団法人情報処理学会の論文
- 1992-04-15
著者
-
平石 裕実
京都産業大学工学部情報通信工学科
-
矢島 脩三
京都大学工学部情報工学教室
-
濱口 清治
京都大学工学部
-
矢島 脩三
京都大学大学院工学研究科情報工学教室
-
濱口 清治
大阪大学大学院基礎工学研究科
-
平石 裕実
京都産業大学
-
矢島 脩三
京都大学工学研究科情報工学専攻
関連論文
- 有限オートマトンと表現等価な正則時相論理とその論理設計検証への応用
- 正則時相論理のモデルチェック法の改良と設計検証への適用
- 連想メモリを利用したハードウェア向き単一化アルゴリズム
- 連想メモリを利用した高速単一化アルゴリズム
- 入力制約監視機能をもつ会話型シミュレーション・システムISS
- 京都大学情報処理教育センターの概要
- 複数の二分決定グラフを用いたNP完全な組合せ問題の解法
- 2)超高精細マルチ画像顕微鏡装置の開発(ヒューマンインフォメーション研究会)
- 超高精細マルチ画像顕微鏡装置の開発
- 関係データベースにおける意味制約を反映した非正規形の関係の設計問題
- データベースにおける非正規関係の設計と操作について(モデル表現とその構築に関する理論と実際の研究)
- 関係データベースシステムにおける従属性を利用したデータの表現について (形式言語理論とオートマトン理論)
- 関係データベースシステムにおける質問作成・改良の補助機能をもつ利用者インタフェースの設計と開発 (情報の記憶と利用に関する理論的研究)
- 文献情報処理のためのMULTI-KWICシステム
- 積和形論理式を表す二分決定グラフの表現能力(アルゴリズムと計算量理論)
- 積和形論理式を表す二分決定グラフの表現能力
- しきい値関数を表す共有2分決定グラフの最適な変数順序付けの計算複雑度
- 等号を含む第一階時相論理のサブクラスとその恒真性判定問題
- 等号を含む第一階時相論理のサブクラスとその恒真性判定問題(計算モデルと計算の複雑さに関する研究)
- 二分モーメントグラフを用いた大規模多項式の操作手法
- 形式的手法によるキャッシュ・プロトコルの設計検証 : 超並列計算機JUMP-1への適用例
- 算術演算回路検証のための二分モーメントグラフの高速生成手法
- 算術演算回路検証のための二分モーメントグラフの高速生成手法
- 設計検証技術(総論) : 現在の設計検証技術はペンティアムのバグを見つけることができるか
- 形式的設計検証のための分岐時間正則時相論理
- 時相論理と言語階層の対応関係について(計算および計算量理論とその周辺)
- 有限オートマトンと表現等価な正則時相論理とその論理設計検証への応用
- 線形時間のモデルチェックアルゴリズムを持つ正則時相論理と変数代入機構による拡張
- On Design Varification between Different Levels of Abstraction Using Regular Temporal Logic
- 正則時相論理の充足可能性判定アルゴリズム
- 高度情報環境におけるプライベート仮想ライブラリ
- 高度情報環境におけるプライベード仮想ライブラリに関する考察
- 乗算型除算および開平のためのハードウェアによる初期近似手法
- 除算と開平のための積和演算を用いた初期近似手法
- 連分数展開に基づく高速開平アルゴリズム
- テンポラル・ロジックで用いられている連接について(アルゴリズムの数学的基礎理論とその応用)
- 論理回路機能の時間的関係の記述と検証(計算機科学の基礎理論とその応用)
- 入力制約を用いた論理回路の形式的検証について(計算機科学の基礎理論)
- 不完全指定順序機械の非両立状態対の割合について (情報科学の数学的基礎理論と応用)
- 仕様が漸化式で与えられた組含せ回路の形式的設計検証
- 二次記憶に格納された共有二分決定グラフを効率良く処理するための幅優先アルゴリズム
- 共有展開に基づくベクトル計算機向き論理関数素項生成法
- ディスプレイ上における文字表示環境の自動最適化について
- プール式処理による不完全指定順序機械の最小化
- マルチコンピュータ・マルチスクリーン・グラフィクス・システム(MCMSシステム)の論理シンボル入力/編集
- 冗長2進表現を用いた右シフト剰余除算のハードウェアアルゴリズム
- 記憶階層のもとでの結合操作について (数理情報科学の基礎理論と応用)
- 部分自律有限オートマトンの等価性 (情報科学の数学的基礎理論と応用)
- 2入出カ対オートマトンによる計算機結合インタフェースの設計手順 (計算機構の数学的研究)
- 除算を表現する二分決定グラフの指数下界
- 共有二分決定グラフを用いた論理回路の多重故障シミュレ一ション
- スライス関数と斉次関数の回路計算複雑さについて
- Representability Problem for Relational Database Design with Multivalued Dependencies (情報科学の数学的基礎理論と応用)
- Query Processing in a Relational Database Using Abstracted Characteristics of Data (情報科学の数学的基礎理論と応用)
- 算術演算回路検証のための二分モーメントグラフの高速生成手法
- 時間記号シミュレーションについて
- 乗除べき乗算のための段数 O((1-α)/α n)) 素子数 O((n^)/(αlogn))回路
- O(n)段剰余べき乗算回路
- 機能メモリを用いたDCTハードウェアアルゴリズム
- SBDDを用いた最小STT状態割当
- SBDDを用いた最小単符号単発状態割当
- 有向非巡回グラフの線形配置アルゴリズムについて
- 高速シミュレータを用いた重み付き乱数によるテスト生成
- 高速故障シミュレータを用いたテスト生成
- ベクトル計算機による高速故障シミュレーションのための動的二次元並列法
- しきい値関数を表す二分決定グラフのサイズと変数順序
- 閾値関数を表す2分決定グラフの変数順序と重みの順序の関係
- 基本操作の依存性を利用した並行処理のための手法(計算機構に関する数学的基礎理論とその応用)
- On the Size of Ordered Binary Decision Diagrams Representing Threshold Functions
- しきい値関数を表現する二分決定グラフの大きさの下界
- マルチコンピュータ・マルチスクリーン・グラフィクスワークステーションの開発
- A New Automaton Model Suitable for Maximal Common Substring Computation and Its Application to Data Compression (Mathematical Studies of Information Processing)
- 最大共通部分系列問題と共通連続部分系列問題のアルゴリズム (情報科学の数学的基礎理論と応用)
- 不成功マッチング処理に適した部分マッチングアルゴリズム (計算機科学の数学的基礎)
- On Tree-Shellable Boolean Functions
- 並列分枝限定法と動的探索木分割によるクラスタシステム向き最適順序付けアルゴリズム(アルゴリズム)
- 通信状態の可視化によるメッセージ通信型並列プログラムのデバッグ支援ツール
- クラスタシステムにおける並列バイトニックソートの性能評価
- Verification of Deadlock Free Property of Asynchronous Robot Control Programs
- 情報技術革命を支える高性能・高効率計算システムの研究
- 平成13年度活動概要
- HRクラスタシステムガイド(ハイテクリサーチプロジェクト)
- 静的部分問題割り当てに基づくN-queen問題の並列アルゴリズム
- 形式的論理設計検証の研究
- 形式的論理設計検証の研究
- 記号モデル検証システムSMVにおける像計算 (テストと設計検証論文特集)
- タスク制御アーキテクチャ入力支援システム
- 形式的論理設計検証およびメッセージ書換型プロキシサーバーの研究
- メッセージ書換型プロキシサーバの研究開発
- 形式的論理設計検証に関する研究
- 順序回路検証の技術
- 2進乱数の改善およびその改善度について
- ハードウェアアルゴリズムの記述法について (形式言語理論とオートマトン理論)
- 非決定性有限オートマトンの状態数最小化(理論計算機科学とその周辺)
- 論理回路の故障の自律検査法 (情報科学の数学的基礎理論と応用)
- 近接関数を用いた多出力論理関数の最小化について
- 論理式と二分決定グラフの表現能力の比較
- Tree-Shellable論理関数について
- 種々のShellable関数の関係について
- 確率的符号化時間記号シミュレーションによるタイミングエラー確率の解析