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

868 questions

986 answers


438 users

0 votes

While looking at paper solutions to translate formulas to Mu-calculus, I observed the (nu y. <>y) -> part is considered in the answers provided in the paper dated 27.08.2019 (indicated in the left image).

However, in 31.08.2021 (right image), we omit the  (nu y. <>y) -> part because of the implies.

Is it an accepted answer in the exam if we solve it either way? Thanks in advance.

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

1 Answer

0 votes
Best answer
Formally, the Phi_Inf formula is required in the ยต-calculus formulas, but one can also do without if the results are corrected afterwards in that the finally deadend states are added to all A-formulas and are removed from all E-formulas. In the example solutions we are therefore a bit sloppy with this formula. To be save, please add Phi-inf, or explain where it should be added if not written there explicitly.
by (139k points)
selected by
Thanks for the clarification.
Imprint | Privacy Policy