 Now, combining (SP1) and (SP2) together we have a way of deciding whether a PDL formula A is satisfiable. It suffices to run them in parallel: if A is satisfiable then (SP2) will eventually answer “yes”, if A is not satisfiable then (SP1) will eventually answer “no”. The procedure halts when either (SP1) or (SP2) provides an answer.