Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

870 questions

988 answers


439 users

+2 votes

I have a problem with the following exercise:

S1=X b & G c
S2=G b & F c

I'm trying to find 2 formulas which satisfy S2 but not S1.

I tried the following 2 formulas:

  • !c&G(b)&X(c)
  • G(b)&F(c)&!G(c)

The LTL Tool says that 

  • G(b)&F(c)&!G(c) -> G b & F c & !(X b & G c) is valid
  • !c&G(b)&X(c) -> G B & F C & !(X B & G C) is valid as well.

However, the student portal gives me the following error: "Please check whether your LTL formula fulfill the requirements."

Which requirements do my formulars not fulfill?

in * TF "Emb. Sys. and Rob." by (1.7k points)
I have the exact same problem
It would be too simple to allow !S1&S2 as one of the two formulas, but one your formulas is equivalent to that.

1 Answer

+2 votes
Best answer

Very tricky. For your formulas phi1 and phi2, we can check that they are satisfiable, they are not equivalent and both imply !S1&S2. So, what is wrong here?

Read carefully the exercise problem. The formulas should satisfy 

phi[i] -> !S1&S2 

but that should be strict, i.e., the formulas should **not** satisfy

phi[i] <-> !S1&S2

However, this is the case with your formula phi2.

by (139k points)
selected by
Thank you. I simply added "&c" in the second formula, therefore the Implication still holds but the formulas are no longer equivalent.

Related questions

+2 votes
1 answer
+1 vote
1 answer
0 votes
1 answer
asked Aug 26, 2021 in * TF "Emb. Sys. and Rob." by KB (280 points)
Imprint | Privacy Policy