Resumen

El costo de la verificación de modelos LTL es altamente sensible a la longitud de la fórmula bajo verificación. Observamos que, bajo algunas condiciones específicas, la fórmula LTL de entrada puede ser reducida a una más fácil de manejar antes de la verificación del modelo. En dicha reducción, estas dos fórmulas no necesitan ser lógicamente equivalentes, pero comparten el mismo conjunto de contraejemplos con respecto al modelo. En el caso de que el modelo esté representado simbólicamente, la condición que permite tal reducción puede ser detectada con un esfuerzo ligero (por ejemplo, con SAT-solving). En este artículo, tentativamente nombramos a esta técnica como reducción preservadora de contraejemplos (CPR, por sus siglas en inglés), y la técnica propuesta es evaluada mediante la realización de experimentos comparativos de verificación de modelos basada en BDD, verificación de modelos acotada y verificación de modelos basada en alcanzabilidad dirigida por propiedades (IC3).

• Materias:Modelos matemáticos Conjuntos difusos Ecuaciones integrales Fusión de características Algoritmo de optimización
• Subjects:Mathematical models Fuzzy sets Integral equations Feature fusion Optimization algorithm
• Palabras claves:Verificación de modelos; Fórmula LTL; Reducción; Contraejemplo; Representación simbólica; Técnica CPR
• Keywords:Model checking; LTL formula; Reduction; Counterexample; Symbolic representation; CPR technique