Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers


424 users

0 votes



S1=S1=[b WB [a WB c]]

S2=S2=[b SB [a WB c]]

Assumed that the alphabets is the set of variables that appear in the formulas


When I check my LTL formulas in "LTL (Linear Temporal Logic) Tools", it gives me VALID answer but my answer is not being accepting by the exercise tool.

My answer: "1 ; G (!a & !b & c) ; G (a & !c) & G !b"

And my search queries in "LTL (Linear Temporal Logic) Tools" are:

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

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

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

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

Thank you.

in * TF "Emb. Sys. and Rob." by (1.7k points)
reshown by

1 Answer

0 votes
Best answer
Did you really try the above queries with the LTL tool? When I try it, then G (a & !c) & G !b -> [b WB [a WB c]] turns out not to be valid. A counterexample is of course a single path where always s&!b&!c holds so that G (a & !c) & G !b is satisfied on that path at the initial point of time. [a WB c] also holds at the initial point of time, since a holds there, but c does not. Therefore, [b WB [a WB c]] must be false, since it requires that [a WB c] must be false at the initial point of time.
by (117k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy