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

1.1k questions

1.2k answers


543 users

0 votes

I have a question according to Sheet 8, Question 2 (b) - find 2 LTL counter-examples. 

For (b) it's:  S = [c WB [b WB a]]. The same example in exercise explanation, I understand how it works, but before it, I tried to solve by myself and I had the next intuition:

S = c WB [b WB a] = c WB [b SB a | G (!a)] = c SB [b SB a | G (!a)] | G(![b SB a | G (!a)]) - by definition of WB. Let's re-write it with abbreviation \psi = b SB a | G (!a):

S* = [c SB \psi] | [G (!\psi)]. I see here two formulas that correspond to !S:

1) G (!c) & G(\psi) - that breaks SB by definition (a SB b = !b U (a & !b)) and G (!\psi) as a consequence. One can re-write it as: G (!c & \psi)

2) \psi U c - breaks S* in the same way as 1).

I tried to submit the next solution: G(!c & ((b SB a) | G(!a))); [(b SB a) | G(!a)] U c and unfortunately parsing error arised. Could you please explain where I'm wrong?

in * TF "Emb. Sys. and Rob." by (270 points)

3 Answers

0 votes
Best answer

The syntax of the binary temporal operators always requires square brackets (see

Hence, using the correct syntax your thoughts are as follows with psi := [b SB a] | G !a 

    S = [c WB [b WB a]] 
      = [c WB [b SB a] | G !a] 
      = [c SB [b SB a] | G !a] | G!([b SB a] | G !a)
      = [c SB psi] | G!psi 

Now you claim that the following is valid (which is true):

    (G(!c&psi)) -> !([c SB psi] | G!psi)

which leads to your first formula G(!c&([b SB a] | G !a)).

Second, you use [c SB psi] = [!psi SU c & !psi] (which is right) and you claim that the following holds:

    [psi SU c] -> !([c SB psi] | G!psi)

which is not correct (I don't see why you think so). However, you may argue that

    !([c SB psi] | G!psi)
    = ![c SB psi] & !G!psi
    = [(!c) WU psi] & F psi
    = [(!c) SU psi]

and hence, you could use [(!c) WU psi] to prove

    [(!c) SU psi] -> !([c SB psi] | G!psi)

I guess that was what you wanted. 

However, also that will not be accepted by our clever tool, since even the following holds:

    [(!c) SU psi] <-> !([c SB psi] | G!psi)

Note that the implication must be a strict one (that was the main reason why the requirements were stated in terms of sets where we have a strict inclusion operator).  Hence, be careful with just doing equivalence transformations of the formulas.

by (166k points)
selected by
0 votes
That strongly depends on your implicit brackets.

If you claim  [b WB a] = [b SB a | G (!a)] and mean by it  [b WB a] = [b SB a] | G (!a), then you are right. If you mean  [b WB a] = [b SB (a | G (!a))], then you aren't right. A path satisfying b at some point but never a would satisfy the original formula  [b WB a] but not [b SB (a | G (!a))] as G(¬b) and hence also (a | G(¬b)) would be satisfied in the first step.

1. Assuming, your [¬b U (a & ¬b)] is [¬b SU (a & ¬b)].
2. Counterexample: c in the first step, never \psi. Then both [\psi SU c] and [\psi WU c] are satisfied but also [c SB \psi, G ¬\psi, and [c WB \psi] are satisfied.
by (25.6k points)
0 votes

Maybe here is a strategy that you had in mind: We unroll the temporal logic operator and create a DNF of the rest, then we negate that and pick the one or the other conjunct. That can give us quickly a couple of counterexamples.

For example, the given formula [c WB [b WB a]] will be converted as follows (note that [phi WB psi] = !psi & (phi | X[phi WB psi]):

    ![c WB [b WB a]]
    = !(![b WB a] & (c | X[c WB [b WB a]]))
    = !(!(!a & (b | X[b WB a])) & (c | X[c WB [b WB a]]))
    = !a&b | !a&X[b WB a] | !c&!X[c WB [b WB a]]

The final step requires some propositional logic simplifications, you may use whatever propositional logic tool to check that. Thus, we now have the following counterexamples:

  1. (!a&b) -> ![c WB [b WB a]]
  2. (!a&X[b WB a]) -> ![c WB [b WB a]]    
  3. (!c&!X[c WB [b WB a]]) -> ![c WB [b WB a]]
by (166k points)
Thank you! The best strategy for this task.

Related questions

0 votes
1 answer
asked Jun 16, 2020 in * TF "Emb. Sys. and Rob." by dardan (150 points)
0 votes
1 answer
0 votes
1 answer
asked Jun 18, 2020 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
Imprint | Privacy Policy