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

From VoWi
Jump to navigation Jump to search

CTL*[edit]

CTL* Pfad Quantoren[edit]

  • 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[edit]

  • 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[edit]

  • 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[edit]

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

ACTL*[edit]

Wie CTL* ohne E Quantor

ACTL[edit]

Kombination aus CTL und ACTL*

=> vor jedem Operator steht ein A Quantor

LTL[edit]

Erlaubt keine Pfad-Quantoren

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