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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

is below right way for above diagram?

(!a&!b&!c)& X(!a&!b&c) & G((X(!a&!b&c) <-> X(!a&!b&!c)))

Thank you.

in # Study-Organisation (Master) by (770 points)

1 Answer

0 votes

Definitely not. Look, the sub formula behind the G-operator is false, since it states that all all points of time, except for the initial one, we should have (!a&!b&c) <-> (!a&!b&!c), but c cannot be true and false at the same time. 

Let us first define

  • s0 := !a&!b&!c
  • s1 := !a&!b&c
  • s2 := !a&!b&!c ( = s0)
Then, I would write instead something like
    s0 & (X s1) & (X X s2) & X G ((s1 -> X s2) & (s2 -> X s1))
The above can be generalized to any kind of counterexample that you will be given by the LTL prover. It describes an initial prefix that is followed by a cycle.
In the above case, this is however not required, since s0=s2 holds (the LTL tool does not generated the smallest possible counterexample). Hence, it should be sufficient to write
    s0 & G((s0 -> X s1) & (s1 -> X s0))
by (170k points)

Related questions

0 votes
1 answer
asked Jun 21, 2020 in # Study-Organisation (Master) by RS (770 points)
0 votes
1 answer
asked Aug 26, 2023 in * TF "Emb. Sys. and Rob." by calvet (250 points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...