Seite 1 von 1

P sat ANF in CSP

Verfasst: 4. Mär 2009 11:43
von tzeenie
Hallo,

eine Frage zur letzten Übung: Wie würde ich formal beweisen, dass ein in CSP modelliertes System eine Anforderung erfüllt? Wir haben in der Übung ja lediglich durch Widerspruch gezeigt, dass ein Modell eine Anforderung nicht erfüllt, was ja mittels Gegenbeispiel verhältnismäßig einfach ist. Aber wie würde ich formal beweisen, dass eine Eigenschaft gilt?

Um es nicht ganz so theoretisch zu belassen, ein kleines (zugegebenermaßen blödes) Beispiel:
Angenommen wir modellieren eine taktgesteuerte Ampel, etwa
\(clock = \mu C\bullet(tick \rightarrow C)\)
\(ampel_{0} = gelb \rightarrow gruen \rightarrow ampel_{1}\)
\(ampel_{1} = tick \rightarrow tick \rightarrow tick \rightarrow tick \rightarrow gelb \rightarrow ampel_{2}\)
\(ampel_{2} = tick \rightarrow tick \rightarrow rot \rightarrow ampel_{4}\)
\(ampel_{3} = tick \rightarrow tick \rightarrow gruen \rightarrow ampel_{1}\)
\(ampel_{4} = tick \rightarrow tick \rightarrow tick \rightarrow tick \rightarrow gelb \rightarrow ampel_{3}\)

Und die Schaltung etwa so:
\(schaltung = ampel_{0} || clock\)

Nun noch zwei Verkehrsteilnehmer :) :
\(fussgaenger = \mu F\bullet((rot \rightarrow geht \rightarrow F) \sqcap (gelb \rightarrow steht \rightarrow F))\)
\(auto = \mu A\bullet((gruen \rightarrow faehrt \rightarrow A) \sqcap (gelb \rightarrow haelt \rightarrow A))\)
(Soll modellieren: Der Fußgänger überquert die Straße, wenn die Ampel auf rot steht; das Auto fährt, wenn die Ampel auf grün steht; beide halten, sobald die Ampel auf gelb schaltet.)

Gesamtes Modell nun:
\(kreuzung = auto || fussgaenger || schaltung\)

Bear with me - ich weiß dass es nicht das beste Beispiel der Welt ist :lol: aber hoffentlich ist wenigstens die Modellierung soweit korrekt.

Jetzt sei unsere Anforderung, dass ein Auto niemals gleichzeitig mit einem Fußgänger in Bewegung ist, formal:
\(GEFAHRLOS(tr) = BEFORE_{HAELT, GEHT}(tr) \wedge BEFORE_{STEHT, FAEHRT}(tr)\)
wobei
\(HAELT = \{haelt\}, STEHT = \{steht\}, GEHT = \{geht\}, FAEHRT = \{faehrt\}\)

Ich denke \(kreuzung\hspace{0.5em} sat\hspace{0.5em} GEFAHRLOS\) gilt, aber wie würde ich das formal zeigen?! Ein Ansatz würde mir schon helfen, ich habs durch "Ausrechnen" von \(traces(kreuzung)\) probiert, hab dann bei den ganzen Projektionen in die versch. Alphabete aber abgebrochen. :roll:

Gruß!
Jens
~~
p.s.: Endlich weiß ich warum mein Fahrlehrer immer meinte, dass ich durch die Prüfung fall wenn ich bei gelb losfahre. Hätte er ja mal formal beweisen können warum, tsk. :mrgreen: