The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Kami membentangkan algoritma semakan kekosongan bahasa simbolik berdasarkan traversal keadaan hadapan. Sifat pengesahan diberikan oleh satu set jejak ralat yang ditulis dalam ungkapan ω-biasa dan dimanipulasi secara eksplisit sebagai graf peralihan keadaan bukan deterministik. Nyatakan ruang model reka bentuk secara tersirat dilalui sepanjang graf eksplisit. Kaedah ini mempunyai jumlah fleksibiliti yang besar untuk mengawal traversal keadaan pada ruang harta benda. Ia harus menjadi rangka kerja pengesahan tambahan atau anggaran yang baik bagi sifat ω-biasa.
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.
Salinan
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
Salinan
@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},}
Salinan
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 -