有限状態機械に対する形式的検証
スポンサーリンク
概要
- 論文の詳細を見る
近年の論理回路の大規模化や多様化にともない、設計された実装が、与えられた仕様を満足するかどうかを完全に保証するための形式的検証はますます重要になってきている。本稿では順序回路を対象とした形式的検証のうち、順序回路を有限状態機械(以下 FSM)で記述し等価を判定する検証手法を取り上げ、基本アルゴリズムとその改善方法について述べる。ここで用いるFSMを < S,I,O,N,Out,Init >で定義する。ただし、Sは内部状態の集合、Iは入力記号の集合、Oは出力記号の集号、Nは状態遷移関数、Outは出力関数、Initは初期状態である。FSMの2つの状態s_iとs_jが同値であるというのは、s_iまたはs_jのどちらを初期状態としても、全ての入力系列に対して出力系列が等しい場合をいう。
- 社団法人電子情報通信学会の論文
- 1997-03-06
著者
関連論文
- 競合状況における投機的計算の導入に関する考察(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- 一般節理論における解釈からの学習に関する一考察(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- 複数のロバスト仕様をみたすPID制御器の設計
- ロボットの動的制御における計算の並列化問題に対する最適化および準最適化アルゴリズム
- 非凸多角形区間演算とそのインプリメント
- 最適化コンパイラによるロボット制御プログラムの開発
- ある種のマルチDSPシステムにおける多目的最適化問題に対する分枝限定法の適用
- 可変近傍探索法による三電極SAWフィルタの最適化設計
- アフォーダンス理論に基づく知能ロボットの創発 : 身体の形状と環境
- 手先コンプライアンスを考慮した冗長アームの最適姿勢問題とその区間解析による解法
- 今西進化論に基づく遺伝アルゴリズムによるモジュール配置問題の多様な最適解の探索
- 今西進化論に基づく遺伝アルゴリズムによる多様なパレート最適解の抽出法 - 多目的資源分割問題を実例として -
- 高速区間二分法による非線形方程式の全解探索とロボットアームの逆運動学問題への適用
- GKSを用いたマルチスクリーン・マルチウィンドウグラフィックスシステム
- パーソナルコンピュータを利用した電気回路解析用CADグラフィックスシステム
- 大学の国際化とメディア利用の展望 : 大学・機関における国際学術・教育交流活動の実態および関心調査から
- 遺伝的アルゴリズムとアフォーダンスを用いた知能ロボットの創発
- 有限状態機械に対する形式的検証
- 距離に基づく遺伝アルゴリズムの構築法 -表現型の距離と調和交叉法-
- 巡回セールスマン問題に対する遺伝的アルゴリズムの構成法 : 表現型の距離と調和交叉法
- 正則表現論理シミュレ-ション手法に基づく非同期順序回路の検証
- 凸多面体リヤプノフ関数を用いた複合系の安定解析II
- 動的凸包算法の高速化
- 凸多面体リヤプノフ関数を用いた複合系の安定解析
- 二分決定グラフの並列構成アルゴリズムについて(理論計算機科学とその周辺)
- ロボットの逆動力学計算に対する最適化システム
- ロボット制御則の並列化問題に対する遺伝アルゴリズムの適用
- ロボット制御則の並列化問題に対する重み付きエッジ交叉法
- 多角形区間演算を用いたゲイン余裕の算出
- ある種のマルチDSPシステムのスケジューリング問題に対する最適化アルゴリズム
- ロボットの動的制御における計算の並列化アルゴリズムとオブジェクト指向による実現
- SA-1-8 多角形区間演算を用いたロバスト制御系の解析・設計(SA-1. 区間演算の工学的応用,シンポジウム)
- 多角形区間演算のロバスト根軌跡法への適用
- リヤプノフ関数の自動生成と安定領域の推定
- ハイブリッドシミュレータを用いたδ差分実現によるEMM制御系の評価
- 多角形区間演算の改良と不確かさを含む伝達関数の値集合の推定 (電気関連学会関西支部連合大会)
- 多角形区間演算を用いた不確かさをもつむだ時間制御系の安定度の解析 (ロバスト制御と適応制御--不確かさをもつ対象の制御)
- 非線形周期解の存在と安定性について
- 遺伝アルゴリズムを枠組としたメタ戦略の構築法-グラフ彩色問題を実例として-
- 操作力を考慮した人工腕の最適姿勢問題と区間解析による大域的最適化
- ロボット制御則の並列処理におけるタスクの自動生成手法 -数式の代数的変換による並列化-
- デフォルト規則を含む拡張論理プログラムの学習
- 非共有記憶型並列計算機上での二分決定グラフの並列化とその応用
- SATソルバと後ろ向き推論によるアクション言語Αの実装
- 随伴回路を用いたサイリスタ回路の定常解析と汎用定常解析プログラムANASPについて
- 正則表現論理シミュレータの実現について
- 平成2年産業応用部門全国大会
- アクション言語Aにおける行動規則の学習
- 非決定性アクション言語NA上のプランニング手続き
- 投機的計算を行う協調型マルチエージェントシステムの構築に関する一手法 (小特集 使えるAI基礎技術)
- ユーザの嗜好を取り入れた文書評価を行うWeb上の情報検索 (小特集 使えるAI基礎技術)
- 補題の利用による効率的なSOL導出の実現
- SATソルバによるアクション言語処理系の実装
- SATソルバによるアクション言語処理系の実装
- 有限オートマトンに基づく非決定性アクション言語
- マルチDSPシステムによるスループット時間が最短であるディジタル制御器の実現
- 非線形等価電気回路による直流法潮流計算と潮流最適化
- 論理回路シミュレータの入出力インタフェースについて
- 拡張した記述関数法によるサイリスタ回路の解析
- タブロ-法によるサイリスタ回路のディジタルシミュレ-ション
- 拡張論理プログラム学習へのトップダウン手続きの組込み
- Java言語によるアクション言語処理系の実装
- アクション言語Aにおける因果関係の学習
- 新仮説の発見を含むアブダクティブ理論プログラムの学習
- アクション言語における非決定性アクションの表現と推論に関する考察
- 共有記憶型並列計算機上での共有二分決定グラフの並列化について
- ゲートレベル論理回路の閉路の切断について
- 系列集合と時間の階層の関係について(計算アルゴリズムと計算量の基礎理論)
- 論理回路における閉路の切断について(計算アルゴリズムの基礎理論)
- タイミング検証に適した系列集合論理シミュレータについて
- タブロ-法を用いたブロック線図系のシミュレ-ションと感度解析によるパラメ-タ最適化
- タブロ-法について
- Local Theorems on the Convergence of Equilibrium Solution Methods Based on Componentwise Inequalities
- 領域の演算上に関する性質と線形系の軌道誤差の評価法に関する考察
- 線形時間不変系における自由振動と周期解について
- ベクトル形不等式に関する諸性質とダイナミカルシステムの過渡応答評価と非負性について
- 平衡点方程式における数値計算法のベクトル形不等式による解析
- A Note on the Convergence of Steepent-Gradient Algorithm for Piecewise-Quadratic Functionals
- μ-functional on Bounded Linear Operators