¿Cómo puedo comparar dos LTL para ver si uno puede contradecirse? Pregunto esto porque tengo una máquina de estados jerárquica y LTL que describen el comportamiento en cada estado. Necesito saber si un LTL local puede contradecir un LTL global. Vi en el artículo 'Especificación de características y detección automatizada de conflictos' que dos propiedades LTL f y g son inconsistentes si la intersección L (f) L (g) está vacía. Y esta es exactamente la pregunta de verificación del modelo con f como programa y ¬g como propiedad. Puede alguien ayudarme con esto? ¿Cómo puedo transformar un LTL f en un programa en SPIN / Promela?

Gracias.