Einleitung

wie überall,

• Trennung von Spezifikation und Implementierung
• jeweils ein mathematisches Modell
• Sätze über Eigenschaften, Beziehungen dieser Modelle
• Algorithmen zur Beantwortung der Frage:
  erfüllt die Implementierung die Spezifikation?

so auch hier:

• Spezifikation: PLTL (propositional linear time logic)
• Implementierung: Omega-Wörter, -Sprachen, -Automaten