More precisely, if F is a temporal formula, then |= F asserts that F is true for all behaviors.