Zeitigkeit bei BEFORE unklar

[barracuda317]

Hallo,

beim Wiederholen hakt es gerade bei einer Definition. Ich war damit auch schon in der Sprechstunde aber auch dort konnte das Problem nicht geklärt werden.



Eingeführt wurde die Definition in Modul 13 Folie 18 mit der Eigenschaft: "Wenn ein Ereignis aus G geschieht, dann muss zuvor ein Ereignis aus F geschehen.

Informell interpretiere ich die Definition als: Sei tr eine Ereignisspur des Prozess P. Wenn ein Ereignis aus G in tr enthalten ist, dann ist auch ein Ereignis aus F in tr enthalten.

Der Unterschied dabei ist schlicht, die Zeitigkeit. Ich kann aus der Definition nicht herauslesen, wann die Ereignisse passieren, sondern nur ob die Ereignisse passieren.

Damit verfehlt aber das Prädikat aber seine Bedeutung.

Daher meine Frage:

Übersehe ich in der Definition etwas, woraus diese Eigenschaft abgeleitet ist, oder liegt hier in der Tat eine Ungenauigkeit vor?

Meine Idee wie das zu beheben wäre, würde wie folgt aussehen:

\(BEFORE_{F,G}(tr) = \exists tr'. tr' \leq tr \wedge tr'\) HAKEN \(G = () \wedge (tr\) HAKEN \(G \neq () \Rightarrow tr'\) HAKEN \(F \neq ())\)

[errt]

Für die einzelne Spur tr stimmt das, aber P sat S ist so definiert, dass S für alle Spuren aus P gelten muss. Nun sind diese unter Präfixbildung abgeschlossen, das heißt, dass S auch unter Präfixbildung abgeschlossen sein muss - und das ist nur der Fall, wenn tatsächlich immer zuerst ein Ereignis aus F eintritt - sonst könnte man ja ein Präfix bilden, in dem das Ereignis aus F noch nicht eingetreten ist, das aus G aber schon und dieses Präfix würde S nicht erfüllen, womit P sat S nicht mehr gelten würde.

[barracuda317]

Vielen Dank. Diese Definition habe ich nicht beachtet, nun leuchtet es mir ein.

Wenn wir also eine Spur haben, in der die Ereignisse aus G und F enthalten sind, wissen wir zunächst nicht, wo sie stehen (also ob das Ereignis aus F tatsächlich vor dem Ereignis aus G geschieht). Da das Prädikat auch für alle Präfixe erfüllt sein muss, prüfen wir für eine Spur, in der das Ereignis aus G das letzte Ereignis ist, was geschieht.

Wenn auch hier die Implikation gilt, wissen wir, dass das Ereignis aus F nicht nach dem Ereignis aus G geschieht.

Ich habe nun noch ein wenig mit der Definition rumgespielt, und eine Sache finde ich noch unklar. Gehen wir davon aus, dass dieses letzte Ereignis aus G, welches wir betrachten auch in F enthalten ist. Es ist ja scheinbar nicht verboten, dass F und G nicht disjunkt sind. Weitere Ereignisse aus F oder G sind nicht in der Spur enthalten.

Für diese Spur tr, mit dem letzten Ereignis \(e \in G \wedge e \in F\) ist die Implikation erfüllt, für alle Präfixe mit kleinerer Länge ist die Implikation auch erfüllt, da \(tr\) Haken \(G = ()\)

Wir sagen also, dass das P sat S gilt.

Jedoch gilt nicht, dass das Ereignis aus F VOR dem Ereignis aus G geschehen ist.

Nun die Frage: Habe ich in meinen Überlegungen erneut etwas vergessen, gilt BEFORE auch bei gleichzeitigem Eintreten oder interessiert uns das garnicht?