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

2006-01-12 VL 22

Nachtrag zu CTL:
================

Zwei weitere CTL-Operationen

  AU(N,P,Q)(s) :<==> für alle N-Pfade s=s0,s1,... existiert ein i0
                     so dass P(si) für all i < i0 und Q(si0)

Damit ist

  AF(N,P) = AU(N,true,P)

Ausserdem gibt es noch EU(N,P,Q)

"Liveness"-Eigenschaft für Semaphore-Beispiel:

  In jedem vom Initialzustand erreichbaren Zustand s gilt:
  Es gibt einen Pfad, beginnend mit s, auf dem Prozess 1 in den
  kritischen Bereich eintreten kann.

Faire Operatoren (jenseits von CTL)

  fairAF(N,P,F)(s) <==> für alle N-Pfade s=s0,s1,... gilt:
                        falls entlang s0,s1,... immer wieder F gilt,
                        dann gilt auch irgendwann P

fairAF nicht CTL-definierbar, wohl aber im mu-Kalkül.

  fairAF(N,P,F) = mu X. nu Y. P OR (F AND AX(N,X)) OR (NOT F AND AX(N,Y))

(Gleichheit nicht trivial).


Abstraktion und Model-Checking
==============================

Sei phi Formel und II unendliche oder sehr große Interpretation.  Um
festzustellen, ob II |= phi, finde endliche Interpretation II* und
Formel phi*, so dass

  a)  II* |= phi* => II |= phi
  b)  II* |= phi*
  
Wunsch: phi* soll möglichst generisch aus phi gewonnen werden.

Bsp.:

  state : TYPE = [# pc1,pc2:location, sem:int #]
  abs_state : TYPE = [# pc1,pc2:location, semleq0,semgt1:boolean #]

  abs (s:state) : abs_state = ...

Wichtiger Spezialfall: phi ist eine Sicherheitseigenschaft

  phi == FORALL s: init(s) => AG(N,safe)(s)

mit init, safe, N relativ einfach (z.B. quantorenfrei).

Man definiere Abstraktionen von N, init, safe so dass gilt:

  N(s1,s2) => abs_N(abs(s1),abs(s2))
  init(s) => abs_init(abs(s))
  abs_safe(abs(s)) => safe(s)

[mit (grind)] und

  |= abs_init <= AG(abs_N,abs_safe)

[mit (model-check)]. Dann folgt |= phi.

Beweis:  Es gelte init(s) und s=s0,s1,s2,...,sn sei ein N-Pfad. Zu
zeigen safe(sn).

Wir haben abs_init(abs(s)) und abs(s0),abs(s1),...,abs(sn) ist ein
abs_N-Pfad. Damit gilt abs_safe(abs(sn)) und damit safe(sn).

Direkte Definition der Abstraktion, z.B.

  abs_init(x) = EXISTS s: x=abs(s) AND init(s)

ist ungeschickt, da der Quantor über einen unendlichen oder großen
Bereich rangiert.  (Nichts gewonnen.)

Besser: Wähle

  abs_init(x) <= EXISTS s: x=abs(s) AND init(s)

aber, abs_init quantorenfrei.  Genauso abs_N.

Bemerkung: Es muss nicht unbedingt gelten, das Im(abs) = abs_state,
also es darf abstrakte ("wilde") Zustände geben, die keinem konkreten
entsprechen.  Ebenso, darf die die abstrakte Transitionsrelation von
"zahmen" in "wilde" übergehen.

PVS kann abs, abs_init, abs_N und abs_safe selbst berechnen.  Es
brauch nur die Typen state, abs_state und den Befehl:

  (abstract-and-mc state abs_state 
    ((semleq0 "lambda s: s`sem<=0")
     (semgt1  "lambda s: s`sem>1")))

Allgemein führt das Berechnen von Abstraktionen (von Prädikaten oder
Relationen zu gegebener Abstraktionsfunktion) auf folgendes Problem:

Gegeben: Zwei Mengen Qa und Qc und Funktion alpha:Qc->Qa,
         Prädikat P <= Qc.

Finde:   P_a <= Qa möglichst klein, sodass 
 
           P(s) => P_a(alpha(s)) für alle s in Qc.

(Bemerkung: Zur Berechnung von abs_init setze 
  Qa = abs_state, Qc = state, alpha = abs.
Zur Berechnung von abs_safe setze
  Qa = abs_state, Qc = state, alpha = abs.
Dann ist abs_safe = NOT (NOT safe)_a.)

Formale Lösung des Problems:

  P*_a(sigma) := EXISTS s in Qc. alpha(s)=sigma AND P(s)

Beweis der Korrektheit: 

1) Trivial (mit inst) gilt
           P(s) => P*_a(alpha(s)) für alle s in Qc.

2) Falls es ein P_a gibt mit
           P(s) => P_a(alpha(s)) für alle s in Qc 
   dann gilt P*_a <= P_a.

Sei weiter Qa endlich und von der Form 2^V, also Belegungen von
Boole'schen Variablen in V = {v1,...,vl}. [Predicate Abstraction,
Graf-Saidi 1990er]
Jedes Prädikat auf Qa ist dann eine Boole'sche Funktion in den vi,
insbesondere auch P*_a.

Idee: Setze Abstraktion P_a als KNF an, also als Menge von Klauseln.
(Je mehr Klauseln hinzugefügt werden, desto besser.)  Eine Klausel C
gehört zu P_a genau dann, wenn

  FORALL s in Qc. P(s) -> C(alpha(s))                  (dagger)

Bsp: C = semgt1 OR semleq0.  Die Bedingung ist dann zu lesen als

  FORALL s. P(s) -> s`sem > 1 OR s`sem <= 0

Vorschlag von Shankar-Ruess: Setze

  P_a := AND { C | PVS kann P(s) -> C(alpha(s)) automatisch zeigen }

O(3^n) Aufrufe an den Theorembeweiser.

So funktioniert abstract-and-mc tatsächlich.


Ausblick: Diese Technik funktioniert nicht gut für E-Formeln.  Dazu
wird eine Diplomarbeit vorgestellt.  Zu Fairness-Abstraktion gibt es
noch fast gar nichts, Diplomand gesucht!