Rechnergestütztes Beweisen (Hofmann, WS 2005/06) 2006-01-11 VL 21 Model checking und PVS ====================== Model checking: Gegeben eine Formel phi und eine Interpretation II, wobei |II(tau)| endlich für alle Typen tau. Stelle fest, ob II |= phi, d.h., [|phi|]_II = tt. Falls phi Formel der erststufigen Logik, so liefert die Definition [|phi|] ein Entscheidungsverfahren, welches polynomiell in n:=|II(tau)| ist (der Grad des Polynoms hängt von der Anzahl der Quantoren ab). Genauer O(n^(Quantorentiefe von phi)). Warum ist Gültigkeit von Formeln in einem endlichen Modell überhaupt interessant? Oft lassen sich Eigenschaften von Programmen, Protokollen, verteilten Systemen als Model-checking-Problem auffassen, falls es sich um Systeme mit endlichem Zustand handelt. * Der Aufzug bewegt sich nicht, wenn die Tür offen ist. * Protokoll X verhindert Deadlocks. Beispiel: section : TYPE = { idle, wait, critical } semaphore : TYPE = { vacant, occupied } state : TYPE = [# pc1:section, pc2:section, sem:semaphore #] |state| = 18 Prozesszyklus: sem=vacant idle -----------> wait --------------> critical ------------> idle sem:=occupied sem:=vacant Das Verhalten des Systems wird durch folgende Relation modelliert: N(s1,s2:state) = s1`pc1=idle AND s2 = s1 WITH [pc1:=wait] OR s1`pc1=wait AND s1`sem=vacant AND s2 = s1 WITH [pc1:=critical,sem:=occupied] OR s1`pc1=critcal AND s2 = s1 WITH [pc1:=idle,sem:=vacant] OR s1`pc2=idle AND s2 = s1 WITH [pc2:=wait] OR s1`pc2=wait AND s1`sem=vacant AND s2 = s1 WITH [pc2:=critical,sem:=occupied] OR s1`pc2=critcal AND s2 = s1 WITH [pc2:=idle,sem:=vacant] Dies definitiert "konzeptuell" eine Interpretation der Signatur TT = {state} PP = {N:[state,state->bool]} Beispiele von Formeln: 1. FORALL s1: EXISTS s2: N(s1,s2) 2. FORALL s1: NOT (s1`pc1=critical AND s1`pc2=critical) 3. FORALL s1: s1`sem=vacant => EXISTS s2: N(s1,s2) 4. FORALL s1: s1`pc1=idle => EXISTS s2: N(s1,s2) 1,2 sind falsch, 3,4 sind wahr. Die Aussagen sind nicht so spannend. Die eigentlich interessanten Eigenschaften wie a) vom Zustand pc1=pc2=idle,sem=vacant ist kein Zustand erreichbar mit pc1=pc2=critical b) wenn jeder Prozess im kritischen Bereich diesen auf wieder verlässt, dann bleibt das System nicht stecken sind in erststufiger Logik nicht ausdrückbar, wohl aber in höherstufiger Logik. Z.B. N*(s1,s2) = FORALL (P:[state->bool]): P(s1) AND (FORALL (x,y): P(x) AND N(x,y) IMPLIES P(y)) IMPLIES P(s2) Dann ist a) ausdrückbar als FORALL (s1,s2): s1=init & N*(s1,s2) => NOT (s2`pc1=critical AND s2`pc2=critical) Auch für höherstufige Logik ist MC entscheidbar, jedoch |[state->bool]| = 2^|[state]| Beispiel: 2 Prozesse, |state|=18, 2^18 = 256K Beispiel: 3 Prozesse, |state|=54, 2^54 = 10^16 (zu groß) Glücklicherweise existieren Fragmente der höherstufigen Logik, für die MC polynomiell ist und mit denen die interessierenden Beispiele formuliert werden können: CTL, mu-Kalkül, ... Computational Tree Logic ======================== Definition: Sei N:[state,state->bool] und P,Q:[state->bool] und s,s',s1,s2:state. EX(N,P)(s) = EXISTS s': N(s,s') & P(s') AX(N,P)(s) = FORALL s': N(s,s') IMPLIES P(s') Bemerkung: Falls es keine Folgezustände zu s gibt, ist AX(N,P)(s) trivialerweise wahr. Es gilt: EX(N,P) = NOT AX(N, NOT P) [Wobei NOT P = LAMBDA(s):NOT P(s)] AG(N,P)(s) = FORALL s': N*(s,s') IMPLIES P(s') Beispiel: FORALL s: init(s) => AG(N,safe)(s) mit safe(s) = NOT (s`pc1=critical AND s`pc2=critical) init(s) = s`sem=vacant & s`pc1=s`pc2=idle Nebenbemerkung: Erststufige Logik definiert immer nur lokale Eigenschaften, Schlagwort: "Satz von Gaifman". EF(N,P)(s) = EXISTS s': N*(s,s') AND P(s') Es gilt: EF(N,P) = NOT AG(N, NOT P) Beispiel: AG(N,EF(N,P))(s) "unendlich oft" EF(N,AG(N,P))(s) AF(N,P)(s) = "für jeden unendlichen Pfad s=s0,s1,s2,s3,... mit N(si,si+1) existiert i, sodass P(si)" EG(N,P)(s) = "es gibt einen unendlichen Pfad s=s0,s1,s2,s3,... mit N(si,si+1) mit P(si) für alle i" Es gilt: EG(N,P)(s) = NOT AF(N, NOT P) Satz (Fixpunkt-Definitionen): Es gilt (1) AG(N,P) = P AND AX(N, AG(N,P)) (AND ist wieder überladen) (2) EF(N,P) = P OR EX(N, EF(N,P)) (3) AF(N,P) = P OR AX(N, AF(N,P)) (4) EG(N,P) = P AND EX(N, EG(N,P)) Ausserdem sind AG(N,P) und EG(N,P) die größte Lösung von (1),(4), und EF(N,P) und AF(N,P) die kleinste Lösung von (2),(3). Beweis: (1) Sei Q:[state->bool] mit FORALL s: Q(s) => P(s) AND AX(N,Q)(s) Es gilt dann Q(s) => AG(N,P)(s) für alle s. Begründung: Es gelte Q(s) und sei ein Pfad s=s0,s1,...,sn mit N(si,si+1) gegeben. Man sieht leicht, dass P(si) gilt für alle i (durch Induktion nach n). Per Definition ist damit AG(N,P)(s). [Q spielt die Rolle einer Invarianten.] (3) Sei P OR AX(N, Q) => Q Sei AF(N,P)(s) gegeben. Zu zeigen Q(s). Annahme: Q(s) gelte nicht. Wir konstruieren einen unendlichen Pfad, beginnend mit s, auf dem P nirgends gilt. Denn gilt Q(si) nicht, dann gilt P(si) nicht und es gibt einen Nachfolger si+1, auf dem Q(si+1) auch nicht gilt. Dies ist im Widerspruch zu AF(N,P)(s). Größte und kleinste Fixpunkte lassen sich durch Iteration berechnen. Beispiel: Zur Berechnung von EF(N,P) halten wir eine Datenstruktur S für Teilmengen von state bereit und führen aus: S := leere Menge done := false while (NOT done) { T := P UNION EX(N,S) done := (S=T) S := T } // S = EF(N,P) Bemerkung: EX(N,S) = { s | es gibt s' in S mit N(s,s') } Analog: S := state done := false while (NOT done) { T := P INTERSECT AX(N,S) done := (S=T) S := T } // S = AG(N,P) Bemerkung: AX(N,S) = { s | für alle s' mit N(s,s') ist s' in S } mu-Kalkül ========= Sei Phi:[pred[state]->pred[state]] wobei pred[state]=[state->bool]. Z.B. Phi(Q)(s) = P(s) OR AX(N,Q)(s) Sei Phi monoton, d.h., wenn Q <= Q', dann Phi(Q) <= Phi(Q'). Dann bezeichnet mu(Phi) : pred[state] den kleinsten Fixpunkt von Phi gegeben durch UNION Phi^i(0) (bei endlichem Zustandsraum state) i >= 0 FORALL Q:pred[state]. (Phi(Q) <= Q) => Q(s) (andernfalls) Nach dem Satz gilt nun: AF(N,P) = mu (LAMBDA(Q): P OR AX(N,Q))