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

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

+1 vote
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 (139k points)
selected by
I understood.
Thank you for clarifying this.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy