Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2006-01-12 Ü 11

Mitschrift von Robert Noll
(Noch ergänzt um Korrektheitsbeweis von kleinstem Fixpunkt)


Computational Tree Logic
========================

C ::= P | EX phi | AX phi |
         EG phi | AG phi |
         EF phi | AF phi |

EX : E:exists A:all  X:next, G:globally, F:finally

       S0 (pq)
   <-->        -->
S1         ---->     S2 (r)  --> s2

nicht grafisch : S0 <--> S1 ; S0 -> S2 ; S1 -> S2 ; S2 -> S2
wobei -> zustandsübergang bedeutet

s0 |= p /\ q
s0 |= EX ( p /\ q )    // wahr wegen s0 -> s1 und s1 (p/\q)

frage : gilt
s0 |= AX (q/\r)  falsch wege s0 -> s2 und in s2 gilt nur r
also gilt :   ( ~ heisst not )
s0 |= ~ AX ( q /\ r)

frage :
s0 |= EF (p/\r)  // existiert irgendein nachfolgezustand, in dem p und r gelten.
falsch, da si |= p /\ r für alle si  : es gibt überhauptkeinen zustand in dem q und r gelten

frage :
s0 |= AG ( r )  falsch, da (nicht s0 |= r), und auch wege der länge 0 für G gelten (alle folgezustände, auch der anfangszustand)

s2 |= Ag ( r )
wahr, man kommt nicht mehr von s2 weg

s1,s2 |= EG ( r )  wahr, wenn man nach s2 geht

s0,s1,s2 |= AF (r)
finally : wenn ich vor dem erreichen von r in einer endlosschleiffe hängen bleiben kann, gilt AF nicht.
es genügt es irgendwann erreichen zu müssen auf jedem pfad, man muss nicht drauf bleiben.

=== FAIR ===

Fair für r
"auf jedem unendlichen pfad gilt r unendlich oft"

AF r
fair r = AF ( r /\ AX fair r)  //  auf jedem pfad kommt irgendwann r nach endlich vielen schritten, und auf jedem folgepfad kommt es auch wieder nach endlich vielen schritten

AG.p = p /\ AX ( AG p)
Fair r = AG(AF r) !!!!   // heisst: auf allen pfaden unendlich oft
AF(AG r) // (stärker als fair, impliziert fairness), heisst : man kommt irgendwann in schleiffe rein, in der r immer gilt


[Ab hier modifiziert von Andreas Abel:]

Fixpunkte
=========

fixpunkt : grösste und kleinste lösung : macht nur sinn wenn man ordnung auf elementen hat (wenn man "im verband" ist)

Bsp1:
fi ( M ) =  M u { 0 }
<= heisst [teilmenge oder gleich]
FP heisst FixPunkt
"u" heisst Vereinigung
|N  : nat.zahlen
fi monoton:  A <= B impliziert fi (A) = A u {0} <= B u {0} = fi (B)
ges : F mit fi (F) = F
   => 0 element F
   kleinster FP : {0}
   groesster FP : |N  
Bestimmung durch Iteration:
kl.FP : {}, fi({}), fi(fi({})) ,,,
              {0} , {0}, ...
gr.FP :  |N, fi(|N) = |N

Bsp2:
fi (M) = M \ {0}
kl.FP = {}
gr.FP = |N \ {0}

Bsp3:
fi (M) = {1} u 2 * M
man überlegt sich, dass das monoton ist.
kl.FP : {},{1},{1,2},{1,2,4},{1,2,4,8} ...
kl.FP = {2^i | i element |N }
   =         U       fi ^ i ( {} )           // U heisst vereinigung
       i element |N
       gr.FP :  |N , {1} u 2*|N , {1,2} u 4|N , {1,2,4} u 8|N ...
   =       |^|       fi ^ i ( |N )           // |^| heisst schnittmenge 
       i element |N                          // (kommt am ehesten an ein 
                                             // umgedrehtes U ran)
(grösster und kleinster FP fallen zusammen)

Nimmt man als Grundmenge statt |N die Menge
       
   |N u { unendlich }

dann ist der kl.FP wie vorher, aber der gr.FP enthält zusätzlich das
Element unendlich.  


Definition kleinster Fixpunkt
-----------------------------

M, Menge ,   fi : M -> M monoton
A <= B => fi(A) <= fi(B)           // <= bedeuted teilmenge
F = |^| { Q <= M | fi(Q) <= Q }    // |^| heisst schnittmenge

Theorem: F kleinster FP von fi

Beweis: Wir zeigen
i) fi(F) = F
ii) fi(Q) <= Q  => F <= Q

i) a) zz: fi (F) <= F
      dh: fi (F) <= |^| {Q <= M | fi (Q) <= Q}
       sei fi(Q) <= Q  [vorraussetzung 1]
       zeige fi(F) <= Q
       wir wissen F <= Q  (weil F aus dem schnitt aller Q ensteht)
       fi monoton => fi(F) <= fi(Q) <=[wegen vorraussetzung 1] Q  

ii) Da fi(Q) <= Q nach Annahme, ist Q in der Menge {Q<=M | fi(Q) <= Q}
    Also gilt für den Schnitt F über alle Elemente dieser Menge: F <= Q.

i) b) zz: F <= fi(F)
      Wir verwenden ii) mit Q := fi(F).  Es genügt zu zeigen, dass
        fi(fi(F)) <= fi(F).  Das folgt aber aus i) a) mit Monotonie von fi.
Qed.