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


546 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 (166k points)
selected by
I understood.
Thank you for clarifying this.

Related questions

Imprint | Privacy Policy