Как я могу сравнить два LTL, чтобы увидеть, если один может противоречить друг другу? Я спрашиваю об этом, потому что у меня есть иерархический конечный автомат и LTL, описывающие поведение в каждом состоянии. Мне нужно знать, может ли локальный LTL противоречить глобальному LTL. В статье «Спецификация характеристик и автоматическое обнаружение конфликтов» я увидел, что два свойства LTL f и g несовместны, если пересечение L (f) L (g) пусто. И это как раз вопрос проверки модели с f в качестве программы и ¬g в качестве свойства. Кто-нибудь может мне с этим помочь? Как я могу превратить LTL f в программу в SPIN / Promela ??

Благодарю.