Coalgebraic specifications and models of deterministic hybrid systems

Coalgebraic specification and semantics, as used earlier for object-oriented programming, is extended with temporal aspects. The (non-temporal) expression ``s.meth'' expressing that method ``meth'' is applied in state s, is extended to an expression ``s.metha'', where a is a time parameter. It means: in state s let the state evolve for a units of time, and then apply method meth. With this formalism we specify various (elementary) deterministic hybrid systems (and give a few simulations). We also define a notion of model for such a specification, and define what it means for a model to be terminal. Terminal models are ``optimal'' in the sense that they involve a minimal set of states, as will be illustrated in a number of examples. This shows that standard model theory can be applied to temporal (coalgebraic) specifications.