 Another example, referring to all computations in the system, is: “If the process \(\sigma\) is eventually enabled on some computation starting from the current state, then on every computation starting there, whenever \(\sigma\) is enabled, it will remain enabled until the process \(\tau\) is disabled”. This property can be formalized in CTL* as