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

2006-01-18 VL 23

Fortsetzung abstract-and-mc:

N*(phi,eta) = EXISTS s,s'. alpha(s)=phi AND alpha(s')=eta AND N(s,s')

P* = AND { C Klausel | |= forall s. P(s) -> C(alpha(s)) }
P_ = NOT (NOT P)*


Es gilt:

  AG(N*,P_)(alpha(s)) -> AG(N,P)(s)
  AF(N*,P_)(alpha(s)) -> AF(N,P)(s)
  AX(N*,P_)(alpha(s)) -> AX(N,P)(s)

Wie ist es bei EX(N,P)?

Gesucht N?, sodass 

   EX(N?,P_)(alpha(s)) -> EX(N,P)(s)                                (*)

   Erinnerung: EX(N,P)(s) = EXISTS s'. N(s,s') AND P(s')

Das gilt mit N? = N_, wobei

 (i)  N_(alpha(s),alpha(s')) -> N(s,s') und 
 (ii) N_ so gross wie möglich

Die formale Lösung lautet

 N_(phi,eta) = FORALL s. alpha(s)=phi -> FORALL s'. alpha(s')=eta -> N(s,s')

Allerdings ist N_ unbrauchbar:

Bsp: Qc = Z 
     N(x,y) = (| x - y | = 1)
     Prädikate: ge0, eq0, lt0 [sic!] [sinnlos, da ge0 = NOT lt0 ]
     alpha(5) = { ge0 = true, eq0 = false, le0 = false }

     N_ ist leer

Für (*) ist (i) nicht zwingend erforderlich, es reicht, dass

  (iii) N?(alpha(s),eta) -> EXISTS s': alpha(s')=eta & N(s,s')
  (iv)  N? möglichst groß

Begründung:

Sei EX(N?,P_)(alpha(s)), also N?(alpha(s),eta) 
und P_(eta) [ = NOT (EXISTS s. alpha(s)=eta AND NOT P(s)) 
              = FORALL s. alpha(s)=eta IMPLIES P(s) ]
Mit (iii) finden wir ein s' mit alpha(s')=eta und N(s,s').
Also gilt P_(alpha(s)), somit P(s).

Formale Lösung von iii, iv:

  N^AE (phi, psi) = FORALL s.  alpha(s) = phi => 
                    EXISTS s'. alpha(s')= eta AND N(s,s')

Für Bsp:

  N*  : ge0 <--> ge0 <--> eq0 <--> lt0 <--> lt0

  N^AE: ge0 <--> ge0 <--  eq0  --> lt0 <--> lt0

  N_  : leer

Berechnung von N^AE bei Prädikatabstraktion.  (Qa = 2^V)

Setze N^AE an als DNF (Disjunktion von Konjunktionen) über 2*|V|
Variablen an.

  N^AE = OR { M Antiklausel | |= M(alpha(s),eta) -> 
                                 EXISTS s'. alpha(s')=eta AND N(s,s') }
                                 ----------------- ** ---------------

Beispiel für Antiklausel:

  le0 AND NOT le0'  (' bedeutet Folgezustand)

Problem: ** nicht mehr quantorenfrei, PVS kann schlecht einen
automatischen Beweis führen.

In vielen Fällen ist N(s1,s2) von der Form "guarded commands":

  OR_{i=1..n} (gi(s1) AND s2=fi(s1))

wobei gi : Q_c -> bool   "guard"   (Zustandstest)
      fi : Q_c -> Q_c    "command" (Zustandsmodifikation)

In diesem Fall kann die Bed. (**) vereinfacht werden wie folgt:

     EXISTS s'. alpha(s')=eta AND (OR_{i=1..n} (gi(s) AND s'=fi(s)))

<==> EXISTS s'. OR_{i=1..n} (gi(s) AND alpha(s')=eta AND s'=fi(s))

<==> OR_{i=1..n} (gi(s) AND EXISTS s'. alpha(s')=eta AND s'=fi(s))

<==> OR_{i=1..n} (gi(s) AND alpha(fi(s))=eta)

Falls die gi und fi quantorenfrei ist, ist dies auch qu.frei.

Diplomarbeit Roland Axelsson:
-----------------------------

Herleitung und Implementierung:
- konkretes System in guarded command Form als abstrakte Syntax
  eingeben
- Programm erzeugt PVS-Rep. von N, N^AE
- Verwendet Stanford Validity Checker (SVC, automatischer Beweiser)
  zur Erzeugung von N^AE
- Graphische Rep. von N*, N^AE.

Weitere Aufgaben:
- Effizienz (nicht blindes Probieren aller Antiklauseln)
- Erweiterung auf Fairness und Lebendigkeit
  Abstraktion mit N* und N^AE könnte versagen bei AG_fair, EG_fair, etc.

Folgendes Problem mit AF, EF: (siehe auch Stefan Merz, Andreas Podelski)
  
  Qc = |N
  N(x,y) = x>0 & y = x-1  "y ist Vorgänger von x"

  Es gilt: AF(N, LAMBDA x: x=0)(s) in allen Zuständen s (Wohlfundiertheit)

  Abstraktion >0, =0

              a
  N*:  (>0) <---> (>0) ---> (=0)
  
  In dieser Abstraktion kann obige Eigenschaft nicht gezeigt werden.

  Abhilfe: Betrachte im abstakten Modell nur solche Pfade, in denen
  Transition a nicht ununterbrochen genommen wird.