LTL Equivalence Exercise 8 1a

Question

The given LTL formulas S1S1 and S2S2 are not equivalent.
LS1∧¬S2LS1∧¬S2 represents a set of ωω-words that only satisfy S1S1.
L¬S1∧S2L¬S1∧S2 represents a set of ωω-words that only satisfy S2S2.

Please construct two LTL formulas φ1φ1 and φ2φ2 that satisfy the following requirements:

• Lφ1≠Lφ2Lφ1≠Lφ2
• Lφi≠{}Lφi≠{}
• Case 1: Lφ1⊊LS1∧¬S2Lφ1⊊LS1∧¬S2 and Lφ2⊊LS1∧¬S2Lφ2⊊LS1∧¬S2
  or
  Case 2: Lφ1⊊L¬S1∧S2Lφ1⊊L¬S1∧S2 and Lφ2⊊L¬S1∧S2Lφ2⊊L¬S1∧S2

where LφiLφi represents a set of ωω-words that satisfy φiφi.

Please use ';' to seperate the LTL formulas.
For Case 1, submit your solution in the form:
1 ; G (!a) ; F b
For Case 2, submit your solution in the form:
2 ; G (!a) ; F b

You can use the LTL online training tool to check your solution.

For the syntax of CTL/LTL and the mu-calculus formulas, see the Quartz reference card under section proof goals/specifications.
In particular, note that you have to put a blank between CTL path quantifiers and temporal operators like 'E G E X a'.

a) S1=S1=[b SU [c WU a]]
S2=S2=[b SU [c SU a]]
Assumed that the alphabets ΣΣ is the set of variables that appear in the formulas.

While solving this, I got the answer as 1;G(a&!b&!c).

How's this incorrect, please? Can someone share steps to solve this?

Comments

The exercise asks for submitting an answer 1;phi;psi or 2;phi;psi with two formulas phi and psi while you only submitted 1;G(a&!b&!c).

Answer 1

Well, have a look at https://q2a.cs.uni-kl.de/2418/exercize-8-problem-1-b.

Simply adapt that to your problem: Given formulas S1=[b SU [c WU a]] and S2=[b SU [c SU a]], we first check whether the one implies the other one.

The tool quickly tells us that [b SU [c SU a]] -> [b SU [c WU a]] is valid, while we get a counterexample for [b SU [c WU a]] -> [b SU [c SU a]] so that S1&!S2 is satisfiable. That counterexample consists of an infinite path where G(!a&!b&c) holds. Hence, we know that the following are valid:

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

which is also easily seen with the semantics of the LTL operators. Hence, we already have a first formula to distinguish between the two formulas, namely G(!a&!b&c).

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) -> ([b SU [c WU a]] -> [b SU [c SU a]])

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

So, since S1&!S2 is satisfiable, we have case 1 mentioned in the exercise, so that your answer could be

1; G(!a&!b&c); G(!a&b&c)

Right?