La terminación o detención es un requisito importante del sistema que muchos sistemas deben satisfacer y se puede expresar en lógica temporal lineal como propiedades eventuales. Diseñamos un enfoque de divide y vencerás para la verificación de modelos eventual con el fin de reducir la explosión del espacio de estados en la verificación de modelos. La idea de la técnica es dividir un problema original de verificación de modelos para propiedades eventuales en múltiples problemas de verificación de modelos más pequeños y manejar cada uno de ellos. Debido a la naturaleza del enfoque de divide y vencerás, cada problema de verificación de modelos más pequeño puede abordarse esencialmente de manera independiente. Por lo tanto, este artículo propone una técnica/herramienta paralela basada en un patrón maestro-trabajador para el enfoque de divide y vencerás en la verificación de propiedades eventuales. Realizamos algunos experimentos para mostrar la efectividad de nuestra técnica/herramienta paralela, que puede mejorar en cierta medida el rendimiento durante la verificación de modelos para propiedades eventuales.