0.5 Using temporal logic to specify properties  (Page 8/11)

For each of these problems, there are many equivalent formulas,some of which are easier to verify as equivalent than others.

• $\square b$
• $◇((\square b\square b)(\square p\square p)(\square r\square r)(\square s\square s)\square e)$ . Remember that if we're in an end-state, then it doesn'tcount as deadlock.
• $\square ◇(p_1{p}_2)(\square ◇p_1\square ◇p_2)$ . In fact, SPIN provides a built-in variable np_ , which corresponds to``all processes are in a non-progress state''. When SPIN does its built-in check for non-progress cycles,it actually just verifying !<>[]np_ . You might recall that SPIN's idea of progress is state-based, not transition-based:SPIN (counterintuitively) considersit progress when a process does nothing but squat in a progress state. (This can only happen if weak fairness is not beingenforced, or a guard is being labeled as progress.) How might we capture ``progress'' but stillpreclude those traces which just sit idly at a progress label? We could add a second progress label immediately following $p_1$ , call it $q_1$ . Similarly, we can introduce $q_2$ . Then we could verify that $((\square ◇p_1\square ◇q_1)(\square ◇p_1\square ◇q_1))$ . (This assumes that all labels are private to each process.)
• ``It's always not the case that $r$ is always on, and yet $s$ doesn't happen an infinite number of times'': $\square (\square r\square ◇s)$ . One equivalent formula is``if $r$ stays on forever, then it's being serviced infinitely often.'': $\square (\square r\square ◇s)$ .
• $(\square ◇r\square ◇s)$