Como posso comparar dois LTLs para ver se um pode se contradizer? Eu pergunto isso porque tenho uma máquina de estado hierárquica e LTLs que descrevem o comportamento em cada estado. Preciso saber se um LTL local pode contradizer um LTL global. Vi no artigo 'Especificação de recursos e detecção automatizada de conflitos' que duas propriedades LTLs f e g são inconsistentes se a interseção L (f) L (g) estiver vazia. E esta é exatamente a questão de verificação de modelo com f como programa e ¬g como propriedade. Alguém pode me ajudar com isso? Como posso transformar um LTL f em um programa no SPIN / Promela?

Obrigado.