Unterschied dynamische Logik vs. temporale Logik?

[Senior Sanchez]

Hi,

Ich lerne immernoch fleißig und gerade frage ich mich, wo denn die genauen Unterschiede zwischen der dynamischen Logik und der temporalen Logik liegt. Kann mir da jemand weiterhelfen? Danke

[Senior Sanchez]

So, ich beantworte das mal selber.

Also sowohl die dynamische als auch die temporale Logik stellen Erweiterungen bzw. eher besser besondere Interpretationen der Modallogik dar.

Die Modallogik kann ja mögliche und notwendige Aussagen über ihre Operatoren abbilden. Die temporale Logik benutzt diese Operatoren dagegen um zeitliche Abläufe für die Vergangenheit oder die Zukunft zu modellieren. So wird aus dem möglich ein "irgendwann" und aus dem notwendig ein "von jetzt an immer".

Die dynamische Logik arbeitet auch mit diesen Operatoren, beschreibt darüber aber keine zeitlichen Abläufe sondern Aktionen/Befehle. So können Aktionen möglicherweise oder eben zwingend ausgeführt werden. Das nutzt man vor allem zur Programmverifikation.

[Aquaschaf]

Eine modale Logik lässt sich ja durch eine Kripke-Struktur beschreiben. Temporale Logik ist der Spezialfall bei dem die Relation der Kripke-Struktur eine strikte Quasiordnung ist. Und bei einer dynamischen Logik gibt es nicht nur eine Relation, sondern unendlich viele.

[Senior Sanchez]

Jo, mit ner Kripke-Struktur geht so etwas, da diese ja die möglichen Welten beschreiben kann.
Was meinst du damit, dass dieRelation der Kripke-Struktur eine strikte Quasi-Ordnung ist?

[Aquaschaf]

Eine Kripke-Struktur besteht aus einer Zustandsmenge, einer Relation und einer Interpretationsfunktion. Bei einer temporalen Logik ist die Relation irreflexiv und transitiv, während sie bei einer modalen Logik beliebig ist.

[Senior Sanchez]

Wie ne Kripke-Struktur aufgebaut ist, weiß ich ja, wobei ich das als Quadrupel kenne, also das noch eine aktuelle Weltrepresentation (wohl der Startzustand) definiert wird. Wie ist das genau zu verstehen, dass die temperale Logik irreflexibel und transitiv ist? Das sich kein Zustand auf sich selber abbilden kann und eben eine Transitivität herrscht. Inwiefern ist das bei einer modalen Logik beliebig?
Sagt das somit im Grunde aus, dass ich einer temporalen Logik eine mögliche Reihenfolge der möglichen Zustände habe und nicht direkt zu einem früheren Zustand zurückkehren kann wie es bei einer modalen Logik der Fall wäre?

Die dynamische Logik entspricht dann in diesem Fall mehr der modalen Logik (klar ist ja auch selber ne modale Logik), oder?

Sorry, falls die Fragen etwas doof kommen, aber ich muss son Kram wissen ohne vorher Logik gehabt zu haben :(

[Aquaschaf]

Vielleicht stifte ich nur unnötige Verwirrung. Ich weiß ja nicht ob ihr das überhaupt auf dieser Ebene von Definitionen wissen müsst. Die Relation der Kripke-Struktur definiert welcher Zustand von welchem erreichbar ist. Temporale Logik ist eben der Spezialfall bei dem die Relation den genannten Bedingungen genügt. Mehr Klarheit eventuell hierdurch:

- Modale Logik (oder Modallogik) ist ein Oberbegriff. Sowohl temporale Logiken als auch dynamische Logiken sind Modallogiken.
- Die Einschränkung bei temporaler Logik kann man sich so vorstellen (wie du selbst schreibst) dass die Zustände auf einem "Zeitstrahl" liegen.

[Senior Sanchez]

Vielleicht stifte ich nur unnötige Verwirrung. Ich weiß ja nicht ob ihr das überhaupt auf dieser Ebene von Definitionen wissen müsst. Die Relation der Kripke-Struktur definiert welcher Zustand von welchem erreichbar ist. Temporale Logik ist eben der Spezialfall bei dem die Relation den genannten Bedingungen genügt. Mehr Klarheit eventuell hierdurch:

- Modale Logik (oder Modallogik) ist ein Oberbegriff. Sowohl temporale Logiken als auch dynamische Logiken sind Modallogiken.
- Die Einschränkung bei temporaler Logik kann man sich so vorstellen (wie du selbst schreibst) dass die Zustände auf einem "Zeitstrahl" liegen.

Joar, okay, so habe ich das auch verstanden :) Vielen Dank für die Erklärung.

Kannst du mir dann noch kurz sagen, inwiefern die dynamische Logik dann anders ist als die temporale Logik? Das ist dann sicherlich so, dass es keine "feste" Zustandsfolge wie bei der temporalen Logik gibt, richtig?

[Aquaschaf]

Kannst du mir dann noch kurz sagen, inwiefern die dynamische Logik dann anders ist als die temporale Logik? Das ist dann sicherlich so, dass es keine "feste" Zustandsfolge wie bei der temporalen Logik gibt, richtig?

Wie gesagt, bei dynamischer Logik gibt es unendlich viele (Zustandsübergangs-)Relationen. Es ist dann aus der jeweiligen Formel abzulesen welche angewendet werden muss. Darüber wie die Relationen aussehen gibt es keine Einschränkungen.

[Senior Sanchez]

Mir ist noch ne Frage gekommen. Die CTL ist ja ne verzweigte dynamische Logik und benutzt neben den Temporaloperatoren eben noch den All- und den Existenzquantor.
(! soll die Negation sein)

Meine Frage ist jetzt folgende: ist !AF Prädikat das gleiche wie AF !Prädikat?

[Gast]

Hi,

also CTL, LTL, CTL*, mu-Kalkuel sind erstmal Temporallogiken,
wobei man im Fall von Aktionen auch von dynamischen Logiken reden kann,
wenn ich die Definition auf Wikipedia als richtig annehme bzw. richtig verstehe.

Verwenden kann man alle zur Verifikation, das Programm wird einfach
als gerichteter (meist endlicher) Graph mit entsprechenden Knotenlabeln
(rein propositional) oder/bzw. Kantenlabeln (was dann wohl als dynamisch
bezeichnet wird) modelliert, was man dann auch als Kripke-Struktur bezeichnet (So kenn ich das aus Buechern ueber Modelchecking/formale Verifikation. Der Sprachgebrauch kann natuerlich bei Logikern/Philosophen anders sein).

Wenn man von User-Eingaben abstrahiert, sollte man eigentlich immer auf Aktionen verzichten koennen.

Und zu der Frage !AF phi:

AF phi = auf allen Pfaden wird irgendwann ein Zustand erreicht, in dem phi gilt

Negation: es existiert ein Pfad, auf dem immer !phi gilt, also:
EG !phi

Lustiger ist es E[ phi U psi] zu negieren ;)

[Senior Sanchez]

Und zu der Frage !AF phi:

AF phi = auf allen Pfaden wird irgendwann ein Zustand erreicht, in dem phi gilt

Negation: es existiert ein Pfad, auf dem immer !phi gilt, also:
EG !phi

Das ist mir soweit ja klar ;)
Ich frage mich nur ob !AF phi eben das gleiche ist wie AF !phi.

[Senior Sanchez]

Vielen Dank für eure Hilfe. :)
In der Genauigkeit kam das heute gar nicht dran und ich hab die Prüfung mit 1.0 bestanden. :)

Also nochmals danke.

[Gast]

Vielen Dank für eure Hilfe. :)
In der Genauigkeit kam das heute gar nicht dran und ich hab die Prüfung mit 1.0 bestanden. :)

Also nochmals danke.
Glueckwunsch,

und wegen deiner Frage: !AF phi (bzw EG!phi) ist nicht dasselbe wie AF!phi.

Es kommt allerdings bisschen darauf an, wie du genau die Semantik
einer CTL-Formel definierst.
Wenn du nur unterscheidest zwischen Kripke-Struktur
erfuellt CTL-Formel j/n, dann gilt z.B.:
EG !phi impliziert AF !phi,
da dann jede Kripkestruktur, die EG!phi erfuellt,
!phi im Startzustand erfuellen muss,
womit der Startzustand aber auch AF !phi erfuellt,
so dass auch die Kripkestruktur AF !phi erfuellt (unter der Annahme, dass
man nur genau einen Startzustand hat).

Ueblicherweise definiert man aber die Semantik als die Menge
von Zustaenden der Kripkestruktur, die die CTL-Formel erfuellen.
Dann sind beide Formeln echt verschieden.

Waehle z.B. phi als atomare Proposition 'a' und die Kripkestruktur wie folgt:

Zustaende: {1,2}
Kanten: 1->2, 2->2
'a' soll in 2 gelten, damit '!a' in 1

Dann gilt [[EG!a]] = {} und [[AF!a ]] = {1}.