# Exercize 8 Problem 1(b)

As my understanding i tried my best. But the tool is not accepting the result. Can you please tell me where i did wrong?

In a state with ¬b and c (on any infinite path)  both [ c SB b ] and [c WB b ] are satisfied. The difference between these two formulas is that the SB formula requires c to hold eventually while WB is happily waiting for c forever as long as b doesn't come along and ruin everything.

See slides 16 and 17 of the Temporal Logic chapter.

Thus, neither of formulas is satisfied (by the first of your two answers). The task was to satisfy precisely one of the two formulas.

Your second answer isn't correct either. As you have a formula of the form F G something, G something is satisfied after finitely many steps. Before that anything may happen. The formula may already be satisfied or not.

by (25.6k points)
edited by

To give some help and instructions how to use the tool, consider the following: Given formulas S1=[a WB [c WB b]] and S2=[a WB [c SB b]], we first check whether the one implies the other one.

The tool quickly tells us that [a WB [c WB b]] -> [a WB [c SB b]] is valid, while we get a counterexample for [a WB [c SB b]] -> [a WB [c WB b]]. That counterexample consists of an infinite path where G(!a&!b&!c) holds. Hence, we know that

• G(!a&!b&!c) -> [a WB [c SB b]]
• G(!a&!b&!c) -> ![a WB [c WB b]]

which is also easily seen with the semantics of the WB and SB operators. Hence, we already have a first formula to distinguish between the two formulas. To find a second one, we ask the tool whether this is the only counterexample in that we let the tool check the following

!G(!a&!b&!c) -> ([a WB [c SB b]] -> [a WB [c WB b]])

A counterexamle would satisfy !G(!a&!b&!c) & [a WB [c SB b]] & ![a WB [c WB b]]. The tools gives a counterexample which is an infinite path where G(a&!b&!c) holds. So, we have a second counterexample.

If you want a third one, you may ask now

!G(!a&!b&!c) & !G(a&!b&!c) -> ([a WB [c SB b]] -> [a WB [c WB b]])

This time, we get a counterexample with two alternating states which may be described with the following LTL formula:

(!a&!b&!c) & G( ((!a&!b&!c) -> X(a&!b&!c)) & ((a&!b&!c) -> X(!a&!b&!c)))

This way, you can construct many counterexamples or models that satisfy a formula like !S1&S2.

by (166k points)