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
Hello,

I have a doubt in converting the below formula in CTL.

¬AXX(GF(¬E[1 U (E¬a)]))

= ¬AXX(GF(¬E[1 U (¬a)]))

can we write [1 U (¬a)]  as F(!a) and then F(!a) as !a?

Thanks in advance.
in * TF "Emb. Sys. and Rob." by (300 points)

1 Answer

0 votes
Well, it depends: If the U is a strong-until, let's write SU for that, then we have [1 SU q] = (F q) since (F q) demands that at some point of time on a path, q holds, and [1 SU q] asks for the same (since the additional demand that 1 must hold until that point of time is trivially true).

However, you cannot write F(!a) as !a: The formula !a means that !a holds at the first point of time (and nothing is stated about any other point of time), and F(!a) means that !a holds at some point of time, which may be the first point of time, but also any other one. Hence, we have (!a) -> F(!a), but not the converse.
by (170k points)
Okay got it, thank you so much.
One more question: So, if we have G(!a) then can we write as (!a)?.

Thanks in advance.
No, you cannot. G(!a) means that a is always false, i.e., false at all points of time while !a just means that a is false at the initial point of time.
Thank You very much!

Related questions

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