Differential Equations as Actions

We extend a conventional action system with a primitive action consisting of a differential equation and an evolution invariant. The semantics is given by a predicate transformer. The weakest liberal precondition is chosen, because it is not always desirable that steps corresponding to differential actions shall terminate.

It is shown that the proposed differential action has a semantics which corresponds to a discrete approximation when the discrete step size goes to zero. The extension gives action systems the power to model real-time clocks and continuous evolutions within hybrid systems.