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

How are AF(a and Xa) and EG(a or Xa) translated? 
Could you let me know how to get to the step highlighted in the image below? 

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

1 Answer

+1 vote
Translating AF(a & X a) to mu-calculus is indeed not that trivial. It was asked here because it appears in the lecture slides (Temporal Logic Chapter, slide 36-37). There, you also find how that is translated to mu-calculus, we just unwind the formulas until we find a fixpoint:

    EG[φ∨Xφ]

    = E[(φ∨Xφ)∧XG(φ∨Xφ)]

    = E[(φ∧XG(φ∨Xφ))∨(Xφ∧XG(φ∨Xφ))]

    = E[φ∧XG(φ∨Xφ)]∨E[Xφ∧XG(φ∨Xφ)]

    = φ∧EXEG[φ∨Xφ]∨EX(φ∧EG[φ∨Xφ])

Replacing EG[φ∨Xφ] now with y yields a fixpoint equation y= φ∧EXy ∨ EX(φ∧y) which finally gives us the mu-calculus formula νy.(φ∧EXy ∨ EX(φ∧y)).
by (166k points)

Related questions

0 votes
1 answer
asked Aug 19, 2020 in * TF "Emb. Sys. and Rob." by mr.nice (440 points)
0 votes
1 answer
Imprint | Privacy Policy
...