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

935 questions

1.1k answers

1.4k comments

442 users

0 votes

How FGb is translated to EFGb ?

Does that mean FGb can be written as EFGb ?

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

1 Answer

+2 votes
 
Best answer

FG b is not equivalent to EFG b, since the former is a path formula and the latter is a state formula. Above, the context makes the two exchangeable. The E quantifier comes from the outer A quantifier and is generated by the following rule (page 42):

A[ψ B φ] = A[ψ B (Eφ)]

by (144k points)
selected by
I understood.
Thank you for clarifying this.

Related questions

Imprint | Privacy Policy
...