\EE y : Phi is the temporal formula obtained by hiding the variable y in the temporal formula Phi. This formula is true for a behavior iff there exist some values for y that would make the behavior satisfy Phi.

               Click here for Explanation Mode       You are in Definition Mode