Figure 3: Axiom DS is incorrect as stated, because it does not ensure that the existentially quantified t does not affect the game c. DS should have been any of the following axioms instead
DS p(x,x') <-> \exists t>=0 p(x,x')
DS T <-> \exists t>=0 T
DS T <-> \exists t>=0 T
In the latter version t:=* is the nondeterministic assignment that for a fresh variable t is definable via an ODE t'=1;t'=-1.