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


529 users

0 votes

In Feb 2022 exam, for problem 8e (Translate the following formula to an equivalent µ-calculus formula), is the above solution correct?

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

1 Answer

0 votes

Your computation is almost fine! The difficult parts are fine, but there is a flaw in your computation. 

First of all, consider G[a WB b] which holds if at any point of time t, "a" holds before "b" or G!b holds at time t. If G!b should not hold at time t, then !G!b holds, i.e., F b holds at time t, and therefore there is a point of time t+d where b holds. At that point of time t+d, it is however not possible that [a WB b] holds, and therefore, it is not possible that G!b does not hold at some time t. Thus, G!b must always hold so that G[a WB b] is equivalent to G!b.

In particular, G[a WB F X b] is therefore equivalent to G !F X b. Good that you have seen this, since this simplifies matters. Because of this, we then get 

    A G[a WB F X b] 
    = A G !F X b
    = A G !X F b
    = A G !F X b
    = A G G X !b
    = A G X !b
    = A G A X !b

and since that is CTL, it is not difficult to get a µ-calculus formula from here. 

However, G !X F b is not equivalent to G !F b. Note that G !X F b is equivalent to GX!b (as explained above), while  G !F b is equivalent to GG!b which is equivalent in turn to G!b. However, GX!b holds if b is initially true and then always false, which does not satisfy G!b.

by (166k points)

Related questions

0 votes
1 answer
+1 vote
1 answer
asked Aug 17, 2020 in * TF "Emb. Sys. and Rob." by dardan (150 points)
0 votes
1 answer
Imprint | Privacy Policy