Modellierung nebenl au ger Systeme Mir besch aftigen uns ... fileOrganisatorischesEinf uhrung...

$: Modellierung nebenl au ger Systeme Mir besch aftigen uns ... fileOrganisatorischesEinf uhrung TransitionssystemeProzesskalk ule PetrinetzeGraphtransformationGoogle Go Vorlesung \Modellierung$
Organisatorisches Einfuhrung Transitionssysteme Prozesskalkule Petrinetze Graphtransformation Google Go

Vorlesung “Modellierung nebenlaufiger Systeme”Sommersemester 2014

Universitat Duisburg-Essen

Barbara KonigUbungsleitung: Sebastian Kupper

Barbara Konig Vorlesung “Modellierung nebenlaufiger Systeme” 1


Prozesskalkule: Motivation

Mir beschaftigen uns nun mit sogenannten Prozesskalkulen, dassind “Mini-Programmiersprachen”, mit denen man interagierendeProzesse beschreiben kann.

Nutzen von Prozesskalkulen

Programmiersprache, mit der man Systeme modular ausProzessen aufbauen kann

Studium von Interaktion, Parallelitat, Modularitat

Einfachheit, um den Kalkul formal untersuchen undAnalysetechniken aufstellen zu konnen(Trade-off zwischen der Machtigkeit einer Sprache und ihrerAnalysierbarkeit)




Was gibt es in Prozesskalkulen?

Kommunikation uber Kanale

Interaktion mit der Umgebung/Reaktivitat

Parallele Komposition

Verschatten von Aktionen gegenuber der Umwelt

Nicht-deterministische Verzweigungen

Was gibt es (im Allgemeinen) nicht in Prozesskalkulen?

Datentypen (Integers, Booleans, . . . )

Sprachkonstrukte wie Funktionen, Prozeduren, Schleifen, . . .

Dies kann jedoch (mit etwas Aufwand) simuliert werden, denn allehier von uns betrachteten Prozesskalkule sind Turing-machtig.




Welche Prozesskalkule gibt es?

CCS (Calculus of Communicating Systems) – eingefuhrt 1980von Robin Milner

CSP (Communicating Sequential Processes) – eingefuhrt vonTony Hoare (dieser Kalkul enthalt mehr primitive Operatorenund erlaubt – im Gegensatz zu CCS – auch Synchronisationvon mehr als zwei Kommunikationspartnern.)

π-Kalkul – enthalt die Moglichkeit, Kanalnamen als Inhalt vonNachrichten zu verschicken und damit die Topologie derKommunikationsstruktur dynamisch zu verandern




Spi-Kalkul – Erweiterung des π-Kalkuls um kryptographischePrimitive zur Analyse von kryptographischen Protokollen

Angewandter π-Kalkul – Verallgemeinerung des Spi-Kalkuls,Anreicherung des π-Kalkuls mit Termen und Gleichungen.

Ambient-Kalkul – modelliert die Mobilitat von sogenanntenAmbients, die als Container fur mobilen Code aufgefasstwerden konnen

. . .

Wir beschaftigen uns vor allem mit CCS.



CCS: Motivation

1. Idee: Transitionssysteme in textueller Form notieren

A

B C D

ab

a

c d A := a.B + b.C + a.D

B := c .A

C := 0

D := d .A

Abgekurzt: A, mit A := a.c .A + b.0 + a.d .A.



CCS: Motivation

Bedeutung der Symbole:

a.P steht fur eine Aktion a, gefolgt von Prozess P. Diesessyntaktische Konstrukt heißt auch Prafix. Es ist eineeingeschrankte Form der sequentiellen Komposition.

P1 + P2 steht fur nicht-deterministische Auswahl. DerTeilprozess Pi , der zuerst eine Aktion durchfuhrt, “gewinnt”und arbeitet weiter, der andere Teilprozess wird verworfen.

0 steht fur den inaktiven Null-Prozess, der keine Aktionenmehr ausfuhrt.



CCS: Motivation

2. Idee: Parallele Komposition von Prozessen erlauben

Beispiel: Prozessa.0 | b.0Die beiden Prozessekonnen unabhangigvoneinanderAktionen ausfuhren.

a.0 | b.0a

yy

b

%%

0 | b.0

b%%

a.0 | 0

ayy

0 | 0

Weiteres Beispiel: A | C mit A := a.b.A, C := c .d .C .



CCS: Motivation

3. Idee: Synchronisation von Ein-/Ausgabe-Aktionen

Zueinanderpassende Ein- undAusgabeaktionen aund a konnen sichsynchronisieren undzu einer internenAktion τ werden.

Beispiel: a.P | a.Q

a.P | a.Q

ayy

τ

��

a

%%

P | a.Qa

%%

a.P | Q

ayy

P | Q

Bemerkungen:

Zu beachten ist, dass eine Synchronisation stattfinden kann,aber nicht muss (siehe obiges Transitionssystem).

Eine Aktion a heißt auch Koaktion. Es gilt a = a und τ = τ .



CCS: Motivation

4. Idee: Verschattung

Bestimmte Aktionen sollen nachaußen hin nicht sichtbar sein, siewerden verschattet (bzw.restringiert).

Falls eine Aktion a nach außenhin verschattet ist, so kannSynchronisation uber a nur nochintern stattfinden.

Beispiel: (a.P | a.Q)\{a}

(a.P | a.Q)\{a}τ

��

(P | Q)\{a}

Bemerkung: In diesem Fall mussen die beiden parallelen Prozessea.P, a.Q kommunizieren.



CCS: Motivation

5. Idee: Umbenennung

Aktionen konnen, bevorsie nach außen gegebenwerden, umbenanntwerden.

Beispiel: (a.b.0)[a/c , b/d ]

(a.b.0)[a/c , b/d ]

c

��

(b.0)[a/c , b/d ]

d��

0[a/c, b/d ]



CCS: Motivation

Bemerkungen zu Umbenennungen:

Bei einer Umbenennung der Form [a/b, b/c] werden alleUmbenennungen “gleichzeitig” ausgefuhrt. Insbesonderewerden alle a’s zu b’s umbenannt (und nicht zu c ’s).

Dagegen beschreibt [a/b][b/c] die Hintereinanderausfuhrungzweier Umbenennungen, d.h., a wird zu c umbenannt.



CCS: Syntax und Semantik

Nach dieser (informellen) Motivation beschreiben wir nun formaldie Syntax und Semantik von CCS-Prozessen.

Syntax von CCS (Definition, Teil 1)

Sei L eine Menge von Labels und Act = {τ} ∪ L ∪ {a | a ∈ L} dieMenge aller Aktionen.

Ein CCS-Prozess ist entweder

der inaktive Prozess 0,

ein Prozess der Form a.P, wobei a ∈ Act,

eine nichtdeterministische Auswahl P1 + P2,

eine parallele Komposition P1 | P2,

eine Restriktion P\L, wobei L ⊆ L,




Syntax von CCS (Definition, Teil 2)

eine Umbenennung P[f ], wobei f : L → L eineUmbennungsfunktion ist, oder

eine Konstante A, wobei A mit einer Definition der FormA := P festgelegt werden muss.

Dabei sind P,P1,P2 wiederum Prozesse.




Wir wollen nun fur einen Prozess die moglichen Transitionenbestimmen. Dabei bedeutet P

a→ Q, dass Prozess P einena-Ubergang machen kann und dabei zu Q wird.

Alle Transitionen eines CCS-Prozesses kann man mit Hilfe vonAbleitungsregeln herleiten, die von folgender Form sind:

X1, . . . ,Xn

Y

angegeben. Dies bedeutet, wenn die Vorbedingungen (oderPramissen) X1, . . . ,Xn erfullt sind, dann kann man daraus dieFolgerung Y ziehen.

Es kann auch n = 0 gelten, das heißt, es gibt keineVoraussetzungen und die Folgerung Y gilt immer.




(Act)a.P

a→ P(Con)

Pa→ P ′

Aa→ P ′

falls A := P

(Plus1)P

a→ P ′

P + Qa→ P ′

(Plus2)Q

a→ Q ′

P + Qa→ Q ′

(Par1)P

a→ P ′

P | Q a→ P ′ | Q (Par2)Q

a→ Q ′

P | Q a→ P | Q ′

(Par3)P

a→ P ′,Q a→ Q ′

P | Q τ→ P ′ | Q ′falls a, a 6= τ




(Res)P

a→ P ′

P\L a→ P ′\L falls a, a 6∈ L

(Ren)P

a→ P ′

P[f ]f (a)→ P ′[f ]

wobei f (τ) = τ , f (a) = f (a)

Diese Art der induktiven Semantik nennt man auch SOS-Semantik(SOS = Structural Operational Semantics).




Beispiel: Ableitung einer Transition des Prozesses

((b.0)[b/a] | (a.0 | b.0))\{a}

(Act) b.0b→ 0 a.0

a→ 0 (Act)

(Ren) (b.0)[b/a]a→ 0[b/a] a.0 | b.0 a→ 0 | b.0 (Par1)

(Par3) (b.0)[b/a] | (a.0 | b.0)τ→ 0[b/a] | (0 | b.0)

(Res) ((b.0)[b/a] | (a.0 | b.0))\{a} τ→ (0[b/a] | (0 | b.0))\{a}

Die zweite Transition, die fur diesen Prozess moglich ist:

((b.0)[b/a] | (a.0 | b.0))\{a} b→ ((b.0)[b/a] | (a.0 | 0))\{a}




Mit einem CCS-Prozess P kann man immer das zugehorigeTransitionssystem TS(P) verbinden.

Transitionssystem eines Prozesses (Definition)

Sei P ein CCS-Prozess. Das Transitionssystem eines Prozessesbesteht aus:

der Zustandsmenge Z , diese Menge enthalt P selbst und alleProzesse, die von P aus uber Transitionen erreichbar sind, und

der Transitionsrelation → zwischen den Prozessen in Z , dievon den vorher angegeben Ableitungsregeln beschrieben wird.

Bemerkung: das Transitionssystem eines Prozesses kann unendlichgroß sein. Ein Beispiel ist der Prozess A := a.(b.0 | A).



Synchrone vs. asynchrone Kommunikation

In CCS ist Kommunikation zunachst immer synchron, d.h., beideKommunikationspartner warten aufeinander (= Rendezvous) undmachen erst dann weiter, wenn der jeweils andere die Nachricht(bzw. die Aktion) empfangen hat:

a.P | a.Q τ→ P | Q

Asynchrone Kommunikation ist ebenfalls moglich, wenn einProzess abgespalten wird, der parallel lauft und dessen einzigerZweck es ist, die Nachricht zu verschicken:

(a.0 | P) | a.Q w→ (a.0 | P ′) | a.Q τ→ 0 | P ′ | Q,

falls Pw→ P ′. Das heißt, der Prozess P kann weiterarbeiten, bevor

Q die Nachricht empfangt.



Modellierung des Alternating Bit Protocols

Wir modellieren nun das Alternating Bit Protocol mit CCS.

Beschreibung: Alternating Bit Protocol

Sender und Empfanger tauschen Nachrichten uber einenfehlerhaften Kanal aus, der Nachrichten verlieren kann.

Jede angekommene Nachricht wird vom Empfanger unterAngabe der Sequenznummer bestatigt. Es werden nur dieSequenznummern 0, 1 (alternierend) verwendet.

Der Sender sendet so lange die gleiche Nachricht, bis er eineBestatigung fur sie erhalten hat. Dann geht er zur nachstenNachricht uber.




Uberlegungen zur Modellierung:

Wir abstrahieren vom Inhalt der Nachrichten, d.h., dieAktionen verraten nur, von welchem Typ die Nachricht ist(eigentliche Nachricht oder Bestatigung) und welcheSequenznummer (0 oder 1) mitgeschickt wird.

Von außen sollen nur die Aktionen accept und deliver sichtbarsein. Mit accept empfangt der Sender eine Nachricht derAnwendung, die zu verschicken ist, und mit deliver liefert sieder Empfanger an seine Anwendung aus.

Das unzuverlassige Kommunikationsmedium (der Kanal) wirdebenfalls durch einen Prozess modelliert, der die Nachrichtenentweder weitergeben oder verlieren kann.




Modellierung des Senders: der Sender verwendet – neben accept –folgende Aktionen:

s0, s1: Nachricht mit Sequenznummer 0 bzw. 1 wird versandt.

rack0, rack1: Bestatigung fur Sequenznummer 0 bzw. 1 wirdempfangen (“receive acknowledgement”).

Modellierung des Empfangers: der Empfanger verwendet – nebendeliver – folgende Aktionen:

r0, r1: Nachricht mit Sequenznummer 0 bzw. 1 wirdempfangen.

sack0, sack1: Bestatigung fur Sequenznummer 0 bzw. 1 wirdversandt. (“send acknowledgement”).




Modellierung des Senders als Transitionssystem und Prozess

accept

S ′0

s0

rack1

accept

s1

S0

S1

S ′1

S ′′1

S ′′0rack0

s1

s0

rack1

rack0

S0 := accept.S ′0S ′0 := s0.S

′′0

S ′′0 := s0.S′′0 + rack0.S1 + rack1.S

′′0

S1 := accept.S ′1S ′1 := s1.S

′′1

S ′′1 := s1.S′′1 + rack1.S0 + rack0.S

′′1




Modellierung eines zuverlassigen Kanals als Transitionssystem undProzess

MsafeSR

s0 r0

r1 s1

MsafeRS

sack1rack1

sack0 rack0

|

MsafeSR := s0.r0.MsafeSR

+ s1.r1.MsafeSR

MsafeRS := sack0.rack0.MsafeRS

+ sack1.rack1.MsafeRS

Msafe := MsafeSR | MsafeRS

(Hin-)Kanal vom Sender zum Empfanger: MsafeSR(Ruck-)Kanal vom Empfanger zum Sender: MsafeRS




Modellierung eines unzuverlassigen Kanals als Prozess

MlossySR := s0.r0.MlossySR+s0.MlossySR

+ s1.r1.MlossySR+s1.MlossySR

MlossyRS := sack0.rack0.MlossyRS+sack0.MlossyRS

+ sack1.rack1.MlossyRS+sack1 .MlossyRS

Mlossy := MlossySR | MlossyRS




Modellierung des Empfangers als Transitionssystem und Prozess

R0

R1

r0

sack0

r1

deliver

deliver

sack1

sack0

sack1

r1

r0

R0 := r0.deliver .sack0.R1

+ r1.R0

+ sack1.R0

R1 := r1.deliver .sack1.R0

+ r0.R1

+ sack0.R1




Modellierung des gesamten Protokolls

Mit zuverlassigem Kanal:

ABPsafe := (S0 | Msafe | R0)\{r0, r1, s0, s1, rack0, rack1,

sack0, sack1}

Mit unzuverlassigem Kanal:

ABPlossy := (S0 | Mlossy | R0)\{r0, r1, s0, s1, rack0, rack1,

sack0, sack1}




Spezifikation

Folgendes Verhalten sollte von außen sichtbar sein:

Spec := accept.deliver .Spec

Frage: Sind ABPlossy und Spec verhaltensaquivalent, das heißt,ununterscheidbar aus der Sicht eines externen Beobachters?



Verhaltensaquivalenzen

Im folgenden wollen wir uns vor allem damit beschaftigen, welcheProzesse das gleiche Verhalten zeigen, obwohl sie syntaktischverschieden sind. Als Verhaltensaquivalenz verwenden wir schwacheund starke Bisimularitat.

Bisimularitat von Prozessen (Definition)

Zwei CCS-Prozesse P,Q heißen (stark) bisimular (in Zeichen:P ∼ Q), wenn ihre Zustande in den Transitionssystemen von Pund Q (stark) bisimular sind.Analog ist schwache Bisimularitat (in Zeichen: P ≈ Q) definiert.




Beispiele: sind folgende Paare P,Q von Prozessen stark bisimular,d.h., P ∼ Q?

1 P = 0 Q = a.0

2 P = 0 Q = τ.0

3 P = 0 Q = (a.0)\{a}4 P = a.0 + b.0 Q = a.0 | b.05 P = a.b.0 + a.c .0 Q = a.(b.0 + c .0)

6 P = a.b.0 + b.a.0 Q = a.0 | b.07 P = a.a.0 + a.a.0 Q = a.0 | a.08 P = a.a.0 + a.a.0 + τ.0 Q = a.0 | a.09 P,Q mit P := a.b.P, Q := a.b.a.b.Q

10 P = a.0 | a.0 Q = τ.0

11 P = (a.0 | a.0)\{a} Q = τ.0




Beispiele: sind folgende Paare P,Q von Prozessen schwachbisimular, d.h., P ≈ Q?

1 P = 0 Q = τ.0

2 P = a.0 | a.0 Q = τ.0

3 P = (a.0 | a.0)\{a} Q = 0

4 P = τ.(a.0 + b.0) Q = a.0 + b.0.

5 P = τ.(a.0 + b.0) Q = τ.a.0 + τ.b.0.

6 P = a.(b.0 + τ.c .0) Q = a.(b.0 + τ.c .0) + a.c.0



Strukturelle Kongruenz

Manche Prozesse sind strukturell so ahnlich, dass wir sofort sagenkonnen, dass die entsprechenden Prozesse (stark) bisimular sind.

Beispiele:

0 | 0 ∼ 0 0 | P ∼ P P | Q ∼ Q | P P + P ∼ P

Zwei Prozesse, die im wesentlichen die gleiche Struktur habennennt man strukturell kongruent.




Strukturelle Kongruenz (Definition, Teil 1)

Folgende Regeln beschreiben, wann zwei Prozesse P,Q strukturellkongruent sind (in Zeichen: P ≡ Q).

P1 | (P2 | P3) ≡ (P1 | P2) | P3 P1 | P2 ≡ P2 | P1

P | 0 ≡ P

(Diese drei Regeln besagen, dass die parallele Kompositionassoziativ und kommutativ ist und 0 als neutrales Element hat.)





P1 + (P2 + P3) ≡ (P1 + P2) + P3 P1 + P2 ≡ P2 + P1

P + 0 ≡ P P + P ≡ P

(Auch die nicht-deterministische Auswahl ist assoziativ undkommutativ, hat 0 als neutrales Element und erfullt außerdemnoch P + P ≡ P.)





P ≡ P

P1 ≡ P2

P2 ≡ P1

P1 ≡ P2,P2 ≡ P3

P1 ≡ P3

(Diese Regeln besagen, dass ≡ reflexiv, symmetrisch und transitivist, d.h., eine Aquivalenzrelation ist.)





P1 ≡ P2

a.P1 ≡ a.P2

P1 ≡ P2

P1\L ≡ P2\LP1 ≡ P2

P1[f ] ≡ P2[f ]

P1 ≡ P2,Q1 ≡ Q2

P1 | Q1 ≡ P2 | Q2

P1 ≡ P2,Q1 ≡ Q2

P1 + Q1 ≡ P2 + Q2

(Diese Regeln besagen, dass ≡ unter den CCS-Operatoren erhaltenbleibt. Man sagt dazu auch: ≡ ist eine Kongruenzrelation.)




Beispiele: folgende Prozesse sind strukturell kongruent, was mitHilfe der obigen Regeln bewiesen werden kann.

0 | P ≡ P

0 + P ≡ P

P + (0 + Q) ≡ P + Q

a.(0 + P) ≡ a.P




Strukturelle Kongruenz und Bisimularitat (Satz)

Die Relation ≡ auf CCS-Prozessen ist eine starke Bisimulation.

(Ohne Beweis)

Bemerkung: Die strukturelle Kongruenz ≡ ist allerdings nicht diegroßte Bisimulation. D.h., sie ist feiner als die Bisimularitat ∼.



Prioritaten der Operatoren

Prioritaten der Operatoren

\L (Verschattung) und [f ] (Umbenennung) binden starker alsalle anderen Operatoren

a. (Prafix) bindet starker als || (parallele Komposition) bindet starker als +

+ (nicht-deterministische Auswahl) bindet am schwachsten

Daher: a.P | Q + b.R\L wird geklammert als((a.P) | Q) + (b.(R\L)).



Up-To-Techniken/Modulo-Techniken

Motivation: wir wollen zeigen, dass die Prozesse A,B mit

A := a.(A | 0) B := a.B

stark bisimular sind.

Problem: die kleinste Bisimulation R, die das Paar (A,B) enthalt,ist unendlich groß, namlich:

R = {(A,B), (A | 0,B), (A | 0 | 0,B), (A | 0 | 0 | 0,B), . . . }

Kann man Bisimularitat auch mit einer endlichen Relation zeigen?

Idee: Wir betrachten die Relation R ′ = {(A,B)}. Das Paar(A | 0,B), das nach einem Schritt erreicht wird, ist “beinahe”schon in R ′ enthalten, denn es gilt A | 0 ∼ A (sogar: A | 0 ≡ A).




Wir betrachten nun sogenannte Up-To-Bisimulationen(“bisimulation up to . . . ” heißt ubersetzt “Bisimulation bis auf. . . ”). Wir sagen auch Modulo-Bisimulationen.

Bisimulation modulo starke Bisimularitat (Definition)

Eine Relation R heißt (starke) Bisimulation modulo starkeBisimularitat, falls fur jedes Paar (P1,P2) ∈ R und fur jede Aktiona ∈ Act gilt:

fur jedes Q1 mit P1a→ Q1 gibt es ein Q2 mit P2

a→ Q2 und(Q1,Q2) ∈∼ R ∼.


a→ Q1 und(Q1,Q2) ∈∼ R ∼.

Dabei ist ∼ R ∼ die Verknupfung dreier Relationen und es giltQ1 ∼ R ∼ Q2 genau dann, wenn es Prozesse Q ′1,Q

′2 gibt mit

Q1 ∼ Q ′1RQ′2 ∼ Q2.




Als Diagramm laßt sich diese Beweistechnik folgendermaßendarstellen:

P1

a��

R P2

Q1

(. . . und dann noch der dazu symmetrische Fall.)





P1

a��

R P2

Q1 Q2






P1

a��

R P2

a��

Q1 ∼ Q ′1 R Q ′2 ∼ Q2





Man muss nun noch zeigen, dass diese Modulo-Bisimulationtatsachlich sinnvoll definiert ist.

Bisimulation modulo starke Bisimularitat (Satz)

Sei R eine Bisimulation modulo starke Bisimularitat. Dann gilt:R ⊆∼. Insbesondere gilt fur jedes Paar von Prozessen (P,Q) ∈ R,dass P ∼ Q.

Bemerkung: Dieser Satz ist auch dann noch korrekt, wenn in derDefinition der Bisimulation modulo starke Bisimularitat dieRelation ∼ R ∼ durch (∼ R ∼)∪ ∼ ersetzt wird. Das heißt, esreicht auch aus, ein Prozesspaar zu finden, das bereits als bisimularbekannt ist.




Auch schwache Bisimulation modulo starke Bisimulation ist einekorrekte Beweistechnik.

Schwache Bisimulation modulo starke Bisimularitat (Definition)

Eine Relation R heißt schwache Bisimulation modulo starkeBisimularitat, falls fur jedes Paar (P1,P2) ∈ R und fur jede Aktiona ∈ Act gilt:

fur jedes P ′1 mit P1a→ P ′1 gibt es ein P ′2 mit P2

a⇒ P ′2 und(P ′1,P

′2) ∈∼ R ∼.

fur jedes P ′2 mit P2a→ P ′2 gibt es ein P ′1 mit P1

a⇒ P ′1 und(P ′1,P

′2) ∈∼ R ∼.

Zur Erinnerung: a = a, falls a ∈ Act\{τ}, und τ = ε.




Schwache Bisimulation modulo starke Bisimularitat (Satz)

Sei R eine schwache Bisimulation modulo starke Bisimularitat.Dann gilt: R ⊆≈. Insbesondere gilt fur jedes Paar von Prozessen(P,Q) ∈ R, dass P ≈ Q.

(Ohne Beweis)




Eine falsche Beweistechnik ist jedoch schwache Bisimulationmodulo schwache Bisimularitat.

Beispiel: P = τ.0, Q = τ.a.0 (diese Prozesse sind bestimmt nichtschwach bisimular!)

Wir betrachten die Relation R = {(τ.0, τ.a.0)} und zeigen, dass sieeine schwache Bisimulation modulo schwache Bisimularitat ist.

Daraus folgt, dass diese Beweistechnik falsch ist.




1. Fall:

τ.0

τ��

R τ.a.0

0

2. Fall:

τ.0 R τ.a.0

τ��

a.0




1. Fall:

τ.0

τ��

R τ.a.0

ε��

0 a.0

2. Fall:

τ.0 R τ.a.0

τ��

a.0




1. Fall:

τ.0

τ��

R τ.a.0

ε��

0 ≈ τ.0 R τ.a.0 ≈ a.0

2. Fall:

τ.0 R τ.a.0

τ��

a.0




1. Fall:

τ.0

τ��

R τ.a.0

ε��

0 ≈ τ.0 R τ.a.0 ≈ a.0

2. Fall:

τ.0 R τ.a.0

τ��

a.0




1. Fall:

τ.0

τ��

R τ.a.0

ε��

0 ≈ τ.0 R τ.a.0 ≈ a.0

2. Fall:

τ.0

ε��

R τ.a.0

τ��

0 a.0




1. Fall:

τ.0

τ��

R τ.a.0

ε��

0 ≈ τ.0 R τ.a.0 ≈ a.0

2. Fall:

τ.0

ε��

R τ.a.0

τ��

0 ≈ τ.0 R τ.a.0 ≈ a.0



Unentscheidbarkeit der Bisimularitat

Unentscheidbarkeit der Bisimularitat (Satz)

Es ist unentscheidbar, ob zwei gegebene Prozesse P,Q (stark oderschwach) bisimular sind.

Intuition:

Prozesse konnen unendlich große Transitionssysteme haben,daher reicht es nicht aus, einfach alle moglichenBisimulationen “durchzuprobieren”.

CCS ist Turing-machtig, d.h., es kann Turing-Maschinensimulieren. Daher ist die Unentscheidbarkeit eine indirekteKonsequenz aus dem Satz von Rice (= es ist unentscheidbar,ob die von einer Turingmaschine berechnete Funktion einebestimmte nicht-triviale Eigenschaft hat).



Beobachtungskongruenz

Man kann zeigen, dass starke Bisimularitat unter denCCS-Operatoren, erhalten bleibt, d.h., eine Kongruenzrelation ist.

Satz (∼ ist eine Kongruenzrelation)

Es gelte P1 ∼ P2. Dann gilt auch:

1 a.P1 ∼ a.P2

2 P1 + Q ∼ P2 + Q

3 P1 | Q ∼ P2 | Q4 P1\L ∼ P2\L5 P1[f ] ∼ P2[f ]




Auch schwache Bisimularitat ist eine Kongruenz bezuglich dermeisten CCS-Operatoren (jedoch nicht bezuglichnicht-deterministischer Auswahl!).

Satz (≈ ist eine Kongruenzrelation)

Es gelte P1 ≈ P2. Dann gilt auch:

1 a.P1 ≈ a.P2

2 P1 | Q ≈ P2 | Q3 P1\L ≈ P2\L4 P1[f ] ≈ P2[f ]

(Der Beweis ist mehr oder weniger analog zum Fall der starkenBisimularitat.)




Schwache Bisimularitat wird jedoch nicht unternicht-deterministischer Auswahl erhalten.

Beispiel: Es gilt a.0 ≈ τ.a.0, jedoch

a.0 + b.0 6≈ τ.a.0 + b.0.

a.0 + b.0a

zz

b

$$0 0

τ.a.0 + b.0τ

yy

b

%%a.0

a��

0

0




Problem: Es ist moglich, dass durch den Austausch vonSubsystemen durch schwach bisimulare Subsysteme (= Prozesse)das Verhalten des Systems verandert wird.

Idee: die schwache Bisimularitat wird so weit verfeinert, dass sieeine Kongruenzrelation ist, d.h., unter den CCS-Operatorenerhalten bleibt.

Wiederholung: schwache Ubergange

Pτ⇒ Q gdw. P

ε⇒ Q gdw. P(τ→)∗Q

Pa⇒ Q gdw. P

a⇒ Q gdw. P(τ→)∗ a→ (

τ→)∗Q fur a 6= τ

Wir definieren nun eine Folge von mindestens einem τ -Ubergang:

Pτ⇒ Q gdw. P(

τ→)∗ τ→ (τ→)∗Q




Beobachtungskongruenz (Definition)

Zwei Prozesse P,Q heißen beobachtungskongruent (in Zeichen:P ≈c Q, engl.: observationally congruent), falls fur jedes a ∈ Act(auch fur a = τ) gilt:

Fur jedes P ′ mit Pa→ P ′ gibt es ein Q ′ mit Q

a⇒ Q ′ undP ′ ≈ Q ′.

Fur jedes Q ′ mit Qa→ Q ′ gibt es ein P ′ mit P

a⇒ P ′ undP ′ ≈ Q ′.

Bemerkung: Nur im ersten Schritt muss ein τ des einen Prozessesdurch mindestens ein τ des anderen Prozesses beantwortet werden.Danach wird schwache Bisimularitat (P ′ ≈ Q ′) gefordert.




Beobachtungskongruenz (Satz)

Die Relation ≈c ist die großte Aquivalenzrelation, die

in der schwachen Bisimularitat ≈ enthalten ist und

kongruent bezuglich aller CCS-Operatoren ist.

(Ohne Beweis)




Damit gilt folgendes fur die Beobachtungskongruenz ≈c :

≈c ist eine Kongruenzrelation (Satz)

Es gelte P1 ≈c P2. Dann gilt auch:

1 a.P1 ≈c a.P2

2 P1 + Q ≈c P2 + Q

3 P1 | Q ≈c P2 | Q4 P1\L ≈c P2\L5 P1[f ] ≈c P2[f ]



Concurrency Workbench


Werkzeug zur Simulation und Verifikation von CCS-Prozessen.

Zwei Versionen:

Edinburgh Concurrency Workbench(http://homepages.inf.ed.ac.uk/perdita/cwb/)Entwickelt von Perdita StevensConcurrency Workbench of the New Century(http://www.cs.sunysb.edu/~cwb/)

Hinweise zur Syntax: ein Prafix a wird durch ′a dargestellt.




Concurrency Workbench – Alternating Bit Protocol

** Agents **

agent ABPlossy = (R0 | Mlossy | S0)\Internals;

agent ABPsafe = (R0 | Msafe | S0)\Internals;

agent Mlossy = MlossySR | MlossyRS;

agent MlossyRS = sack0.’rack0.MlossyRS +

sack0.MlossyRS + sack1.’rack1.MlossyRS +

sack1.MlossyRS;

...

agent Spec = accept.’deliver.Spec;

** Action sets **

set Internals = {r0,r1,rack0,rack1,s0,s1,sack0,sack1};




Concurrency Workbench – Simulation

Command: sim ABPsafe;

Simulated agent: ABPsafe

Transitions:

1: --- tau ---> (R0 | (MsafeSR | ’rack1.MsafeRS)

| S0)\Internals

2: --- accept ---> (R0 | Msafe | S0’)\Internals




Concurrency Workbench – Verifikation

Starke Bisimularitat uberprufen:

Command: strongeq(ABPlossy,Spec);

false

Schwache Bisimularitat uberprufen:

Command: eq(ABPlossy,Spec);

true




Concurrency Workbench – Verifikation

Beobachtungskongruenz uberprufen:

Command: cong(ABPlossy,Spec);

false

Beobachtungskongruenz mit anderer Spezifikation:

Command: agent Spec’ = tau.Spec;

Command: eq(ABPlossy,Spec’);

true



CCS und Wechselseitiger Ausschluss

Wir modellieren den Algorithmus von Lamport zum wechselseitigenAusschluss in CCS.

Dabei betrachten wir: zwei Prozesse P1, P2 mit unterschiedlichemProgrammcode, die beide den kritischen Bereich betreten wollen,und zwei Boolesche Variable f1, f2 (initialisiert mit false).




Prozess P1

while true do

1: f1 := true;

2: while (f2 = true?) do

skip

od;

3: [Betrete krit. Bereich];

4: [Verlasse krit. Bereich];

5: f1 := false

od;

skip: Null-Operation (hat keine Auswirkungen)




Prozess P2

while true do

1: f2 := true;

2: if (f1 = true?) then do

begin

3: f2 := false;

4: while (f1 = true?) do skip od;

goto 1

end;

5: [Betrete krit. Bereich];

6: [Verlasse krit. Bereich];

7: f2 := false

od;




Modellierung der beiden Prozesse und der beiden Variablen alsCCS-Prozesse.

Aktionen fur Schreiben und Lesen der Variablen:

f1wt – Variable f1 mit true belegen

f1wf – Variable f1 mit false belegen

f1rt – Uberprufen, ob Variable f1 mit true belegt ist

f1rf – Uberprufen, ob Variable f1 mit false belegt ist

(Analog fur f2).

Betreten und Verlassen des kritischen Bereichs:

bkb1 – Prozess 1 betritt kritischen Bereich

vkb1 – Prozess 1 verlasst kritischen Bereich

(Analog fur Prozess 2).




Prozesse in der Syntax der Concurrency Workbench:

* Variable f1

agent F1t = ’f1rt.F1t + f1wt.F1t + f1wf.F1f

agent F1f = ’f1rf.F1f + f1wt.F1t + f1wf.F1f

* Variable f2

agent F2t = ’f2rt.F2t + f2wt.F2t + f2wf.F2f

agent F2f = ’f2rf.F2f + f2wt.F2t + f2wf.F2f




Prozesse in der Syntax der Concurrency Workbench:

* Prozess P1

agent P1 = ’f1wt.f2rf.bkb1.vkb1.’f1wf.P1

* Prozess P2

agent P2 = ’f2wt.(f1rt.’f2wf.f1rf.P2 +

f1rf.bkb2.vkb2.’f2wf.P2)

* Mutex-Algorithmus

agent Mutex = (F1f | F2f | P1 | P2)\{f1rf,f1wf,f1rt,

f1wt,f2rf,f2wf,

f2rt,f2wt}




Fragen:

Hat der Prozess Deadlocks?

Wie sieht das Transitionssystem von Mutex aus? Andersausgedruckt: minimiere Mutex bezuglich schwacherBisimularitat.

Was ist eine geeignete Spezifikation und wie kann man zeigen,dass Mutex diese Spezifikation erfullt?




Das System enthalt keine Deadlocks:

Command: deadlocks(Mutex);

None.

Mogliche Spezifikation:

agent Spec = bkb1.vkb1.Spec + bkb2.vkb2.Spec

Das System und die Spezifikation sind nicht schwach bisimular,aber die Sprache des Systems ist in der Sprache der Spezifikationenthalten:

Command: eq(Mutex,Spec);

false

Command: maypre(Mutex,Spec);

true



Kontexte und Up-to-Context-Techniken

Kontext (Definition)

Ein Kontext C [ ] ist ein Prozess, der an genau einer Stelle statteines Sub-Prozesses das Zeichen (= Unterstrich) enthalt. DiesesVorkommen von wird auch als Platzhalter bezeichnet.

Mit C [P] bezeichnet man den Kontext C [ ], bei dem das Zeichendurch P ersetzt wurde.

Beispiele:

a.P + + b.Q

(a.P | )\{a}[f ]




Kongruenzrelationen (Korollar)

Seien P1,P2 CCS-Prozesse und C [ ] ein beliebiger Kontext. Danngilt:

Aus P1 ∼ P2 folgt immer auch C [P1] ∼ C [P2].

Aus P1 ≈c P2 folgt immer auch C [P1] ≈c C [P2].

Beweis: dieses Korollar folgt direkt aus den obigen Satzen, dieaussagen, dass ∼ bzw. ≈c Kongruenzrelationen sind.




Bisimulation modulo Kontext (Definition)

Eine Relation R heißt (starke) Bisimulation modulo Kontext, fallsfur jedes Paar (P1,P2) ∈ R und fur jede Aktion a ∈ Act gilt:


a→ Q2 und(Q1,Q2) ∈ R.


a→ Q1 und(Q1,Q2) ∈ R.

Dabei steht R fur die Relation

R = {(C [P1],C [P2]) | (P1,P2) ∈ R,C [ ] ist beliebiger Kontext}.




Bisimulation modulo Kontext (Satz)

Sei R eine Bisimulation modulo Kontext. Dann gilt: R ⊆∼.Insbesondere gilt fur jedes Paar von Prozessen (P,Q) ∈ R, dassP ∼ Q.

Beweis (Skizze): Man zeigt direkt, dass die Relation R aus dervorherigen Definition eine Bisimulation ist. Dazu benotigt manunter anderem die Tatsache, dass Bisimularitat eine Kongruenz ist.




Das bedeutet, es reicht bei Bisimulationsbeweisen aus, zuuberprufen, dass die Nachfolgerprozesse in der Relation R sind,moglicherweise mit zusatzlichem (aber identischem) Kontext.(Diese Technik ist auch mit anderen Modulo-Technikenkombinierbar.)

Beispiel:

P mit P := a.(P | P)

Q mit Q := a.(Q | P)

Zu zeigen: R = {(P,Q)} ist eine Bisimulation modulo Kontext.



Axiomatisierung

Wir suchen nun weitere Gesetze bzw. Axiome furVerhaltensaquivalenzen, sowohl fur starke Bisimularitat, als auchfur Beobachtungskongruenz.

Bereits bekannt:

P ≡ Q ⇒ P ∼ Q.

P ∼ Q ⇒ P ≈c Q.

Sowohl starke Bisimularitat als auch Beobachtungskongruenzsind Kongruenzrelationen.

Eine Axiomatisierung ist nur dann sinnvoll, wenn es sich um eineKongruenzrelation handelt, ansonsten konnen Teilprozesse nichtdurch verhaltensaquivalente Teilprozesse ersetzt werden.



Axiomatisierung

Wir betrachten zunachst das sogenannte Expansionsgesetz.

Expansionsgesetz (Satz)

P︷︸︸︷(∑

i∈I

ai .Pi

)|

Q︷︸︸︷∑

j∈J

bj .Qj

∼∑

i∈I

ai .(Pi | Q) +∑

j∈J

bj .(P | Qj ) +∑

ai =bj

τ.(Pi | Qj ).

Notation: Sei I = {i1, . . . , in} eine Indexmenge. Dann gilt:

∑

i∈I

Pi = Pi1 + · · ·+ Pin .



Axiomatisierung

Beispiel fur die Anwendung des Expansionsgesetzes:

P︷︸︸︷(a.P1 + b.P2) |

Q︷︸︸︷(a.Q1 + c .Q2)

∼ a.(P1 | Q) + b.(P2 | Q) +

a.(P | Q1) + c .(P | Q2) +

τ.(P1 | Q1)



Axiomatisierung

Verschattungsgesetze

(Res1) 0\L ∼ 0

(Res2) (P\L)\L′ ∼ P\(L ∪ L′)

(Res3) (a.P)\L ∼{

a.(P\L) falls a, a 6∈ L0 sonst

(Res4) (P + Q)\L ∼ P\L + Q\L



Axiomatisierung

Umbenennungsgesetze

(Ren1) 0[f ] ∼ 0

(Ren2) (P[f ])[f ′] ∼ P[f ′ ◦ f ]

(Ren3) (a.P)[f ] ∼ f (a).(P[f ])

(Ren4) (P + Q)[f ] ∼ P[f ] + Q[f ]

Verschattungs-Umbenennungs-Gesetz

(ResRen) (P[f ])\L ∼ (P\f −1(L))[f ]



Axiomatisierung

Folgende Gesetze gelten fur die Beobachtungskongruenz:

τ -Gesetze

(Tau1) a.P ≈c a.τ.P

(Tau2) τ.P ≈c τ.P + P

(Tau3) a.(P + τ.Q) ≈c a.(P + τ.Q) + a.Q



Axiomatisierung

Alle obigen Gesetze (auch Axiome genannt) sind korrekt fur diestarke Bisimularitat bzw. Beobachtungskongruenz. Man kannjedoch auch folgende Frage stellen:

Gegeben seien zwei Prozesse P,Q mit P ∼ Q (bzw. P ≈c Q).Kann man die Verhaltensaquivalenz von P und Q nur durchAnwendung der Gesetze nachweisen?

Eine Axiomatisierung, die diese Eigenschaft erfullt, heißtvollstandig.



Axiomatisierung

Fur CCS im allgemeinen ist die Axiomatisierung nicht vollstandig.

Es gelten jedoch Vollstandigkeitsresultate fur eine Teilmenge vonCCS:

CCSfin (Definition)

Sei CCSfin die Menge aller CCS-Prozesse, die keine Konstantenenthalten.

Das heißt insbesondere, dass keine Rekursion moglich ist und jederProzess in CCSfin nach endlich vielen Schritten terminiert.



Axiomatisierung

Vollstandigkeit fur ∼Seien P,Q zwei Prozesse in CCSfin mit P ∼ Q. Dann kann diestarke Bisimularitat von P und Q unter Verwendung folgenderGesetze nachgewiesen werden:

Gesetze fur strukturelle Kongruenz Gesetze ,

Expansionsgesetz,

Gesetze (Res1), (Res3), (Res4), (Ren1), (Ren3), (Ren4)und

der Tatsache, dass ∼ eine Kongruenzrelation ist.



Axiomatisierung

Beweisidee:

Uberfuhre zunachst beide Prozesse P,Q in ihre Normalformdurch

Entfernen der parallelen Komposition (Expansionsgesetz)Entfernen der Verschattung und Umbenennung(Verschattung und Umbenennung mit Hilfe derentsprechenden Gesetze ganz nach innen schieben)

Die so entstehenden Prozesse enthalten nur noch 0, Summeund Prafix.

Zeige, dass die Bisimularitat von Prozessen in Normalformdurch die Anwendung der Gesetze fur die strukturelleKongruenz nachgewiesen werden kann.



Axiomatisierung

Beispiel: Zeigen Sie – nur unter Anwendung der Gesetze – diestarke Bisimularitat folgender Prozesse:

P = ((a.0 + b.0) | (a.0 + c .0))\{a}Q = τ.0 + (a.0 | b.0)[a/c] + b.c .0



Axiomatisierung

Vollstandigkeit fur ≈c

Seien P,Q zwei Prozesse in CCSfin mit P ≈c Q. Dann kann dieBeobachtungskongruenz von P und Q unter Verwendung folgenderGesetze nachgewiesen werden:

Gesetze fur strukturelle Kongruenz Gesetze ,

Expansionsgesetz,

Gesetze (Res1), (Res3), (Res4), (Ren1), (Ren3), (Ren4),

τ -Gesetze und

der Tatsache, dass ≈c eine Kongruenzrelation ist.



Axiomatisierung

Bedeutung der Axiomatisierung:

“Rechnen” mit nebenlaufigen Systemen

Analogie zu Ingenieurwissenschaften, wo die Stabilitat vonBauwerken mit Hilfe von Differentialgleichungen berechnetwird

Ziel: Verhaltensaquivalenz eines Prozesses mit der Spezifikationbeweisen, indem beide entsprechend umgeformt werden

Da die Axiomatisierung nicht notwendigerweise vollstandig ist, istdieses Ziel nicht immer zu erreichen.


Modellierung nebenl au ger Systeme Mir besch aftigen uns ... fileOrganisatorischesEinf uhrung...

Documents

Transcript of Modellierung nebenl au ger Systeme Mir besch aftigen uns ... fileOrganisatorischesEinf uhrung...