Difference between revisions of "TU Wien:Programm- und Systemverifikation VU (diverse)/Temporal Logic"

From VoWi
Jump to navigation Jump to search
m
m
 
(5 intermediate revisions by the same user not shown)
Line 1: Line 1:
 +
== CTL* ==
 +
 +
=== CTL* Pfad Quantoren ===
 
*'''A'''p: Für alle möglichen Pfade gilt p
 
*'''A'''p: Für alle möglichen Pfade gilt p
 
*'''E'''p: Es gibt mindestens einen Pfad für den p gilt
 
*'''E'''p: Es gibt mindestens einen Pfad für den p gilt
wobei p eine CTL Formel ist
+
wobei p eine CTL* Formel ist
 +
 
 +
=== CTL* Operatoren ===
 +
*'''X'''q: Im nächsten Zustand gilt q (''d.h. ne'''X'''t'')
 +
*'''F'''q: Nach beliebig  vielen Schritten gibt es einen Zustand in dem q gilt ''(d.h. irgendwann in der Zukunft - '''F'''uture)''
 +
*'''G'''q: q gilt in jedem (folgenden) Zustand (''d.h. immer - '''G'''lobally'')
 +
*q '''U''' r: q gilt bis r gilt, wobei r irgendwann gelten muss, möglicherweise auch im ersten Zustand (''d.h. '''U'''ntil'')
 +
Die Operatoren beziehen sich immer nur auf genau einen Pfad => ''immer'' bedeutet ''immer auf diesem Pfad''
 +
 
 +
=== Nützliche Kombinationen ===
 +
* '''AG'''q: q gilt auf allen (vom Startzustand aus erreichbaren) Pfaden immer
 +
* '''GF'''q: q gilt unendlich oft
 +
* '''FG'''q: ab einem Zeitpunkt gilt q immer
 +
* '''AF'''q: q gilt schlussendlich, also irgendwann
 +
* '''EF'''q: 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
  
*'''X'''q: Im nächsten Zustand gilt q
+
(Man kann aber auch einen '''A''' Quantor vor die gesamte LTL Formel schreiben)
*'''F'''q: Nach beliebig  vielen Schritten gibt es einen Zustand in dem q gilt
 
*'''G'''q: q gilt in jedem folgenden Zustand
 
*q '''U''' r: q gilt bis r gilt, wobei r irgendwann gelten muss, möglicherweise auch im ersten Zustand
 

Latest revision as of 16:37, 30 July 2020

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)