Neue Frage

CTL*/CTL/LTL question

gefragt 2017-08-23 17:51:28 +0200

Dieser Post ist als Wiki-Post markiert

Das ist ein Wiki-Beitrag. Jeder mit Karma >75 darf diesen Beitrag verbessern.

aktualisiert 2017-08-23 17:51:28 +0200

arsinux Gravatar-Bild

It seems to me that the solution provided here is wrong, because I think the solution satisfies both formulas. Would you please prove me wrong if I am mistaken? This does not mean that I am claiming that the formulas are equivalent. So please provide another counter example if the one here is wrong, and if it is correct please explain why.


bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort


geantwortet 2017-08-23 19:21:33 +0200

PS Gravatar-Bild

Using CTL model checking, you can quickly check that

  • 〖AG a〗 = {s2}
  • 〖AF AG a〗 = {s1;s2}

The meaning of these formulas should be clear: In general, AG a holds in all states where all outgoing infinite paths always satisfy a (which is only the case in s2), and AF phi holds in all states where all outgoing infinite paths at least once satisfy phi. In case of phi=(AG a), we seek the states where all outgoing infinite paths at least once visit state s2. That is true in states s1 and s2, but not in state s0, since there is the path that always loops in s0.

The formula AGFGa is equivalent to AFG a (you can use the LTL prover on to prove the equivalence G F G a <-> F G a). AFGa holds in all states where all outgoing infinite paths finally always satisfy a. That is true in state s0, since the first path which always loops in s0 satisfies the property, and the second path that leaves s0 (after looping there for some finite time), will have to reach s2 where it loops forever and therefore, it will also finally always satisfy a.

Hence, AGFGa holds in state s0, but AFAG a does not, and therefore the structure distinguishes between the two formulas.

bearbeiten Als beleidigend melden löschen publish Link mehr


Thanks! The explanation is persuasive, but then another question rises. Finding a solution for this question does not seem to be intuitive, at least for me. It makes sense to analyze the answer but to come up with an answer seems hard, Do you have any tips on that?

arsinux ( 2017-08-24 10:04:27 +0200 )bearbeiten

Well, there is an algorithmic way to decide these problems, but I would say that this would be overkill. It is best to carefully read the formulas and to try to intuitively find a difference. If that does not help, split it into a present and future part (by unwinding temporal operators).

PS ( 2017-08-24 12:19:20 +0200 )bearbeiten

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]


1 Follower


Gefragt: 2017-08-23 17:51:28 +0200

Gesehen: 34 mal

Letztes Update: Aug 23