Temporale Logiken: LTL

Question 1

Syntax von LTL

Answer 1

LTL ( “linear time temporal logic”):

Die Formeln von LTL sind induktiv wie folgt definiert:

• Alle aussagenlogischen Formeln über {P_i : i element I} gehören zu LTL
• LTL ist abgeschlossen unter den Booleschen Operatoren und, oder, impliziert, nicht.
• wenn phi, psi element LTL, dann sind auch die Ausdrücke Xpsi und (phi U psi) Formeln von LTL

LTL wird wie ML an einzelnen Punkten ausgewertet. Der Ausdruck Xpsi (“next psi”) bedeutet, dass am unmittelbar folgenden Element v_i+1 die Formel psi gilt, und der Ausdruck psi U phi (“psi until phi”) besagt, dass an irgendeinem “späteren” Element v_n phi gilt, und davor immer psi wahr ist.

Question 2

Definition 5.23 (Skript 132) Semantik von LTL

Answer 2

Sei W~ eine endliche oder unendliche Folge von ELementen v_0, .., v_n-1 oder v_0v_1 …. und atomaren Relationen P_i für i element I. Die Bedeutung der Formeln P_i und der aussagenlogischen Junktoren ist auf die übliche Weise definiert. Ausserdem gilt:

• W~, v_i |= Xpsi genau dann, wenn v_i nicht das letzte Element von W~ ist und W, v_i+1 |= psi;
• W~, v_i |= (psi U phi), wenn ein n >= i existiert, so dass W~, v_n |= phi und W~, v_m |= psi für alle m mit i <=m < n

Question 3

Notation. Zwei wichtige Abkürzungen F, G

Answer 3

Fpsi := (1 U psi) (irgendwann wird psi gelten)

Gpsi := nicht F nicht psi (immer wird psi gelten)

Question 4

Satz 5.25: äquivalente FO-Formeln

Answer 4

Zu jeder LTL-Formel psi existiert eine FO-Formel psi*(x) der Signatur {