Wie kann ich zwei LTLs vergleichen, um festzustellen, ob sich eine widersprechen kann? Ich frage dies, weil ich eine hierarchische Zustandsmaschine und LTLs habe, die das Verhalten in jedem Zustand beschreiben. Ich muss wissen, ob eine lokale LTL einer globalen LTL widersprechen kann. Ich habe im Artikel 'Feature Specification and Automated Conflict Detection' gesehen, dass zwei LTL-Eigenschaften f und g inkonsistent sind, wenn L (f) intersection L (g) leer ist. Und das ist genau die Frage der Modellprüfung mit f als Programm und ¬g als Eigenschaft. Kann mir jemand dabei helfen? Wie kann ich eine LTL f in ein Programm in SPIN / Promela umwandel

Vielen Dank