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.
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.
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 -