# # 2016.02.17 prob8 . part d :

gefragt 2017-08-22 16:07:00 +0200

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

AX(a -> Fb) _ AX(a -> AFb)

isn't it != ? (look at the kripke in attached pic) I think the attached kripke satisfies the first formula but not the second one.

bearbeiten retag schließen löschen

## Kommentare

Please give some more information. What was the task? What should be not equal? And also, why do you think, it should be equal? Explain your thinking, then others can really say if you've understood it and not only confirm a guess ;)

( 2017-08-22 16:14:53 +0200 )bearbeiten

The question is updated with the task you requested. I think the given Kripke can distinguish the difference between them.

( 2017-08-22 16:28:36 +0200 )bearbeiten

## 1 Antwort

geantwortet 2017-08-22 18:15:33 +0200

Hmh, I think that you are wrong and that the solutions given for that problem are correct. Look at your Kripke structure

Looking at your structure (I hope that I have added the arrows above correctly), I get the following

• 〖a〗= {s1;s2;s3;s4;s6}
• 〖b〗= {s5}
• 〖A F b〗=〖µx.(b∨[]x)〗= {s4;s5}
• 〖a -> A F b〗 = {s0;s4;s5}
• 〖A X(a -> A F b)〗 = {s4}

Looking at the other formula, we first consider the two essential paths that start in the initial state s0.

• On the path s0,s1,s2,s3,s3..., the formula a->Fb holds only at the initial point of time since a is false there. At all other points of time, a holds, but Fb is false, so that the formula a->Fb is also false.
• On the path s0,s1,s4,s5,s6,s6,..., the formula Fb holds from s0 up to s5 (including s5). Also, the formula a->Fb holds from s0 up to s5 (including s5), but no longer from s6.

Hence, A X(a -> F b) is also false in s0, since there is an infinite path (the path s0,s1,s2,s3,s3...) that does not satisfy X(a -> F b). Since also A X(a -> A F b) does not hold in s0, you do not have a counterexample.

Indeed, both formulas are equivalent which can be proved as shown in the given solutions to that example.

mehr

## 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]

## Statistik

Gefragt: 2017-08-22 16:07:00 +0200

Gesehen: 50 mal

Letztes Update: Aug 22 '17