== Beziehungen zu anderen Logiken == == Automata theoretic Linear temporal logic model checking == Ein wichtiger Weg zur Modellprüfung besteht darin, die gewünschten Eigenschaften (wie oben beschrieben) mit LTL-Operatoren auszudrücken und dann zu überprüfen, ob das Modell diese Eigenschaften erfüllt. Ferner ist es möglich, einen zum Modell...