TU Wien:Programm- und Systemverifikation VU (diverse)/Temporal Logic

CTL*

CTL* Pfad Quantoren

• Ap: Für alle möglichen Pfade gilt p
• Ep: Es gibt mindestens einen Pfad für den p gilt

wobei p eine CTL* Formel ist

CTL* Operatoren

• Xq: Im nächsten Zustand gilt q (d.h. neXt)
• Fq: Nach beliebig vielen Schritten gibt es einen Zustand in dem q gilt (d.h. irgendwann in der Zukunft - Future)
• Gq: q gilt in jedem (folgenden) Zustand (d.h. immer - Globally)
• q U r: q gilt bis r gilt, wobei r irgendwann gelten muss, möglicherweise auch im ersten Zustand (d.h. Until)

Die Operatoren beziehen sich immer nur auf genau einen Pfad => immer bedeutet immer auf diesem Pfad

Nützliche Kombinationen

• AGq: q gilt auf allen (vom Startzustand aus erreichbaren) Pfaden immer
• GFq: q gilt unendlich oft
• FGq: ab einem Zeitpunkt gilt q immer
• AFq: q gilt schlussendlich, also irgendwann
• EFq: es ist möglich, dass q gelten wird

CTL

Wie CTL* nur, dass die Quantoren und Operatoren immer nur Paarweise auftreten können.

ACTL*

Wie CTL* ohne E Quantor

ACTL

Kombination aus CTL und ACTL*

=> vor jedem Operator steht ein A Quantor

LTL

Erlaubt keine Pfad-Quantoren

(Man kann aber auch einen A Quantor vor die gesamte LTL Formel schreiben)