VRS Sheet 8 Q1 LTL Semantics

Question

I've solved these questions but the answers are incorrect. Can anyone guide me on where I am doing wrong?

Q1: [[c SU b] WU a]

A1: G(!a & b & !c); G(!a & b & !c)

Q2: [c SB [a SB b]]

A2: G(a & !b & !c); G(!a & !b & c)

Answer 1

Please repeat the question of the exercise sheet so that also students of later semesters can understand what we are discussing here. The question is that for a given LTL formula φ, we should construct two LTL formulas φ1 and φ2 that satisfy the following requirements:

1. φ1 and φ2 are not equivalent
2. φ1 and φ2 are both satisfiable
3. φ1->!φ and φ2->!φ are valid

For the given formula φ=[[c SU b] WU a], you suggest φ1=G(!a & b & !c) and φ2=G(!a & b & !c) which does obviously violate the first requirement: The formulas are even syntactically the same, so they are definitely equivalent. 

For the second formula φ=[c SB [a SB b]], you suggest φ1=G(a & !b & !c) and φ2=G(!a & !b & c) which are satisfiable and not equivalent. Also, φ1->!φ is valid, but φ2->!φ is not valid: A counterexample is a single path where always !a&!b&c holds which obiviously satisfies φ2 but also satisfies φ.

Comments

Thanks for the help. I've updated my questions as per your instructions for other students.