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
Apresentamos um algoritmo de verificação de vazio de linguagem simbólica baseado na travessia de estado direto. Uma propriedade de verificação é dada por um conjunto de traços de erro escritos em expressão regular ω e é manipulada explicitamente como um gráfico de transição de estado não determinístico. O espaço de estados do modelo de design é percorrido implicitamente ao longo do gráfico explícito. Este método tem uma grande flexibilidade para controlar a passagem de estado no espaço de propriedades. Deve tornar-se uma boa estrutura de verificação incremental ou aproximada de propriedades ω-regulares.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -