The search functionality is under construction.
The search functionality is under construction.

Efficient Forward Model Checking Algorithm for ω-Regular Properties

Hiroaki IWASHITA, Tsuneo NAKATA

  • Full Text Views

    0

  • Cite this

Summary :

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.

Publication
IEICE TRANSACTIONS on Fundamentals Vol.E82-A No.11 pp.2448-2454
Publication Date
1999/11/25
Publicized
Online ISSN
DOI
Type of Manuscript
Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category

Authors

Keyword