Temporale Logiken: CTL Flashcards
(6 cards)
Syntax von CTL (Skript 135)
Die Formeln von CTL (“computational tree logic” oder auch “branching time temporal logic”)
sind induktiv definiert wie folgt:
- Alle aussagenlogischen Formeln über {P_i : i element I} gehören zu CTL.
- CTL ist abgeschlossen unter den Booleschen Operatoren und, oder, impliziert, nicht.
- Wenn psi, phi element CTL, dann sind auch die Asudrücke EXpsi, AXpsi, E(psi U phi) und A(psi U phi) Formeln von CTL.
Die Intuition bei der Modellbeziehung ist folgende: Sei K~ ein Transitionssystem und v ein Zustand von K~. Dann quantifizieren E und A über unendliche Pfade v= v_0 v_1 v_2 … in K~, welche bei v beginnen und auf denen die temporalen Operatoren dann ausgewertet werden.
Semantik von CTL (Skript 135)
Sei K~ = (V, E, (P_i)i element I) eine Kripkestruktur und v element V. Dann gilt:
- EXpsi logisch äq. <>psi;
- AXpsi logisch äq. []psi;
-Es gilt K~,v |= E(psi U phi), wenn ein Pfad v_0 v_1 … mit v=v_0 und ein n >= 0 existiert, so dass K~,v_n |= phi und K~,v_m |= psi für alle m mit 0 <=m
Wichtige Abkürzungen EFpsi, AFpsi, EGpsi, AGpsi
Analog zu LTL:
EFpsi := E(1 U psi) ex. ein Pfad, auf dem irgendwann psi gilt
AFpsi := A(1 U psi) auf allen Pfaden gilt irgendwann psi
EGpsi := nicht AF nicht psi (ex. ein Pfad, auf dem immer psi gilt)
AGpsi := nicht EF nicht psi (auf allen Pfaden gilt immer psi)
Wie schnell können CTL-Formeln ausgewertet werden?
Satz 5.29
CTL-Formeln können effizient ausgewertet werden (in linearer Zeit sowohl bezüglich der Länge der Formel wie der Größe des Transitionssystems)
Satz 5.29: Es gibt einen Algorithmus, welcher zu einem gegebenen ___endlichen___ Transitionssystem K~ und einer Formel psi element CTl in Zeit O( ||K~|| * |psi|) die Extension [[psi]]^K berechnet
Zwei weitere wichtige Fakten zu CTL
CTL hat die Endliche-Modell-Eigenschaft
Das Erfüllbarkeitsproblem für CTL ist entscheidbar (in exponentieller Zeit)
Ist CTL einbettbar in FO?
Im Gegensatz zu ML kann CTL ___nicht___ in FO eingebettet werden
