Matthias Bernauer - Freiburg im Breisgau
      Start > Skript-Sammlung > Rechnerarchitektur > Aequivalenzpruefung >>







Aequivalenzpruefung


Produktautomaten MProd von MA und MB = (I, {0,1}, SA xSB, (s0A,s0B), Prod, Prod) mit
Prod(sA,sB,w) = (A(sA,w), B(sB,w)) für alle sA aus SA, sB aus SB, w aus I
lProd(sA,sB,w) = 1 gdw. lA(sA,w)=lB(sB,w) für alle sA aus SA, sB aus SB, w aus I
MA und MB sind genau dann nicht äquivalent wenn es eine Eingabefolge w=(w0,w1,..., wz) gibt, so dass
- die zugehörige Ausgabefolgen von MA und MB verschieden sind
- der Produktautomat eine Folge != (1,...,1) ausgibt (k Einsen)
D.h. das äquivalenzproblem von MA und MB entspricht einem Erreichbarkeitsproblem im Produktautom.
-> gibt es einen Zustand (s*A,s*B) im Produktautomaten und ein Eingabesymbol w* aus I, so dass
lProd(s*A,s*B,w*) = 0 und (s*A,s*B) vom Startzustand (s0A,s0B) aus durch irgendeine Eingabefolge
erreichbar ist?
- Berechene Produktautomten
- Bestimme die Menge aller Zustände Sbad={(s*A,s*B)| es gibt ein w* aus I, s.d. lProd(s*A,s*B,w*)=0} - Bestimme die Menge aller vom Startzustand (s0A,s0B) aus erreichbaren Zustände Srechable
(funktioniert da Mprod endlich!)
- Ist Sbad geschnitten Sreachable leer (d.h. dann auch äquivalent) oder nicht?
! Das Verfahren lässt sich BDD basiert ohne explizites Darstellen von Zustandsmengen durchführen !
Google MSN Suche
<< Start | Studium | Poolmgr | Tanzen | GPG | Impressum >>
Matthias Bernauer