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

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes
Hello,

I have one doubt regarding the below question.

• ϕ2 = ¬EFE[1 SU ¬a] ∧ AGA[a SB b]

= ¬EFE[1 SU ¬a] ∧ AGA[a SB b]

= ¬EFEF¬a ∧ AGA[a SB b]

= AGAGa ∧ AGA[a SB b]

 = AGAGa ∧ AG [a SB b]

 = AGa ∧ AG(Fa ∧ ¬b)

= AG(a ∧ ¬b)

In the last step, how we are getting AG(a ∧ ¬b) from AGa ∧ AG(Fa ∧ ¬b) ?. Is it because, "a & Fa" can be written as "a".?

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

1 Answer

+1 vote
As AG means “on every step of every infinite path”, we can use the well known conversion:

AGa ∧ AG(Fa ∧ ¬b)  = AGa ∧ AGFa ∧ AG¬b

As a implies Fa, AGa also implies AGFa (intuitively: whenever we satisfy AGa, we also satisfy AGFa, so it makes no difference in the conjunction). Hence, we just drop AGFa. And there you go, a beautifully hand-crafted:

AGa ∧ AG¬b
by (25.6k points)
Thank You so much for the explanation!

Related questions

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