P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

cdn
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 13. Dez 2008 13:54

P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

Beitrag von cdn »

Rein nach der Definition von rek. Gleichungssystemem auf Folie 23 des Foliensatzes 12 sind ja nur der bis dahin eingeführte Teilbereich der Ausdrücke in den rechten Seiten von Gleichungen erlaubt. Gilt das auch weiterhin so oder kann ich auch die danach eingeführten Erweiterungen wie Fixpunktnotation, Ausdrücke der Form P || Q etc in Gleichungssystemen nutzen?

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

Beitrag von oren78 »

fragen wir doch mal so rum, warum soll es nicht gehen?
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

cdn
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 13. Dez 2008 13:54

Re: P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

Beitrag von cdn »

weil es in der Definition für rekursive Gleichungssysteme erstmal nicht vorgesehen ist?
Schließlich wird dort extra nochmal \(P ::= STOP_E | SKIP_E | (x\rightarrow P) | (P \sqcap P) | Id\) aufgeführt und die Menge der Gleichungen soll die Form \(\{ id =_E P | id \in ID \}\) haben. Jetzt verbleibt ein Interpretationsspielraum, ob die nachfolgenden Folien diese für hier gültige Definition von P für die rechten Seiten von Gleichungen erweitern oder ob Gleichungssysteme auf genau diese Ausdrücke eingeschränkt bleiben. Denkbar sind erstmal beide Interpretationen, da Erweiterungen evtl. die Lösbarkeit beeinflussen können.

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

Beitrag von oren78 »

cdn hat geschrieben:weil es in der Definition für rekursive Gleichungssysteme erstmal nicht vorgesehen ist?
Schließlich wird dort extra nochmal \(P ::= STOP_E | SKIP_E | (x\rightarrow P) | (P \sqcap P) | Id\) aufgeführt und die Menge der Gleichungen soll die Form \(\{ id =_E P | id \in ID \}\) haben. Jetzt verbleibt ein Interpretationsspielraum, ob die nachfolgenden Folien diese für hier gültige Definition von P für die rechten Seiten von Gleichungen erweitern oder ob Gleichungssysteme auf genau diese Ausdrücke eingeschränkt bleiben. Denkbar sind erstmal beide Interpretationen, da Erweiterungen evtl. die Lösbarkeit beeinflussen können.
in hoare's buch ist das selbe ja auch enthalten: http://www.usingcsp.com/cspbook.pdf

du hast ja: \(\mu X:E.F(X)\) das bedeutet: E = Ereignisalphabeth, X = der spez. prozes und F(X) der dazugehörende CSP Ausdruck,
da P || Q bzw. P ||| Q gültige CSP ausdrücke darstellen, ist F(X) erfüllt und somit können diese enthalten sein..
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

schuster
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 5. Okt 2007 15:43

Re: P || Q, P;Q und P|||Q in Gleichungssystemen erlaubt?

Beitrag von schuster »

cdn hat geschrieben:Rein nach der Definition von rek. Gleichungssystemem auf Folie 23 des Foliensatzes 12 sind ja nur der bis dahin eingeführte Teilbereich der Ausdrücke in den rechten Seiten von Gleichungen erlaubt. Gilt das auch weiterhin so oder kann ich auch die danach eingeführten Erweiterungen wie Fixpunktnotation, Ausdrücke der Form P || Q etc in Gleichungssystemen nutzen?
Sie dürfen die Operatoren, die danach eingeführt wurden auch in Gleichungssystemen verwenden.

Beste Grüße,

Dieter Schuster

Antworten

Zurück zu „Archiv“