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

From VoWi
Jump to navigation Jump to search
(LT Übersicht angefangen)
(No difference)

Revision as of 14:53, 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