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

From VoWi
Jump to navigation Jump to search
(LT Übersicht angefangen)
 
m
Line 1: Line 1:
*Ap: Für alle möglichen Pfade gilt p
+
*'''A'''p: Für alle möglichen Pfade gilt p
*Ep: 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
  
*Xq: Im nächsten Zustand gilt q
+
*'''X'''q: Im nächsten Zustand gilt q
*Fq: Nach beliebig  vielen Schritten gibt es einen Zustand in dem q gilt
+
*'''F'''q: Nach beliebig  vielen Schritten gibt es einen Zustand in dem q gilt
*Gq: q gilt in jedem folgenden Zustand
+
*'''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
+
*q '''U''' r: q gilt bis r gilt, wobei r irgendwann gelten muss, möglicherweise auch im ersten Zustand

Revision as of 14:54, 30 July 2020

  • 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

  • Xq: Im nächsten Zustand gilt q
  • Fq: Nach beliebig vielen Schritten gibt es einen Zustand in dem q gilt
  • Gq: 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