I've got some questions about the temporal operators in computation tree logic:
- Does the F
qhas to hold in a subsequent state or is it also fulfilled when
qholds in the current state?
Please consider the following example:
What exactly is specified here? Does it mean: If
q AND rholds on a path
Pin a graph
qhas to hold somewhere on the subsequent path of
P. Or does it mean: ...
qhas to hold somewhere on the subsequent path of every path of