traces((P || Q)) - Semantik unklar

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

traces((P || Q)) - Semantik unklar

Beitrag von barracuda317 »

Hallo,

auch bei P || Q habe ich noch ein Verständnisproblem.

Es handelt sich hier bekanntlich um nebenläufige Systeme, die bei gemeinsamen Ereignissen synchronisert werden.

Die Definition besagt dabei:

Bild

Nun schaue ich mir die Lösung der 13 Übung an, konkret dabei Aufgabe 2.

Sei nun also P = Board und Q = Rule

Betrachtet man das Gleichungssystem von Board, so ist (right, left) in traces(Board).

Nun prüfen wir, ob nach der Definition \((right, left) \in traces(Board||Rule)\)

Es muss also gelten:

\((right,left)\) HAKEN \(\alpha Board \in traces (Board)\) und \((right, left)\) HAKEN \(\alpha Rule \in traces (Rule)\)

Wir prüfen:

\((right,left)\) HAKEN \(\alpha Board \in traces (Board)\)

Es ist \((right,left)\) Haken \(\{right,left, up, down\} = (right, left ) \in traces (board)\)

Weiter prüfen wir:

\((right,left)\) HAKEN \(\alpha Rule \in traces (Rule)\)

Es ist \((right,left)\) Haken \(\{right, up\} = (right) \in traces (Rule)\)

Damit wäre \((right,left) \in traces ((Board || Rule))\)

Im Lösungsvorschlag ist das jedoch nicht der Fall.

In der Sprechstunde wurde gesagt, dass in traces((P||Q)) nur die synchronisierten (also in beiden Ereignismengen enthaltenen) Ereignisse berücksichtigt werden. Also quasi \(tr \in traces (P) \wedge tr \in traces(Q)\)

Das würde aber bedeuten, dass ich entweder die Definition missverstanden habe, oder ein anderer Fehler in meiner Interpretation vorliegt.

Nun also der Frage: Wo ist der Fehler?

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: traces((P || Q)) - Semantik unklar

Beitrag von errt »

Das Alphabet von Rule ist hier auch {right, left, up, down}.

Daher ist (right,left) Haken {right, left, up, down} = (right, left) nicht Element traces(Rule)

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Re: traces((P || Q)) - Semantik unklar

Beitrag von barracuda317 »

Kannst du mir kurz erläutern warum das Alphabet von Rule hier auch \(\{right, left, up, down\}\) ist? In den Gleichungen für Rule kommen doch left und down garnicht vor

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: traces((P || Q)) - Semantik unklar

Beitrag von errt »

Ist halt so definiert. Oben im Text steht E = {right, left, up, down}, unten steht Rule =_E ...

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Re: traces((P || Q)) - Semantik unklar

Beitrag von barracuda317 »

Tatsächlich, danke. Da habe ich wohl wieder die Aufgabenstellung nicht genau gelesen.

Wäre meine Begründung von oben denn richtig gewesen, wenn wir \(\{right, up \} = \alpha Rule\) angenommen hätten. In diesem Fall wäre nach meiner Argumentation \((right,left) \in Tr\) gewesen.

Antworten

Zurück zu „Archiv“