Efficient Forward Model Checking Algorithm for ω-Regular Properties (Special Section on VLSI Design and CAD Algorithms)

スポンサーリンク

概要

• 論文の詳細を見る

• We present a symbolic language emptiness check algorithm based on forward state traversal. A verification property is given by a set of error traces written in ω-regular expression and is manipulated explicitly as a non-deterministic state transition graph. State space of the design model is implicitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It should become a good framework of incremental or approximate verification of ω-regular properties.

• 社団法人電子情報通信学会の論文
• 1999-11-25

著者

• Iwashita H

  Fujitsu Laboratories Ltd.

• IWASHITA Hiroaki

  Fujitsu Laboratories Ltd.

• NAKATA Tsuneo

  Fujitsu Laboratories Ltd.

• Nakata T

  Fujitsu Laboratories Ltd.

関連論文

• Efficient Forward Model Checking Algorithm for ω-Regular Properties (Special Section on VLSI Design and CAD Algorithms)
• Integrated Design and Test Assistance for Pipeline Controllers (Special Issue on VLSI Testing and Testable Design)

スポンサーリンク