Resumen

Este trabajo presenta una solución eficiente utilizando un sistema de álgebra computacional para realizar la verificación de propiedades temporales lineales para sistemas digitales síncronos. El método se basa esencialmente en enfoques de bases de Groebner y simulación simbólica. Se estudia un mecanismo para construir representaciones simbólicas basadas en conjuntos de polinomios canónicos tanto para descripciones de circuitos como para afirmaciones. Luego presentamos un marco de algoritmo de verificación completo basado en estas representaciones algebraicas utilizando bases de Groebner. Los resultados de la experiencia computacional en este trabajo muestran que el enfoque algebraico es un método de verificación bastante competitivo y será un complemento útil a los métodos de verificación existentes basados en simulació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:Solución eficiente; Sistema de álgebra computacional; Verificación de propiedades temporales lineales; Sistemas digitales síncronos; Bases de Groebner; Simulación simbólica
• Keywords:Efficient solution; Computer algebra system; Linear temporal properties verification; Synchronous digital systems; Groebner bases; Symbolic simulation