I've got some questions about the temporal operators in computation tree logic:
- Does the F
inally
path-specific quantifierFq
mean thatq
has to hold in a subsequent state or is it also fulfilled whenq
holds in the current state? Please consider the following example:
What exactly is specified here? Does it mean: If
q AND r
holds on a pathP
in a graphG
thenq
has to hold somewhere on the subsequent path ofP
. Or does it mean: ...q
has to hold somewhere on the subsequent path of every path ofG
?