[MaLo] Blatt 9

[jim]

also ich würd sagen nur {1,5}

Die Formel bedeutet doch:
alle Nachfolger haben einen Pfad der in 2 oder 3 Schritten zu P führt.

[Daniel]

ja, habe ich genauso, also nur {1,5}

Am einfachsten ist es wenn du das ganze von innen nach außen machst. ALso zuerst suchst du dir alle Knoten an denen P gilt, und die, von denen man in einem Schritt nach P kommen kann (2,1,5,4). Dann suchst du dir alle Knoten, von denen man in einem Schritt zu deinem der 4 Knoten kommen kann (das ist der nächste <>). Dann machst du das ganze nochmal mit der neuen Menge.

Zu guter letzt den [] bearbeiten. Dazu gehst du einfach alle Knoten durch und schaust, komme ich mit JEDER Kante von dem Knoten in die Menge <><>(Pv<>P).

[fw]

An die Leute, die ATFS gehört haben: Das ganze erinnert doch irgendwie sehr stark an den Markierungsalgorithmus zur Minimierung von endlichen Automaten, oder kommt mir das nur so vor? Äquivalente Zustände und nicht-unterscheidbare Zustände und so...

[SpatzenArsch]

An die Leute, die ATFS gehört haben: Das ganze erinnert doch irgendwie sehr stark an den Markierungsalgorithmus zur Minimierung von endlichen Automaten, oder kommt mir das nur so vor? Äquivalente Zustände und nicht-unterscheidbare Zustände und so...

Jab da hab ich auch als erstes dran gedacht!

[nathan99]

:edit:

Sollen wir bei A2 (b) eine Formel Phi angeben, die für JEDES Knotenpaar (v, w) dass nicht bisimular ist, für v wahr ist und bei w falsch?

Oder für jedes nicht bs. Knotenpaar eine Formel?

[jim]

:edit:

Sollen wir bei A2 (b) eine Formel Phi angeben, die für JEDES Knotenpaar (v, w) dass nicht bisimular ist, für v wahr ist und bei w falsch?

Oder für jedes nicht bs. Knotenpaar eine Formel?

Ich denke da reicht es für jedes Paar eine Formel anzugeben und nicht eine Formel für alle Paare.

Die Formeln hat man ja automatisch wenn man den Algorithmus aus dem Tutorium verwendet.

Zu A1(c)(iii): Mir fällt da nur sowas ein:
<>P ^ <><>notP ^ <><><>P ^ <><><><>notP
Aber dann hab ich ja das Problem, dass ich 4 verschiedene Pfade haben kann auf denen die Teilbedinungen gelten.
Tipps?

[kb]

das kannst du einfach mit klammern lösen:

<>(P ^ <>(!P ^ ...
will ja nicht die ganze lösung hinschreiben, aber rest ist eigentlich klar denk ich

[tromba_marina]

das kannst du einfach mit klammern lösen:
<>(P ^ <>(!P ^ ...

Richtig, aber es ist nicht gefordert, dass in einem benachbarten Knoten P gilt, sondern nur, dass auf dem Weg abwechselnd P und !P gilt ... daran hast du aber wahrscheinlich auch schon gedacht :)

Und @fw: Das kann man wirklich genau so machen wie in ATFS. Statt einer "trennenden" Eingabe kommt dann in jedes Tabellenkästchen eine "trennende" Formel aus ML, bis keine neuen Kästchen mehr gefüllt werden können.

[kb]

hm. also wenn ich lese "auf dem Pfad gilt abwechselnd P und !P", dann versteh ich das so "es gilt P, am nächsten Knoten !P, am nächsten Knoten wieder P usw.".
Muss ich den Startknoten mit einbeziehen?
Und wenn man meine Formel unten weiterführt, sagt sie genau das aus, was in A1/c/iii steht. Dass es vlt. noch andere Formeln gibt, ist ja nicht ausgeschlossen.
Ich hab das Gefühl, ich verstehe nicht ganz, was du gemeint hast ^^ bitte nochmal erklären

[tromba_marina]

Ok ... ich meinte eigentlich nur, die erste Möglichkeit ist, dass in einem Nachfolgeknoten P gilt, in einem von dessen Nachfolgern !P etc. Aber die zweite Möglichkeit ist doch dann, dass im Nachfolger !P gilt, in dessen Nachfolger dann P etc., d.h. die Forderung "abwechselnd P und !P" sagt nichts darüber aus, womit man beginnt. Oder?

[heipei]

ich glaube das mit dem "wo man beginnt" ist in der modallogik ja eh das schöne weil es relativ ist

scherz beiseite, ist es nicht einfach P \Diamond \neg P \Diamond P .... usw. heisst doch nur dass es einen moeglichen pfad gibt auf dem das abwechselnd gilt, heisst ja nicht dass man nicht nach der ersten kante wo ganz anders hingehen kann. oder denk ich zu simpel?

[tromba_marina]

scherz beiseite, ist es nicht einfach P \Diamond \neg P \Diamond P .... usw. heisst doch nur dass es einen moeglichen pfad gibt auf dem das abwechselnd gilt, heisst ja nicht dass man nicht nach der ersten kante wo ganz anders hingehen kann. oder denk ich zu simpel?

Ja ... betrachte den Graphen 1 -> 2 -> 3 -> 4, mit P := {2, 4}. Dann gibt es einen Kantenzug der Länge vier von 1 nach 4, in dem abwechselnd P und !P gilt, aber keinen, der zu der Formel "P \and \diamond(!P \and \diamond(P \and ..." passt. Und in der Form von oben (ohne Klammern und Junktoren dazwischen) macht die ohnehin keinen Sinn.

[fw]

würde sagen es ist so zu verstehen, dass man mit P beginnt.. ansonsten macht man halt zwei formel.. eine die mit P beginnt, eine die mit !P beginnt und dann einfach die disjunktion

[kb]

Ok ... ich meinte eigentlich nur, die erste Möglichkeit ist, dass in einem Nachfolgeknoten P gilt, in einem von dessen Nachfolgern !P etc. Aber die zweite Möglichkeit ist doch dann, dass im Nachfolger !P gilt, in dessen Nachfolger dann P etc., d.h. die Forderung "abwechselnd P und !P" sagt nichts darüber aus, womit man beginnt. Oder?

Nein, aber das ist meiner Meinung nach nicht wichtig, denn beide Formeln würden die Aufgabe erfüllen ;]

[tromba_marina]

Finde ich nicht. Die Formel soll doch sowohl Pfade erkennen können, die mit einem P-Knoten beginnen, als auch Pfade, die mit einem !P-Knoten beginnen, und nicht nur einen der beiden Typen. Kann doch gut sein, dass ein Graph mehrere solche Kantenzüge enthält, und zwar von jedem der beiden Typen mindestens einen. Ich verstehe ehrlich gesagt gerade nicht, wo das Problem liegt -- es geht doch nur darum, hinter die Formel nochmal (mit ODER verknüpft) dasselbe zu schreiben, nur dass im hinteren Teil P durch !P ersetzt wird.