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
  1. AF[a & Xa] = mu y. (a | []y) & [](a | y)

 From slides we know that, #1 is correct but in solution of February 2017, 8b it is written as following:

AF[a & Xa] = mu y. (a | []y) & (!a | [](a | y))

Please confirm which one is correct.

https://es.cs.uni-kl.de/teaching/vrs/exams/2017.02.15.vrs/2017.02.15.vrs.exam.pdf

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

1 Answer

+1 vote
 
Best answer

I think that both are correct.

And I can justify this claim also: Just consider the two body formulas (a | []y) & [](a | y) and (a | []y) & (!a | [](a | y)) and make a case distinction to prove (a | []y) & [](a | y) = (a | []y) & (!a | [](a | y)):

  1. a=0: then, we get ([]y) & [](y) = ([]y) which is true
  2. a=1: then, we get (1) & [](1) = (1) & ([](1)) which is also true
So, the fixpoints are the same.
by (170k points)
edited by

Related questions

Imprint | Privacy Policy
...