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
b) S1=S1=[c WB [b WB a]]
S2=S2=[c SB [b SB a]]
How to solve this?
