Resumen

La Evaluación Generalizada de Trayectorias Simbólicas (GSTE) es un enfoque de verificación de modelos que ha demostrado con éxito su capacidad poderosa en la verificación formal de sistemas VLSI. GSTE es una extensión de la Evaluación de Trayectorias Simbólicas (STE) para la verificación de propiedades -regulares. Es una alternativa a los algoritmos clásicos de verificación de modelos donde las propiedades se especifican como autómatas finitos. En GSTE, las propiedades se especifican como gráficos de afirmaciones, que son gráficos dirigidos etiquetados donde cada borde está etiquetado con dos funciones de etiquetado: antecedente y consecuente. En este documento, mostramos la relación complementaria entre los gráficos de afirmaciones de GSTE y los autómatas finitos con la expresividad de los lenguajes regulares y -regulares. Presentamos un algoritmo que transforma un gráfico de afirmaciones de GSTE en un autómata finito y viceversa. Al aplicar este algoritmo, transformamos el problema de implicación

• Materias:Modelado matemático Modelo de red neuronal Tasa de convergencia Aritmética Ondículas libres
• Subjects:Mathematical modeling Neural network model Convergence rate Arithmetic Free wavelets
• Palabras claves:Verificación de modelos; GSTE; Evaluación de trayectorias simbólicas; Sistemas VLSI; Grafos de afirmaciones; Autómatas de estado finito
• Keywords:Model checking; GSTE; Symbolic trajectory evaluation; VLSI systems; Assertion graphs; Finite-state automata