Download - Formale Spezi kation und Veri kation - LMU
Formale Spezifikation und Verifikation
Martin Hofmann
Sommersemester 2014
1
Uberblick uber die Vorlesung
Was ist Spezifikation?
Beschreibung eines Teils des gewunschten Systemverhaltens.
QuickSort berechnet sortierte Permutation
Iterator bietet alle Elemente der Menge in einer beliebigenReihenfolge an
Wird equals() uberschrieben, so muss auch hashcode()entsprechend angepasst werden
Die vom Roboterarm beschriebene Trajektorie muss innerhalbder erlaubten Toleranz mit der im Programm vorgegebenenubereinstimmen. Die Grenzgeschwindigkeiten und-beschleunigungen durfen nicht uberschritten werden
Die Handy-Anwendung darf nicht mehr SMS verschicken alszuvor autorisiert.
Nicht: Zweck des Systems (“Ihre Software soll in der Buchhaltung10% Personal einsparen.”)
2
Uberblick uber die Vorlesung
Was ist Verifikation?
Nachweis, dass System eine gegebene Spezifikation erfullt
Durch Tests (“unvollstandig”)
Durch Argumentation
Durch rigorosen Beweis
Durch automatisches Verifikationswerkzeug
Durch formalisierten Beweis
3
Uberblick uber die Vorlesung
Was heißt “formal”?
Mit Mitteln der Logik ausgedruckt.
Bedeutung einer formalen Spezifikation ist exakt festgelegt(konnte aber moglicherweise das Gewunschte nicht erfassen)
Eine formale Verifikation liefert die Gultigkeit der zugehorigenSpezifikation mit 100%-iger Sicherheit, allerdings nur fur daszugrundegelegte formale Modell des Systems.(Extrembeispiele: Kurzschluss, Uberlastung, Compilerfehler)
Formale Spezifikation und Verifikation kann dieSystementwicklung sinnvoll unterstutzen, ist aber keinAllheilmittel.
4
Uberblick uber die Vorlesung
Inhalt
Kapitel I Propositionale Logik: Wdh. Syntax, Semantik. Reduktion aufSAT, SAT-Solver, Anwendung auf Modellierung. BDDs.
Kapitel II Temporallogik und Model Checking: Temporallogik CTL,Syntax und Semantik, Model Checking Algorithmen,Temporallogik LTL und Buchi-Automaten, die WerkzeugeSMV und SPIN.
Kapitel III Programmanalyse und Typsysteme: Operationelle Semantik,Datenflussanalyse, Java Bytecode Verifier, Typsysteme furRessourcen.
Kapitel IV Erststufige Logik, Programmlogik: Wdh. Syntax, Semantik,Hoare-Logik, JML.
5
Uberblick uber die Vorlesung
Organisatorisches, Literatur
Vorlesungs- und Klausurtermine, siehe Homepage derVeranstaltung.
Literatur
Huth, Ryan: Logic in Computer Science.
Clarke, Grumberg, Peled: Model checking.
Nielson, Nielson, Hankin: Program analysis.
Als Wdh. der Logik: Skripten von Till Tantau, Martin Langeund MH.
Das Folienskript sollte als Unterlage genugen; ersetzt aber nichtden Besuch der Vorlesung und Ubungen.
6
Propositionale Logik
Kapitel I
Propositionale Logik
7
Propositionale Logik
Inhalt Kapitel I
2 Motivation3 Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit4 Mengennotation und indizierte Variablen5 Normalformen6 SAT-Solver
Optimierungen7 Gleichheit von Schaltkreisen8 Modellierung nebenlaufiger Systeme
Gegenseitiger Ausschluss mit SemaphorPeterson Algorithmus
9 BDDs (binare Entscheidungsdiagramme)Grundlegende DefinitionenLogische Operationen auf BDDsImplementierung von BDDsNebenlaufige Systeme mit BDDs8
Propositionale Logik
Motivation
Protokollchef
Der Botschafter bittet Sie eine Einladungsliste fur den Ball derBotschaft zusammenzustellen.
Sie sollen Peru einladen oder Katar nicht einladen.
Der Vizebotschafter mochte, dass Sie Katar, Rumanien, oderbeide einladen.
Aufgrund eines aktuellen Vorfalls konnen Sie nicht Rumanienund Peru zusammen einladen.
Wie stellen Sie die Einladungsliste zusammen?
9
Propositionale Logik
Motivation
Modellierung in propositionaler Logik
Peru oder nicht Katar: P _ K
Katar oder Rumanien: K _ R
Nicht Rumanien und Peru zusammen: pR ^ Pq
Man muss die propositionalen Variablen P,K ,R so mitWahrheitswerten true, false belegen, dass alle drei Formeln wahrwerden.Ist das moglich, so ist die Formelmenge erfullbar.Ist hier der Fall, z.B. mit P � true,K � true,R � false.Alternative: P � false,R � true,K � false.Die Formelmenge tP _ K ,K _ R, pR ^ Pqu ist also erfullbar.Oben stehen zwei erfullende Belegungen.
10
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Syntax der Aussagenlogik
Sei eine Menge A von Aussagenvariablen A,B,C ,D . . . gegeben.Die aussagenlogischen Formeln uber A sind durch folgende BNFGrammatik definiert.
F ::� A| F (Negation, Verneinung)| F ^ F (Konjunktion, logisches Und)| F _ F (Disjunktion, logisches Oder)| F ñ F (Implikation, Wenn-Dann-Beziehung)
| F ô F (Aquivalenz, Genau–Dann-Wenn-Beziehung, “iff”)| J Verum, wahre Formel| K Falsum, falsche Formel
Die Symbole t ,^,_,ñ,ôu heißen Junktoren.
11
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Syntaxbaume
Formal ist eine Formel also ein Syntaxbaum:
entspricht pA^ Bq _ ppC ñ Dq ^ p Aqq.Manche Klammern darf man weglassen, da nach Konvention amstarksten bindet und dann ^,_,ñ,ô.Gleiche Junktoren werden von rechts geklammert, alsoA ñ B ñ C ist A ñ pB ñ C q.
12
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Semantik der Aussagenlogik
Eine Formel der Form φ^ ψ ist wahr, wenn φ und ψ beidewahr sind. Ist entweder φ oder ψ falsch, so ist φ^ ψ falsch.
Eine Formel der Form φ_ ψ ist wahr, wenn φ wahr ist oderwenn ψ wahr ist. Nur wenn φ und ψ beide falsch sind, ist dieFormel φ_ ψ falsch.
φ ist wahr, wenn φ falsch ist. Ist φ wahr, so ist φ falsch.
φñ ψ ist wahr, wenn entweder φ falsch ist, oder aber φ wahrist und ψ dann auch wahr ist. Nur wenn φ wahr ist undzugleich ψ falsch ist, ist φñ ψ falsch.
Eine Formel der Form φô ψ ist wahr, wenn φ und ψdenselben Wahrheitsgehalt haben, also entweder beide wahr,oder beide falsch sind.
Die Formel J ist wahr, die Formel K ist nicht wahr; beidesunabhangig vom Wahrheitsgehalt der Variablen.
13
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Formale Semantik
Formal definiert man fur jede Belegung η, die den VariablenWahrheitswerte zuweist und Formel φ einen Wahrheitswert rrφssη.Z.B.: rrφ^ ψ _ ρssη � prrφssη& rrψssηq || rrρssηwobei & und || durch folgende Wahrheitstafeln gegeben sind.
& false true
false false falsetrue false true
|| false true
false false truetrue true true
14
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit
Tautologien
Definition
Eine Formel φ ist eine Tautologie, wenn sie unabhangig vomWahrheitsgehalt der Variablen stets wahr ist. Formal also, wenn furalle Belegungen η ihrer Variablen gilt rrφssη � true.
Beispiele fur Tautologien
A_ A
pA ñ Bq ñ pB ñ C q ñ pA ñ C q
A ñ A
A^ B _ A^ B _ A^ B _ A^ B
15
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit
Erfullbare Formeln
Definition
Eine Formel φ ist erfullbar (satisfiable), wenn es eine Belegungihrer Variablen gibt, die sie erfullt (wahrmacht). Formal heißt das,dass eine Belegung η existiert, derart, dass rrφssη � true.Eine Formel φ ist unerfullbar (unsatisfiable), wenn sie nichterfullbar ist.
Beispiele erfullbarer Formeln
A
A^ B
pA_ Bq ^ p A_ Bq ^ pA_ Bq
16
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit
Aquivalenz
Aquivalenz
Zwei Formeln φ und ψ sind aquivalent, wenn fur alle Belegungen ηgilt: rrφssη � rrψssη
Beispiele aquivalenter Formeln
φ_ ψ ist aquivalent zu ψ _ φ
φñ ψ ñ ρ ist aquivalent zu pφ^ ψq _ ρ
17
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit
Erfullbarkeitsaquivalenz
Erfullbarkeitsaquivalenz
Zwei Formeln φ und ψ sind erfullbarkeitsaquivalent, wenn gilt: φerfullbar gdw. ψ erfullbar.
Beispiele erfullbarkeitsaquivalenter Formeln
A_ B ist erfullbarkeitsaquivalent zu J
φ_ ψ ist erfullbarkeitsaquivalent zu p A_ φq ^ pA_ ψq
18
Propositionale Logik
Syntax und Semantik der Aussagenlogik
Tautologien und Erfullbarkeit
Zusammenhange
Satz
φ ist Tautologie, gdw. φ unerfullbar ist.
φ ist Tautologie, gdw. φ aquivalent zu J ist.
φ ist erfullbar, gdw. φ erfullbarkeitsaquivalent zu J ist.
19
Propositionale Logik
Mengennotation und indizierte Variablen
Mengennotation
Abkurzung�
iPI φi ��tφi | i P I u � φi1 ^ � � � ^ φin , wenn
I � ti1, . . . , inu.
Analog�
iPI φi .
Leere Konjunktion:�H � J.
Leere Disjunktion:�H � K.
20
Propositionale Logik
Mengennotation und indizierte Variablen
Beispiel Sudoku
Fur i , j P t0, . . . , 8u und k P t1, . . . , 9u fuhren wir eine Variable xijkein. Bedeutung von xijk : In Zeile i , Spalte j steht die Zahl k .Folgende Formeln modellieren die Sudoku Spielregeln.�
i
�j
�k xijk (alle Felder sind ausgefullt).
�i
�j
�k�k 1 pxijk ^ xijk 1q (nur eine Zahl pro Feld).
�i
�j�j 1�
k pxijk ^ xij 1kq (nicht dieselbe Zahl zweimal ineiner Zeile)�
i�i 1�
j
�k pxijk ^ xij 1kq (nicht dieselbe Zahl zweimal in
einer Spalte)�
zPt0,1,2u
�wPt0,1,2u
�k
�u,u1Pt0,1,2u
�v ,v 1Pt0,1,2u if u �
u1 || v � v 1 then px3z�u,3w�v ,k ^ x3z�u1,3w�v 1,kq else J(nicht dieselbe Zahl zweimal in einer 3x3 Box)
21
Propositionale Logik
Mengennotation und indizierte Variablen
Losung eines Sudoku
Gibt man zu den so formulierten Spielregeln die schon besetztenFelder dazu (per ^), so entsprechen die erfullenden Belegungengerade den Losungen.Beispiel:
�pi ,j ,kqPI xijk wobei
I � tp0, 0, 6q, p0, 4, 1q, p0, 5, 7q, p0, 6, 5q,p1, 1, 8q, p1, 2, 1q, p1, 3, 2q, p1, 7, 7q,p2, 5, 5q,p3, 1, 2q, p3, 2, 9q, p3, 3, 4q, p3, 8, 1q,p4, 1, 5q, p4, 2, 4q, p4, 4, 2q, p4, 7, 3q,p5, 2, 6q, p5, 4, 7q, p5, 5, 8q, p5, 7, 5q, p5, 8, 4q,p6, 5, 9q, p6, 6, 3q, p6, 8, 7q,p7, 2, 3q, p7, 3, 8q, p7, 6, 4q,p8, 2, 5q, p8, 7, 9qu
Aus der “Zeit” vom 22.10.2009 (“schwer”).22
Propositionale Logik
Normalformen
Literale und Maxterme
Literal
Ein Literal ist eine negierte oder nichtnegierte Variable. Ist ` einLiteral, so definiert man ` durch pAq � A und p Aq � A.
Minterm, Und-Block
Eine Konjunktion (Ver-undung) von Literalen heißt Minterm oderUnd-Block.
Maxterm, Klausel
Eine Disjunktion (Ver-oderung) von Literalen heißt Maxterm oderKlausel oder Oder-Block.
23
Propositionale Logik
Normalformen
Konjunktive Normalform, Disjunktive Normalform
Konjunktive Normalform, KNF
Eine Konjunktion von Klauseln (Oder-Blocken) heißt KonjunktiveNormalform (KNF).
Disjunktive Normalform, DNF
Eine Disjunktion von Mintermen (Und-Blocken) heißt DisjunktiveNormalform (DNF).
Satz von der DNF
Jede aussagenlogische Formel ist aquivalent zu einer DNF.
Beweis: Man fuhrt je einen Minterm pro true-Zeile in derWahrheitstafel ein.Analoges gilt fur die KNF (hier je ein Maxterm pro false-Zeile).
24
Propositionale Logik
Normalformen
Berechnung einer erfullbarkeitsaquivalenten KNF
Die zu einer Formel aquivalente KNF kann sehr (exponentiell) großsein.Besteht man nur auf Erfullbarkeitsaquivalenz, so geht es effizienter:
Satz
Zu jeder Formel φ kann in polynomieller Zeit eineerfullungsaquivalente KNF Γ linearer Große (bezogen auf die Großevon φ) berechnet werden.
Man definiert rekursiv eine Funktion KNF, die zu jeder Formel φeine KNF Γ und eine Variable A liefert, sodass Γerfullungsaquivalent mit A ô φ ist.Die gesuchte KNF ist dann A^ Γ.
25
Propositionale Logik
Normalformen
Definition der Funktion KNF (Tseitin Ubersetzung)
KNFpAq � pA,Jq (leere KNF)
KNFp φq � let pB, Γq � KNFpφq inpC , Γ^ pC _ Bq ^ p C _ Bqq.
KNFpφ1 _ φ2q � let pB1, Γ1q � KNFpφ1q in let pB2, Γ2q �KNFpφ2q inpC , Γ1 ^ Γ2 ^ p C _ B1 _ B2q ^ p B1 _ C q ^ p B2 _ C qq
Rest als Ubung.
NB: Die Variable C ist jeweils frisch zu wahlen.NB: A1 _ A2 _ � � � _ Am _ B1 _ � � � _ Bn ist aquivalent zup�
i Ai q ñ p�
j Bjq.NB: Es bietet sich an, mit dynamischer Programmierung dafur zusorgen, dass identische Teilformeln nur einmal verarbeitet werden.Das ist insbesondere wichtig, wenn Teilformeln ge”shart” sind(Schaltkreise).
26
Propositionale Logik
Normalformen
Beispiel
OR OR
OR
ANDXORAND
NEGZ
D
E
F
G
X
Y
A
B
C
pA_ X _ Y q ^ p A_ X q ^ p A_ Y q^p B _ Y _ Z q ^ pB _ Y q ^ pB _ Z q^p C _ A_ Bq ^ p C _ A_ Bq ^ pC _ A_ Bq ^ pC _ A_ Bq^p D _ A_ Bq ^ pD _ Aq ^ pD _ Bq^pE _ C _ Dq ^ p E _ C q ^ p E _ Dq^p F _ Dq ^ pF _ Dq^p G _ E _ F q ^ pG _ E q ^ pG _ F q^G
26
Propositionale Logik
SAT-Solver
Das SAT-Problem
Das SAT-Problem besteht darin, von einer gegebenen KNF zuentscheiden, ob sie erfullbar ist.Mit der Tseitin-Ubersetzung lasst sich Erfullbarkeit von Formelnund beliebigen Schaltkreisen auf SAT reduzieren.Formeln (Schaltkreise) φ, ψ sind aquivalent, genau dann wenn pφô ψq unerfullbar ist.Das SAT-Problem ist bekanntlich NP vollstandig. Dennoch lasst essich in vielen Fallen mittlerer Große ( 106 Variablen undKlauseln) praktisch losen.Dazu gibt es als SAT-Solver bezeichnete Programme, z.B. zChaff,Minisat.
27
Propositionale Logik
SAT-Solver
DIMACS-Format
Die SAT-Solver akzeptieren eine KNF in einem standardisiertenFormat (“DIMACS-Format”).Variablen werden durch Integer ¡ 0 reprasentiert. NegierteVariablen durch entsprechende negative Zahlen. Klauseln werdendurch 0-terminierte Zeilen, die ihre Literale enthalten, reprasentiert.Außerdem ist in einem Header die Zahl der Variablen und Klauselnanzugeben. Beispiel fur p A_ B _ C q ^ pA_ B _ D _ E q:
c Kommentarzeile.
p cnf 5 2
-1 2 3 0
1 -2 4 50
Verwendet man einen SAT-Solver, so muss man eine Zuordnungder Variablen zu Zahlen fixieren und sich merken. HierA � 1,B � 2,C � 3,D � 4,E � 5.
28
Propositionale Logik
SAT-Solver
DPLL-Algorithmus
Alle SAT-Solver verwenden den DPLL-Algorithmus (Davis,Putnam, Logemann, Loveland). Prinzip: “Vorrechnen” und wenndas nicht hilft, verzweigen.Formal kann DPLL als rekursive Prozedur DPLLpη, Γq beschriebenwerden, die zu gegebener Belegung η und KNF Γ entweder eineerfullende Belegung fur Γ liefert, die η erweitert, oder “UNSAT”liefert, wenn es keine solche gibt.
29
Propositionale Logik
SAT-Solver
DPLL genauer
DPLLpη, Γq :1 Vereinfache alle Klauseln gemaß η. D.h. entferne falsche
Literale aus Klauseln, entferne Klauseln, die ein wahres Literalenthalten.
2 Falls Γ die leere Klausel enthalt, so gib UNSAT zuruck. Dieleere Klausel entsteht insbesondere nach Schritt 1, wenn ΓEinerklauseln enthalt, die η widersprechen.
3 Falls Γ noch Einerklauseln enthalt, so fuge die entsprechendenSetzungen zu η hinzu und wiederhole die Schritte 1 und 2.Das passiert z.B., wenn Γ eine Klausel t A,Bu enthalt undηpAq � true.
4 Wenn die Schritte 1,2,3 keinen Fortschritt mehr bringen, sowahle beliebige noch nicht von η belegte Variable X und rufeder Reihe nach DPLLpΓ, ηrX ÞÑfalsesq undDPLLpΓ, ηrX ÞÑtruesq auf. Gibt es keine zu setzende Variablemehr, so ist η selbst die gesuchte erfullende Belegung.30
Propositionale Logik
SAT-Solver
DPLL Algorithmus: Anmerkungen
Die Schritte 1,2,3 heißen Unit Propagation
Hilft die Unit Propagation nicht mehr weiter und sind alleVariablen gesetzt, so ist η in der Tat erfullende Belegung.
Vorsicht: Man darf Γ nicht als globale Variable vorhalten, dasonst der Aufruf DPLLpΓ, ηrX ÞÑfalsesq das Γ modifiziert(“zerschießt”) und es dann nicht mehr fur den AufrufDPLLpΓ, ηrX ÞÑtruesq zur Verfugung steht.
Bei rekursiver Implementierung werden die Γs und ηs auf demKeller abgelegt. In der Praxis implementiert man diesen Kellerexplizit und speichert auf diesem nur jeweils die Anderungenab.
31
Propositionale Logik
SAT-Solver
Optimierungen
Optimierungen
Anstatt die KNF Γ explizit zu verandern, merkt man sich nurfur jede Klausel, welche Literale bereits gesetzt sind. Um neugefundene Setzungen schnell zu propagieren, “beobachtet”jede Klausel die Variablen zweier ihrer unbesetzten Literale(watched literals). Wird eine von diesen gesetzt, so wird einneues watched literal gesucht. Gibt es keines, so liegt eineEinerklausel vor (; Unit Propagation).
Bei einem Konflikt (UNSAT) wird ermittelt, welcheVariablensetzungen fur den Konflikt verantwortlich waren undals neue “gelernte” Klausel der KNF hinzugefugt. War z.B.X � true,Y � false,Z � false verantwortlich, so “lernt” man X _ Y _ Z .Man speichert hierzu bei jeder Setzung den entsprechendenGrund mit ab.
32
Propositionale Logik
SAT-Solver
Optimierungen
Beispiel
à ��t�tA,B,Cu,
�tA,B, Cu,
�tA, B,C ,X u,�
tA, B, C , X u,�t A, B,C ,X uu
Wir beginnen mit X � false und dann A � false und dannB � false. Durch Unit Propagation erhalten wir aus den erstenbeiden Klauseln einen Konflikt. Beteiligt waren nur die SetzungenA � B � false. Wir konnen daher die Klausel A_ B lernen. Siehilft uns spater bei X � true.
33
Propositionale Logik
Gleichheit von Schaltkreisen
Schaltkreise
Ein Schaltkreis ist ein DAG (gerichteter azyklischer Graph) dessenKnoten mit Junktoren beschriftet sind.
XOR AND
HAOR
ORXOR
XOR AND AND AND
VA2VA
HA
HA
OR
Um VA � VA2 zu zeigen, beginnen wir mit drei Variablen X ,Y ,Cund bilden die Formel
ppVApX ,Y ,C q1 ô VA2pX ,Y ,C q1q^pVApX ,Y ,C q2 ô VA2pX ,Y ,C q2qq
wobei VApX ,Y ,C q1 den ersten Ausgang von VApX ,Y ,C qbezeichnet, etc.34
Propositionale Logik
Gleichheit von Schaltkreisen
Ubersetzung in KNF
Tseitin-Transformation: KNF mit 37 Variablen, 58 Klauseln(UNSAT)Ersetzt man das untere XOR von VA2 durch ein OR, so wird dieentsprechende KNF erfullbar. zChaff findet: x � y � true, c � false
35
Propositionale Logik
Gleichheit von Schaltkreisen
Erzeugung von KNF mit OCAML
Das OCAML Modul cnf.ml auf der Homepage erlaubt dieErzeugung von KNF in DIMACS-Format ausgehend von logischenFormeln. Es bietet u.a. folgende Funktionen an:
val reset : unit -> unit (* resetting the variable generator *)
val newvar : unit -> int (* a fresh variable *)
val nvar : unit -> int (* number of generated variables since last reset *)
type formula (* abstract type of formulas *)
val var : int -> formula
val dtrue, dfalse : formula
val dor, dand : formula -> formula -> formula
val xor : formula -> formula -> formula
val iff : formula -> formula -> formula
val neg : formula -> formula
val dands : formula list -> formula
val dors : formula list -> formula
36
Propositionale Logik
Gleichheit von Schaltkreisen
Ein- und Ausgabe
Tseitin-Transformation und Ausgabe als DIMACS Format:
val mk_dimacs : string -> formula list -> string -> unit
Aufruf (mk_dimacs filename formulas header)Einlesen einer zChaff-Ausgabe:
val parse_zchaff : string -> int list option
Falls (parse_zchaff filename) = None, dann enthaltfilename die Inf UNSAT.Falls (parse_zchaff filename) = Some l, dann ist l die infilename enthaltene erfullende Belegung.
37
Propositionale Logik
Gleichheit von Schaltkreisen
Gleichheit von Addierern
let ha x y = (xor x y,dand x y)
let va x y c =
let (yc,d) = ha y c in
let (s,e) = ha x yc in
let cr = dor e d in (s,cr)
let va2 x y c =
let s = xor (xor x y) c in
let cr = dor (dor (dand c y) (dand y x)) (dand c x)) in
(s,cr)
38
Propositionale Logik
Gleichheit von Schaltkreisen
Gleichheit von Addierern
let test1 =
let xx = var (newvar()) in
let yy = var (newvar()) in
let cc = var (newvar()) in
let (s1,cr) = va xx yy cc in
let (s2,cr2) = va2 xx yy cc in
neg(dand (iff s1 s2) (iff cr cr2))
let _ = mk_dimacs "adder_test1.cnf" [test1] ""
39
Propositionale Logik
Gleichheit von Schaltkreisen
Compilierung und Ausfuhrung
ocamlopt -c adder.ml
ocamlopt -c cnf.ml
ocamlopt -o adder str.cmxa cnf.cmx adder.cmx
./adder
./zchaff adder_test1.cnf
40
Propositionale Logik
Gleichheit von Schaltkreisen
Ripple-Addierer
Um Binarzahlen zu addieren, kann man Volladdiererhintereinanderschalten (Ripple-Adder):
VA VA VA VA
x1 y1 x y3x0 y0 x2 y2
s0 s1 s2 s3 co
Die Durchlaufzeit ist hier proportional zur Zahl n der addiertenBits (schlecht bei n � 64).Grund: Ubertrag muss durch alle n Volladdierer laufen (“ripple”)
41
Propositionale Logik
Gleichheit von Schaltkreisen
Carry-Lookahead Addierer
Gunstiger ist es, den Ubertrag ci am i-ten Volladdierer als logischeFunktion der Inputs direkt zu berechnen.
carry, gen und prop
ci � if i�0 then K else gen0i
genij � if i�j then xi ^ yi else genkj _ pgenipk�1q ^ propkjq
propij � if i�j then xi _ yi else propipk�1q ^ propkj
wobei jeweils k � tpj � i � 1q{2u� i der “Mittelpunkt” von i und j .
Es bedeutet genij , dass am Ende des Blocks i . . . j ein Ubertrag aufjeden Fall entsteht.Und propij bedeutet, dass der Block i . . . j einen moglicherweise
einlaufenden Ubertrag propagiert.Da sich das Intervall jeweils halbiert, ist die Rekursionstiefe unddamit die Tiefe der entstehenden Schaltkreise Oplogpnqq.42
Propositionale Logik
Gleichheit von Schaltkreisen
Implementierung in OCAML (1)
Wir verwenden das Funktional fordo aus cnf.mli:
fordo i j a f � f pj � 1q pf pj � 2q . . . pf pi � 1q pf i aqq . . . q
um zwei Assoziationslisten (“maps”) fur die Eingabevariablen zuerzeugen:
let size = 30
let xs = fordo 0 size [] (fun i l -> (i,newvar())::l)
let x i = var(List.assoc i xs)
let ys = fordo 0 size [] (fun i l -> (i,newvar())::l)
let y i = var(List.assoc i ys)
Jetzt ist zum Beispiel x 5 die Eingabevariable x5.
43
Propositionale Logik
Gleichheit von Schaltkreisen
Implementierung in OCAML (2)
Den Ripple-Addierer implementiert man so:
let rec rippleadd i = if i=0 then (dfalse,[]) else
let (c,ss) = rippleadd (i-1) in
let (s,d) = va (x (i-1)) (y (i-1)) c in
(d,ss@[s])
Es ist insbesondere rippleadd size� cout, rs0; . . . ; ssize�1s.
44
Propositionale Logik
Gleichheit von Schaltkreisen
Implementierung in OCAML (3)
Die gen- und prop-Schaltkreise:
let rec carry i =
if i = 0 then dfalse else gen 0 (i-1)
and gen i j =
if i = j
then dand (x i) (y i)
else let k = (j+1-i)/2 + i in
dor (gen k j) (dand (gen i (k-1)) (prop k j))
and prop i j =
if i = j
then dor (x i) (y i)
else let k = (j+1-i)/2 + i in
dand (prop k j) (prop i (k-1))
45
Propositionale Logik
Gleichheit von Schaltkreisen
Implementierung in OCAML (4)
Die Aquivalenz der Summenbits:
let lookaheadaddbit i =
va2 (x i) (y i) (carry i)
let carryout,sumbits = rippleadd size
let test2= neg
(dand (iff carryout (snd (lookaheadaddbit (size-1))))
(dands (fordo 0 size [] (fun i l ->
let (s,c) = lookaheadaddbit i in
iff s (List.nth sumbits i) :: l))))
let _ = mk_dimacs "adder2.cnf" [test2] ""
46
Propositionale Logik
Modellierung nebenlaufiger Systeme
Modellierung nebenlaufiger Systeme
Man kann SAT-Solver dazu verwenden, um zu zeigen, dass einSystem nach n Schritten keinen verbotenen Zustand erreicht:Z : Systemzustande; I � S : Startzustande;V � Z : verbotene ZustandeVariablen xzt fur z P Z und 0 ¤ t n.Klauseln:
Fur alle t genau ein xzt gesetzt (vgl. Sudoku)�zPI xz0�n�2t�0
�z ÞÑz 1 xzt ^ xz 1pt�1q�n�1
t�0
�zPV xzt (verbotener Zustand erreichbar)
Das�
z ÞÑz 1 erstreckt sich uber alle Paare pz , z 1q von Zustanden,sodass z 1 Folgezustand von z ist.Hat der Zustand mehrere Komponenten z � pz1, . . . , z`q, so kannman auch Variablen xzi t einfuhren (“10� 10� 10� 10 statt10 � 10 � 10 � 10” bei vier Komponenten a 10 Moglichkeiten).47
Propositionale Logik
Modellierung nebenlaufiger Systeme
Gegenseitiger Ausschluss mit Semaphor
Gegenseitiger Ausschluss mit Semaphor
Es gibt P Prozesse, jeder Prozess ist in einem von drei Zustanden(tsleep,wait,worku).Dazu gibt es einen Semaphor mit zwei Zustanden (tfree, occu).Zu jedem Zeitpunkt macht genau ein Prozess und moglicherweiseder Semaphor eine Aktion. Moglich sind:
sleep ÞÑ wait (Semaphor unverandert)
wait ÞÑ work (nur wenn Semaphor free, anschl. occ)
work ÞÑ sleep (Semaphor anschl. free)
sleep: goto wait;
wait: if (sem==free) {sem=occ;goto work}
work: sem=free;goto sleep
48
Propositionale Logik
Modellierung nebenlaufiger Systeme
Gegenseitiger Ausschluss mit Semaphor
Modellierung mit Aussagenlogik
Variablen: Fur p P und z P tsleep,wait,worku und t n eineVariable qpzt . Außerdem fur w P tfree, occu und t n eineVariable swt .Klauseln:
Fur t n, p P, genau ein qpzt und genau ein swt gesetzt.�
p qp sleep 0 ^ sfree 0�t
�p1�p2
qp1work t ^ qp2work t�t n�1
�pp�
p1�p
�z qp1ztôqp1zpt�1qq ^�
pz,w ,z 1,w 1qPR qpzt ^ qpz 1pt�1q ^ swt ^ sw 1pt�1q
Hier ist R � tpz ,w , z 1,w 1q | z�sleep&z 1�wait&w�w 1 ||z�wait&z 1�work&w�free&w 1�occ || z�work&z 1�sleep&w 1�freeu.Siehe sema.ml fur OCAML-Modellierung.
49
Propositionale Logik
Modellierung nebenlaufiger Systeme
Peterson Algorithmus
Peterson Algorithmus
Semaphor erfordert atomares Abprufen und Setzen.Ohne solche Unterstutzung funktioniert der Peterson Algorithmus.
Zwei Prozesse 0,1. Jeder hat ein Flag flagris und es gibt eineVariable turn : t0, 1u, die angibt, wer dran ist.
Mochte ein Prozess den kritischen Bereich betreten, so signalisierter das durch Setzen seines Flags.
Sodann setzt er turn auf den jeweils anderen Prozess und wartetdann (“busy wait”), bis er an der Reihe ist oder das Flag desanderen nicht gesetzt ist.
p: 0 flag[p] := 1; goto 1
1 turn := other(p); goto 2
2 if flag[other(p)] goto 3 else goto 4
3 if turn = p goto 4 else goto 2
4 flag[p] := 0; goto 0 (* kritischer Bereich hier *)50
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
BDDs Grundidee
Man kann Boole’sche Funktionen durch Entscheidungsdiagramme(binary decision diagrams, BDDs) reprasentieren:
F T
F
x
y y
c
F T
TF
T
F
T
Ein Entscheidungsdiagramm fur die Boole’scheFunktion x^y_x^c_y^c , welche den Ubertragin einem Volladdierer berechnet.
Um zu gegebener Belegung den Funktionswertauszurechnen, verfolgt man im Entscheidungsdia-gramm den entsprechenden Pfad. Man endet dannim Knoten, der dem Funktionswert entspricht.Z.B.: x � z � true (im Diagramm “T”) undy � false (im Diagramm “F”):
F T
F
x
y y
c
F T
TF
T
F
T
51
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Grundlegende Definitionen
Definition BDD
Es wird eine Ordnung auf den Variablen fixiert.
Definition BDD
Ein BDD ist ein gerichteter azyklischer Graph mit Wurzel, so dass:
Jeder Knoten ist entweder ein Blatt oder ein innerer Knoten.
Bltter besitzen keine ausgehenden Kanten und sind mit trueoder false beschriftet.
Jeder innere Knoten ist mit einer Variablen beschriftet undbesitzt genau zwei ausgehende Kanten, die mit false, bzw.true beschriftet sind.
Auf allen Pfaden von der Wurzel zu einem Blatt treten dieVariablen gemaß der vorab fixierten Ordnung auf.
Es gibt keine zwei verschiedene isomorphe Teilgraphen,insbesondere gibt es hochstens zwei Blatter.
Kein Knoten hat zwei identische Nachfolger.52
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Grundlegende Definitionen
Beispiele
Ordnung der Variablen: x y c
F T
F
x
y y
c
F T
TF
T
F
T
F T
F
F T
TF
T
F
T
y
x x
c
Falsche
OrdnungOK
T
x
y y
c
F T
TF
F
T
FT
c
FF
T
Isomorphe
Teilgraphen
T
x
y y
c
F T
TF
T
F
T
F
c
FF
F
T
Knoten mit
ident. Nachf.
NB: “Isomorph” heißt: “bis auf Herumschieben von Knoten”.Formal: bijektive Abbildung der Knoten, die mit den Kanten undden Beschriftungen vertraglich ist. Im 2. Beispiel sind dieTeilgraphen mit Wurzel c isomorph.
53
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Grundlegende Definitionen
Erzeugung von BDDs
Ein nichtreduziertes BDD ist ein BDD, welches isomorpheverschiedene Teilgraphen und identische Nachfolger enthaltenkann. Etwa das 2.Beispiel der letzten Folie.Mit folgenden Regeln kann ein nichtreduziertes BDD in ein BDDuberfuhrt werden.
Reduktion
Knoten mit identischen Nachfolgern entfernen.
Knoten mit derselben Beschriftung und gleichen Nachfolgern(true und false Kanten) verschmelzen.
Alle true-Blatter verschmelzen; alle false-Blatter verschmelzen.
Satz: Kann keine dieser Regeln mehr angewendet werden, so liegtein BDD vor.
Bemerkung: Oft werden unsere BDDs als OBDDs (ordered BDD)oder ROBDDs (reduced OBDDs) bezeichnet.54
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Grundlegende Definitionen
Eindeutigkeit der BDDs
Satz
Definieren zwei BDDs uber derselben Ordnung dieselbe Boole’scheFunktion, so sind sie gleich (genau: isomorph).
Beweis durch Induktion uber die Große der beiden BDDs p1 und p2.
Daraus ergibt sich ein Algorithmus fur Aquivalenz Boole’scherFormeln: Fur jede der beiden BDD aufstellen; prufen, ob isomorph.
55
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Grundlegende Definitionen
Shannon Zerlegung und sub-BDDs
Shannon-Zerlegung
Sei f eine Boole’sche Funktion und x eine Variable. Mit f rx :�truesund f rx :�falses bezeichnet man die Funktionen, die man erhalt,wenn x entsprechend vorbesetzt wird.Es gilt (Shannon-Zerlegung):
f � x ^ f rx :�trues _ x ^ f rx :�falses� p x _ f rx :�truesq ^ px _ f rx :�falsesq
Beweis durch Fallunterscheidung nach x .
Ist p ein BDD und x die erste Variable, die in p abgefragt wird, sosind die beiden Nachfolger des ersten Knotens BDDs furfprx :�falses und fprx :�trues (wobei fp die durch p definierteBoole’sche Funktion ist).
56
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Negation und einstellige Operationen
Um ein BDD zu negieren, vertauscht man einfach die beidenBlatter. Damit ist die Anwendung einstelliger Boole’scherFunktionen auf ein BDD bereits erledigt, denn es gibt nur dieNegation und die Identitatsfunktion.
F T
F
x
y y
c
F T
TF
T
F
T
F T
F
x
y y
c
TF
T
F
T
T F
57
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Setzen einer Variablen
Um eine Variable x in einem BDD auf einen Boole’schen Wert bzu setzen, entfernt man alle Knoten fur diese Variable und lenktdie einlaufende Kante zum b-Nachfolger um. Anschließend ggf.reduzieren!
F T
F
x
y y
c
F T
TF
T
F
T
[y:=F]
F
x
c
TF
T
F T
Es gilt also fprx :�bs � pfpqrx :�bs (hier bezeichnet prx :�bs dasBDD p nach der Einsetzoperation). b
Spezialfalle:
x kommt in p nicht vor: prx :�bs � p
x ist p’s Kopfvariable: prx :�bs ist der entsprechendeNachfolger der Wurzel; insbes. ist keine Reduktion erford.
58
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Zweistellige Boole’sche Operationen
Sei ` eine zweistellige Boole’sche Funktion und seien p1, p2 BDDs,die die Boole’schen Funktionen f1 und f2 berechnen.
Algorithmus zur Bestimmung von p1 ` p2 fur f1 ` f2
Wir berechnen mit dynamischer Programmierung fur jedes Paarpq1, q2q, wobei q1, q2 sub-BDDs von p1, p2 sind, ein (das BDD) furdie Boole’sche Funktion g1 ` g2, wobei g1, g2 die von q1, q2
berechneten Funktionen sind.
Ist q1 ein Blatt b, so wende man die einstellige Funktionb `� auf q2 an. Fall “q2 ein Blatt” ist analog.
Seien x1 und x2 die Kopfvariablen von q1 und q2 und seio.B.d.A. x1 ¤ x2. Dann ist entweder x1 � x2 oder x1 kommtin q2 gar nicht vor. Damit sind q1rx1:�bs und q2rx1:�bssub-BDDs von q1 bzw. q2. Das ges. BDD hat Kopfvariable x1
und b-Nachfolger q1rx :�bs ` q2rx :�bs fur b � false, true.59
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Beispiel
F T T
TFT
c
T
T
F
y
y
T
c
T
F T
F
T
y
F
Fc
T
T
F T
F
x
y y
TF
T
F
c
T
T F
xTF
F
y T
T
F
F
y T
c
T
T F
c
T TF F
F T F
F
F
T
c
T
T
TF
Man berechne:
Nebenrechnungen:
T
60
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Beispiel Forts.
F
T
y
F
Fc
T
T
T
T
F Ty
T
T
F
T
y
F
Fc
T
T
T
y
F
Fc
T
T F
F Tx
F T
F
x
y y
TF
T
F
c
T
T F
xTF
F
y T
60
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Beispiel Forts.
F
T
y
F
Fc
T
T
xx
F T
F
y yT
F
c
T
T F
F
Fc
T
T FF
Fc
T
T F
y
Fc
T
T
F T
Fc
T
T F
y
c
F T
T
F
Fc
T
T F
y
c
F T
T
F
TF
F
y TT
y
F
Fc
T
T
FT
Diese Nebenrechnungen sind nicht wirklich erforderlich, illustrierenaber die Vorgehensweise zusatzlich.
61
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Existentielle Quantifizierung
In den Anwendungen ist es haufig nutzlich, eine oder mehrereVariablen existentiell zu quantifizieren.Man fuhrt das auf Einsetzen und Disjunktion zuruck:
Dx .p :� prx :�falses _ prx :�trues
Im allgemeinen wird sich die Große hier verdoppeln und also beider Quantifizierung von n Variablen ver-2n-fachen. Man hofftnaturlich, dass die jeweils anfallenden Reduktionen die Großewieder verringern.
62
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Große der BDDS
Im allgemeinen haben BDDs eine (in der Zahl der Variablen)exponentielle Große.In den praktisch vorkommenden Beispielen sind die BDDs aberhaufig beherrschbar klein.
Allerdings hangt die Große oft von der gewahlten Ordnung ab.
Es gibt viel Literatur uber die richtige Wahl der Variablenordnung. . .
63
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Beispiel einer Familie von BDDs exponentieller Große
Wir betrachten die Variablenordnung
x1 x2 � � � xn y1 y2 � � � yn
Das BDD fur die Boole’scheFunktion
�ni�1 xiôyi beginnt
mit einem vollstandigen binarenBaum der Tiefe n, in dem jededer 2n Belegungen der xi sepa-rat behandelt wird.
Danach sind die yi leicht zu be-handeln.
y1
y2
y3y3
y2
y1
x3 x3
x2
x1
x2
x3 x3
F T
T
TT
T
T
T
F
F
F F
F
T
F
F
T
T
T
F
F
F
64
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Logische Operationen auf BDDs
Selbe Funktion, andere Ordnung
Mit der Variablenordnung
x1 y1 x2 y2 x3 y3 � � � xn yn
haben die BDDs lineare Große.Alle fehlenden Kanten fuhren in das false-Blatt.
y1
y2
y3
y1
y2
y3
x1
x2
x3
T
T
T
T
T
T
TF
F
F
F
F
F
F
65
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Implementierung I
In der Praxis reprasentiert man alle wahrend einer Sitzungauftretenden BDDs nur einmal (sharing):
Treten zum Beispiel die Funktionen f1 �xôy , f2 � y , f3 � x ^ y auf, soentsteht nebenstehendes Diagramm: F
T TF
TF
y y
xxT
FF
Tf
ff
3
21
Gleichheit von BDDs ist dann einfach Gleichheit von Zeigern.
66
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Implementierung II
Um festzustellen, ob ein gerade benotigter BDD schonvorhanden ist, verwendet man eine Hashtabelle.
Den Hashwert eines BDDs berechnet man aus derKopfvariablen und (rekursiv) aus den Hashwerten der beidenNachfolger.
Vgl. Behandlung von Stringliteralen in Java.
67
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Implementierung III
Anstatt einen BDD durch Vertauschen der Blatter zukomplementieren, kann man auch in jedem Knoten einKomplementbit vorsehen, welches besagt, dass sich derdarunterliegende BDD komplementiert versteht.
Man kann fur jeden Knoten einen Referenzzahler einfuhren,der die Zahl der Verweise auf den Knoten mitzahlt. Sind keinevorhanden, so kann er freigegeben werden. (“garbagecollection”).
Es gibt viele BDD-Bibliotheken mit Frontends furverschiedene Programmiersprachen. Wir verwenden dieC-Bibliothek CUDD mit dem OCAML-InterfaceMLCUDDIDL. Es gibt auch Java, C++, Perl Interfaces.
68
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Das cudd Interface mlcuddidl
Verwendet die C-Bibliothek CUDD (F. Somenzi)
Installation und Compilierung siehe Doku, bzw. Makefile
Standalone Programme konnen auf das Modul Cudd zugreifen,welches die Untermodule Man (Sitzungsmanager) und Bdd
(BDDs) enthalt. Typischerweise offnet man alle drei Module.
Zum Experimentieren empfiehlt sich der OCAML-Toplevelcuddtop. In diesem ist Cudd bereits geoffnet.
69
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Beispielsitzung mit mlcuddidl
# open Cudd;;
# open Bdd;;
# open Man;;
# let man = make_d();;
val man : Cudd.Man.d Cudd.Man.t = <abstr>
# let x = newvar man;;
val x : Cudd.Man.d Cudd.Bdd.t = <abstr>
# let y = newvar man;;
val y : Cudd.Man.d Cudd.Bdd.t = <abstr>
# let c = newvar man;;
val c : Cudd.Man.d Cudd.Bdd.t = <abstr>
# let carry = dor (dand x y) (dor (dand x c) (dand y c));;
val carry : Cudd.Man.d Cudd.Bdd.t = <abstr>
# is_equal carry (dor x (dor y c));;
- : bool = false
# is_equal carry (dor (dand x (dor y c)) (dand y c));;
- : bool = true70
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Implementierung von BDDs
Lookahead Addierer mit CUDD
Der Programmtext ist ahnlich wie bei der Losung mit SAT-Solver.Siehe adder.ml.Unterschiede:
Variablen werden mit newvar man erzeugt (man ist der zuvorerzeugte Manager).
dors dands fordo mussen selbst definiert werden.
Einige Funktionen heißen anders: Z.B. neg heißt dnot, sieheDoku.Test auf Gleichheit erfolgt mit is equal:let rec test i = if i=0 then true else
let s,c = lookaheadaddbit (i-1) in
is_equal s (List.nth sumbits (i-1)) &
(if i = size then is_equal carryout c else true)&
test (i-1)
let _ = if test size then print_string "OK\n"
else print_string "Error!\n"71
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Nebenlaufige Systeme mit BDDs
BDDs erlauben eine Modellierung nebenlaufiger Systeme ohneZeitschranke (“tmax”).Wir fuhren zunachst nur Variablen ein, die den Zustand zueinem festen aber beliebigen Zeitpunkt beschreiben.Im Beispiel “Semaphor” waren dies also: Fur p P undz P tsleep,wait,worku je eine Variable qpz . Außerdem furw P tfree, occu je eine Variable swJeder Zustand zu einem gewissen Zeitpunkt entspricht alsoeiner Belegung dieser Variablen.Mengen von Zustanden entsprechen demnach Boole’schenFunktionen (besser: Ausdrucken) uber diesen Variablen.Ziel ist nun, ein BDD uber diesen Variablen zu finden, welchesgerade die Menge der von einem (hier: dem) Anfangszustandaus erreichbaren Zustande reprasentiert.Man kann dann prufen, ob diese Menge verbotene Zustandeenthalt.72
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Semaphor mit BDDs
Sinnvolle Zustande:
sanity �©
p
ª
z
qpz^©
z�z 1
qpz 1^psfree_soccq^ psfree^soccq
Anfangszustand(e):
initial � sanity^©
p
qpsleep ^ sfree
Verbotene Zustande:
undesired � sanity^ª
p p1
qpwork ^ qp1work
Erreichbare Zustande:
reachable � “siehe nachste Folien”
Man prufe, ob reachable^ undesired � K. Wenn ja: OK; wennnein: System fehlerhaft.
73
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Zustandsubergangsrelation
Fuhre einen zweiten Satz Variablen fur Folgezustand ein: q1pzund s 1w .
Wahle Variablenordnung so, dass eine gestrichene Variableimmer unmittelbar auf ihr ungestrichenes Pendant folgt, alsonicht: erst alle ungestrichenen, dann alle gestrichenen.
Definiere nun BDD next fur die Relation “ist moglicherFolgezustand von”. Im Beispiel:
next �ª
p
p©
p1�p
©
z
qp1zôq1p1ztq^ª
pz,w ,z 1,w 1qPR
qpz^q1pz 1^sw^s 1w 1
wobei R � tpz ,w , z 1,w 1q | z�sleep&z 1�wait&w�w 1 ||z�wait&z 1�work&w�free&w 1�occ || z�work&z 1�sleep&w 1�occu.
74
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Iteration
Fur i � 0, 1, 2, 3, . . . berechne nun die Menge reachi der inhochsten i Schritten erreichbaren Zustande. Es ist:
reach0 � initial,
Falls reachi bereits definiert ist, so ist
reachi�1 � reachi _ sanity^ substpexistspreachi ^ nextqq
Hier bezeichnet:
exists die existentielle Quantifizierung der ungestrichenenVariablen. Die Formel (BDD) existspreachi ^ nextq enthaltalso nur noch die gestrichenen Variablen;
subst die Ersetzung der gestrichenen Variablen durch dieungestrichenen.
Bezeichnen wir mit s, s 1, s Kopien der Variablensatze und machenwir die Abhangigkeiten durch Klammern explizit, so haben wirintuitiv: reachi�1psq � reachi psq _ Ds.reachi psq ^ nextps, sq.75
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Erreichbare Zustande
Es ist klar, dass reachi ñ reachi�1 Tautologie ist.
“In hochstens i Schritten” impliziert ja “in hochstens i � 1Schritten. Da es nur endlich viele Zustande gibt, muss es also eini0 geben, sodass
reachi0 � reachi0�1
Ab diesem Zeitpunkt i0 andert sich also nichts mehr und reachi0
beschreibt somit die Menge der uberhaupt erreichbaren Zustande.
Wie gesagt, ist i0 hochstens so groß wie die Zahl der Zustande. Inder Praxis ist i0 aber meist viel kleiner. Es ist ja die maximale Zeit,nach der jeder uberhaupt erreichbare Zustand erreicht wird. ImSemaphorbeispiel ist z.B. i0 � |P| � 1.
76
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Algorithmus zur Berechnung der erreichbaren Zustande
Mit folgendem Algorithmus kann man also die erreichbarenZustande als BDD berechnen.
new :� Krepeat
old :� newnew :� old_ sanity^ substpexistspold^ nextqq
until new � oldreach :� new
Die Abbruchbedingung in der repeat-until Schleife kann beiBDD-Reprasentation in konstanter Zeit gepruft werden.
Siehe bdd.tgz fur entsprechende Implementierung fur Semaphorund Petersons Algorithmus.
77
Propositionale Logik
BDDs (binare Entscheidungsdiagramme)
Nebenlaufige Systeme mit BDDs
Zusammenfassung Kapitel 1
Wdh. Aussagenlogik
Erfullungsaquivalente KNF mit Tseitin Ubersetzung
DPLL Algorithmus, SAT Solver
Aquivalenz von Schaltkreisen, Bsp. Lookahead Addierer
Modellierung nebenlaufiger Systeme durch exhaustiveSimulation in Aussagenlogik
Binare Entscheidungsdiagramme BDDs, Definition undGrundalgorithmen
Implementierung von BDDs
Modellierung nebenlaufiger Systeme mit BDDs, Berechnungaller erreichbarer Zustande durch Fixpunktiteration.
78