Neue Frage

Correct Counterexamples for formula

gefragt 2017-08-25 19:35:08 +0200

td Gravatar-Bild

Hey there,

Like in Problem 7 of the last exam (2.2017) I can follow the given solution, but I am not sure if mine is also correct. Can someone just check them and give maybe short comments? Would the explanation below be sufficient to get the points in the exam?



s1 is satisfied, because on all paths Ga or F!a holds

s2 is not satisfied, because the path 0(2)^w does not hold, since Ga is false and !a is also false in the initial state.


[$\phi$ SU $\psi$] is only true, if we have $\phi$*$\psi$, which means, that somewhere $\psi$ must hold.

[$\phi$ WU $\psi$] on the other side is also true, if we have only $\phi$.

Therefore s1 is not satisfied, because b never holds.The same is true for s2 except we have GFa here and in state 1 a holds indeed infinity often. So s2 is satisfied


S1 is satisfied, because IF at some time t a holds, in t+1 b must hold.

S2 is not satisfied, because in the next Step (which is one after the initial state) a has to hold if and only if b holds finally. But we are in an endless loop of b, so a cannot hold. The right example doesn't show this, since in the next step a holds and then we reach the b-loop.


S2 is satisfied, because on all paths (we obviously have only one path) infinity often !b holds.

S1 is not satisfied, because there is no path, where after one step and some time finally !b holds always.


b never holds, so according to my understanding above [c SU b] never becomes true. This leads to A[ false SU a] which should be false as well. Therefore S2 is not satisfied. (Would it be satisfied, if the initial state is empty, which means false? Then [false SU c] would hold).

S1 is satisfied, because we have a sub-path (initial state) with only one c, which satisfies [c WU b] and then reach a.

In e) I am not 100% sure.. Thanks in advance for help.

bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort


geantwortet 2017-08-25 21:09:46 +0200

PS Gravatar-Bild

a) is fine but you could directly say that a is true at initial time on your path while Ga is not. Also, you do not need state 1 of your counterexample. Note that (G a) | !(G a) is simply true so that the first formula will reduce to Atrue which holds in all structures. Thus, you only need a structure that will falsify the other formula. To that end, a single path (the one you mentioned) will do as you can prove by checking the following LTL formula with the LTL prover tool:

a & (X G !a) -> !((G a) <-> a)

b) is true which you can also check like this:

!a &!b & (X G(a&!b)) -> ![(G a) SU b] & [(F a) WU b]

c) you are right with your first structure

a &!b & (X G(!a&b)) -> (F(a<->X b)) & !X(a<->F b)

and also right with your second (it satisfies both formulas):

!a & !b & X(a & !b) & (X X G (!a&b)) -> (F(a<->X b)) & X(a<->F b)

In your explanation the IF is however not right. The formula says that at some point of time t (in the path considered it is t=0), the formula a<->Xb should hold. Since a holds at t=0 and b at t=1 it is true.

d) you are also right with this (note that on a single path structure with an infinite path, you can neglect A and E and just consider the LTL formula obtained that way):

b & G(!b<-> X b) -> (G F X !b) & !(X F G!b)

e) again you are right:

!a&!b&c & (X G(a&!b&c)) -> [[c WU b] SU a] & ![[c SU b] SU a]

and here is the answer to you question

!a&!b&!c & (X G(a&!b&c)) -> ![[c SU b] SU a] & G![c SU b]

seems that you will get your points ...

bearbeiten Als beleidigend melden löschen publish Link mehr


Thank you very much for your answer!

td ( 2017-08-25 21:42:07 +0200 )bearbeiten

I have a doubt regarding the question. For the last question why !a&!b&c & (X G(a&!b&!c)) wont satisfy for the [[c WU b] SU a]. Because c will satisfy [c WU b] and a is holding in the next state

SR ( 2017-08-26 22:40:43 +0200 )bearbeiten

In that structure, we have !a&!b&c & (X G(a&!b&!c)) -> G(![c WU b] & ![c SU b]) & ![[c WU b] SU a] & ![[c SU b] SU a] & X G([[c WU b] SU a] & [[c SU b] SU a]). Note that a is false at t=0, and since b is also false there, we need G c to satisfy [c WU b] at t=0, but c only holds at t=0 and not for t>0.

PS ( 2017-08-27 10:36:06 +0200 )bearbeiten

Thank you so much.

SR ( 2017-08-27 11:42:02 +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-25 19:35:08 +0200

Gesehen: 34 mal

Letztes Update: Aug 25