0 votes

The given LTL formulas S1S1 and S2S2 are not equivalent.
LS1¬S2LS1∧¬S2 represents a set of ωω-words that only satisfy S1S1.
L¬S1S2L¬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φ1Lφ2Lφ1≠Lφ2
  • Lφi{}Lφi≠{}
  • Case 1: Lφ1LS1¬S2Lφ1⊊LS1∧¬S2 and Lφ2LS1¬S2Lφ2⊊LS1∧¬S2
    or
    Case 2: Lφ1L¬S1S2Lφ1⊊L¬S1∧S2 and Lφ2L¬S1S2Lφ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?

in * TF "Intelligent Systems" by (280 points)

1 Answer

0 votes
by (91.8k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
2 answers
Imprint | Privacy Policy
...