Resumen

Como técnica complementaria del enfoque basado en BDD, la verificación de modelos acotada (BMC) ha sido aplicada con éxito a la verificación simbólica de modelos LTL. Sin embargo, la expresividad de LTL es bastante limitada y algunas propiedades importantes no pueden ser capturadas por dicha lógica. En este artículo, presentamos un enfoque semántico de codificación BMC para tratar la mezcla de y . Dado que este tipo de lógica temporal involucra tanto autómatas finitos como de bucle como conectivos, todas las propiedades regulares pueden ser especificadas de manera concisa con ella. El algoritmo presentado está integrado en el model checker ENuSMV, y el enfoque es evaluado mediante la realización de una serie de experimentos imperiales.

• 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:Técnica complementaria; Verificación acotada del modelo; Verificación simbólica LTL del modelo; Enfoque de codificación BMC semántica; Lógica temporal; Verificador de modelos
• Keywords:Complementary technique; Bounded model checking; LTL symbolic model checking; Semantic BMC encoding approach; Temporal logic; Model checker