Die Suche ergab 104 Treffer

von L4_
7. Apr 2013 13:39
Forum: Archiv
Thema: Klausur - LTL auswerten - No- oder weak-fairness als default
Antworten: 5
Zugriffe: 831

Re: Klausur - LTL auswerten - No- oder weak-fairness als def

Strong fairness wird nicht relevant sein, wurde nur kurz angestochen. Aber schau dir die Formel aus der Lösung von Ü3, P6 an: Weak Fairness: [] enabled A -> <> taken A (Strong Fairness: []<> enabled A -> <> taken A) D.h. ein programm würde bei strong fairness auch zweige nehmen, die zwischendurch ma...
von L4_
6. Apr 2013 16:17
Forum: Archiv
Thema: Übung 6, P1 und P2 - Alternative Lösung?
Antworten: 5
Zugriffe: 634

Re: Übung 6, P1 und P2 - Alternative Lösung?

Joa, 0 ist eben nicht positiv :D
Ich weiß, dass die auch bei P2 zwischen "positive" und "strictly positive" unterscheiden, aber mathematisch gesehen ist dadurch die 0 immer noch keine positive Zahl :P
von L4_
6. Apr 2013 16:13
Forum: Archiv
Thema: Übung 6, P1 und P2 - Alternative Lösung?
Antworten: 5
Zugriffe: 634

Re: Übung 6, P1 und P2 - Alternative Lösung?

x ist doch positiv dachte ich ;)

Bzw. nach der Musterlösung steht dann wieder x => 0 als invariante - aber abgesehen davon.
Wir nehmen nunmal an, dass bei P1 und P2 von positiven zahlen gesprochen wird.
von L4_
6. Apr 2013 16:04
Forum: Archiv
Thema: Übung 6, P1 und P2 - Alternative Lösung?
Antworten: 5
Zugriffe: 634

Übung 6, P1 und P2 - Alternative Lösung?

Hallo, in P1 hatte ich alles gleich bis auf folgendes: loop_invariant (y >= 0) && (x - (z/x) == y) in P2 folgendes anders: ensures \result == x/y loop_invariant (x1 >= 0) && (x/y == x1/y + q) Ich sah dabei auf den ersten Blick keine Probleme und hätte gesagt, dass es soweit passt. Was meint ihr dazu...
von L4_
5. Apr 2013 14:42
Forum: Archiv
Thema: Frage zu LTL Formeln ohne Quantifier am Anfang
Antworten: 1
Zugriffe: 416

Frage zu LTL Formeln ohne Quantifier am Anfang

Hallo, bisher stellten wir in Labs, als auch in anderen Aufgaben Formeln auf, die mindestens ein "[]" oder "<>" als Präfix hatten. Das macht ja auch durchaus Sinn. Aber wie sieht das denn nun für eine LTL Formel auf, die z.B. folgende Form hat: 1. "p && q || r" 2. "p -> <>q" (eine Mischung, also nic...
von L4_
5. Apr 2013 14:32
Forum: Archiv
Thema: weak fairness
Antworten: 6
Zugriffe: 1220

Re: weak fairness

Okay super, das hilft mir nun noch besser und jetzt verstehe ich auch die Formel aus Ü3, Problem6 besser:

Weak fairness:
Für alle Aktionen A gilt:
[] enabled A -> <> taken A

Und wenn die Voraussetzung falsch ist, darf spin den Zweig ignorieren.
Danke! :)
von L4_
5. Apr 2013 14:05
Forum: Archiv
Thema: weak fairness
Antworten: 6
Zugriffe: 1220

Re: weak fairness

Okay, ich glaub es sitzt nun ;)

Wenn ich nun "pan" mit -f starte, dann wird weak fairness erzwungen.
Ist denn dann ohne -f keine weak fairness, sprich gilt dann starke fairness?
von L4_
5. Apr 2013 13:52
Forum: Archiv
Thema: weak fairness
Antworten: 6
Zugriffe: 1220

Re: weak fairness

Ohne weak fairness gilt hier folgende Formel zum Beispiel nicht: \diamond var Denn wenn wir einfach immer den unteren Fall von do nehmen wird var niemals true werden. Ich bin bei der Bedeutung von "weak fairness" und dem Gegenteil davon immer noch nicht im klaren. In deinem Beispiel hätte ich jetzt...
von L4_
18. Mär 2013 17:48
Forum: Archiv
Thema: Übung 4 e)
Antworten: 5
Zugriffe: 1422

Re: Übung 4 e)

Noch präziser:

\(c_1^{-a} \Longleftrightarrow c_1^{k\varphi(n)-a}\), wobei k element aus den ganzen Zahlen ist ;)
von L4_
16. Mär 2013 18:35
Forum: Archiv
Thema: Übung 7 - Bell-La Padula
Antworten: 4
Zugriffe: 1352

Re: Übung 7 - Bell-La Padula

Ich selbst unterscheide immer zwischen potenziellen Rechten (durch Einteilung in eine Sicherheitsklasse) und expliziten Rechten (jene, die durch die Relationen festgelegt werden) Das explizite Recht impliziert das potenzielle. Mit "nahezu eindeutig" habe ich das wie folgt verstanden (angelehnt an di...
von L4_
15. Mär 2013 11:23
Forum: Archiv
Thema: Klausurergebnis und Einsicht
Antworten: 44
Zugriffe: 7909

Re: Klausurergebnis und Einsicht

Frage zur Einsicht: Kann man damit rechnen, dass die Einteilung Einsichtszeiten auch strikt ist und funktionieren wird? In GDI2 letztes Semester war das beispielsweise absolut chaotisch, daher die Frage. Würde an dem Tag nämlich gerne meinem Plan nachgehen und dann wäre es ungünstig, wenn ich zwar p...
von L4_
15. Mär 2013 11:11
Forum: Archiv
Thema: Übung 8, Wechselseitige Authentifikation sicher gegen Replay
Antworten: 4
Zugriffe: 1521

Re: Übung 8, Wechselseitige Authentifikation sicher gegen Re

Okay danke, das hilft mir schonmal mehr um den Unterschied zu verstehen - damit wäre meine eigentliche Frage auch beantwortet. Aber ist das im Allgemeinen so, dass man Nonces auch durch beliebige Zufällige Zahlen ersetzen darf und sie somit nicht speichern bräuchte? Ich dachte immer, dass die Zahlen...
von L4_
15. Mär 2013 01:11
Forum: Archiv
Thema: Übung 8, Wechselseitige Authentifikation sicher gegen Replay
Antworten: 4
Zugriffe: 1521

Übung 8, Wechselseitige Authentifikation sicher gegen Replay

Hallo, ich sah gerade in meinen Notizen die Lösung, die wir durch einen Tutor mal an die Tafel angeschrieben bekamen. Diese lautet: (I) A \rightarrow B: A, N_A (II) B \rightarrow A: B, Sig(N_A)_B, N_B (III) A \rightarrow B: Sig(N_B)_A Jetzt soll das gegen Replay-Attacken sicher sein. Jedoch musste i...
von L4_
14. Mär 2013 11:44
Forum: Archiv
Thema: Wie war die Klausur
Antworten: 10
Zugriffe: 2010

Re: Wie war die Klausur

Ich bin irgendwie skeptisch bei der CSP Aufgabe mit den Ampeln. A und F hatten die gleiche Ereignismenge. Das bringt doch das Problem mit sich, dass keiner der beiden Prozesse jeweils einen Schritt alleine gehen durfte. Ist also der Teilausdruck "FußRot -> ..." in F drin, dann muss nach der Definiti...
von L4_
12. Mär 2013 14:09
Forum: Archiv
Thema: Modul13 - Alphabet von Charlie richtig angegeben?
Antworten: 1
Zugriffe: 433

Modul13 - Alphabet von Charlie richtig angegeben?

Hallo, wenn ich das richtig verstehe, dann ist doch im Alphabet von Charlie send.u.m für beliebige u und m möglich. Ich sehe hier das Problem, dass dann die Spur t = ( send.A.{A.Na}_Pu(C) ) nicht in Alice || Bob || Charlie || Net({}) drin wäre, obwohl es ja so sein sollte! Denn es gilt: t "projezier...

Zur erweiterten Suche