IEICE TRANSACTIONS on Fundamentals
Efficient Forward Model Checking Algorithm for ω-Regular Properties
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
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Hiroaki IWASHITA, Tsuneo NAKATA, "Efficient Forward Model Checking Algorithm for ω-Regular Properties" in IEICE TRANSACTIONS on Fundamentals,
vol. E82-A, no. 11, pp. 2448-2454, November 1999, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e82-a_11_2448/_p
Copy
@ARTICLE{e82-a_11_2448,
author={Hiroaki IWASHITA, Tsuneo NAKATA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Efficient Forward Model Checking Algorithm for ω-Regular Properties},
year={1999},
volume={E82-A},
number={11},
pages={2448-2454},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - Efficient Forward Model Checking Algorithm for ω-Regular Properties
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2448
EP - 2454
AU - Hiroaki IWASHITA
AU - Tsuneo NAKATA
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E82-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 1999
AB - 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.
ER -
English
