FB18 - Das Forum für Informatik

fb18.de / Bachelorstudieng / PM Formale Informatik

Prozessalgebra: Widerspruchsbeweis

Prozessalgebra: Widerspruchsbeweis 2007-12-16 15:55
NaZo
Ich habe Probleme damit einen Widerspruchsbeweis in BPA, PAP, ACP etc. zu führen. Woher weiß ich, dass aus [latex]s \neq t [/latex] folgt, dass [latex]s \stackrel{t}{\rightarrow} \surd[/latex] falsch ist? Natürlich ist das falsch, und natürlich gibt es auch keine Regel, mit der ich das ableiten kann, aber wie kann man beweisen, dass es falsch ist?

RE: Prozessalgebra: Widerspruchsbeweis 2007-12-16 21:47
Anonymer User
Hmmm… mir ist nicht ganz klar, was du erreichen willst. Wenn du so etwas wie s != t hast, dann
sind mit s und t ja Prozessterme gemeint. Das t über deinem Pfeil drückt aber etwas anderes aus.
(Eine Folge von Aktionen mit der man von s ausgehend zur Termination kommt.)

Vielleicht meinst du den Zusammenhang zwischen der Gleichheit im Kalkül und der Bisimulation?
Für den BPA-Kalkül wurde ja relativ zu Anfang des Kapitels über Prozessalgebra bewiesen, dass
s = t genau dann gilt, wenn s und t bisimilar sind.

Kannst du deine Frage noch mal anders formulieren?

Frank :)

RE: Prozessalgebra: Widerspruchsbeweis 2007-12-17 11:28
georg
Ich habe Probleme damit einen Widerspruchsbeweis in BPA, PAP, ACP etc. zu führen. Woher weiß ich, dass aus [latex]s \neq t [/latex] folgt, dass [latex]s \stackrel{t}{\rightarrow} \surd[/latex] falsch ist? Natürlich ist das falsch, und natürlich gibt es auch keine Regel, mit der ich das ableiten kann, aber wie kann man beweisen, dass es falsch ist?

Abgesehen davon (wie Frank schon gesagt hat), dass [latex]s\stackrel{t}{\to}\surd[/latex] nur
dann stimmen kann, wenn t atomar ist, ist die Behauptung nicht
richtig. Es gilt nämlich [latex]a+b\ne a[/latex], aber trotzdem [latex]a+b\stackrel{a}{\to}\surd[/latex].