Coalgebraic semantics for timed processes

We give a previous termcoalgebraicnext term formulation of timed processes and their operational previous termsemanticsnext term. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”, which amount to partial monoid actions of the time domain or, equivalently, coalgebras for an “evolution comonad” generated by the time domain. All our examples of time domains satisfy a partial closure property, yielding a distributive law of a monad for total monoid actions over the evolution comonad, and hence a distributive law of the evolution comonad over a dual comonad for total monoid actions. We show that the induced coalgebras are exactly timed transition systems with delay operators. We then integrate our previous termcoalgebraicnext term formulation of time qua timed transition systems into Turi and Plotkin’s formulation of structural operational previous termsemanticsnext term in terms of distributive laws. We combine timing with action via the more general study of the combination of two arbitrary sorts of behaviour whose operational previous termsemanticsnext term may interact. We give a modular account of the operational previous termsemanticsnext term for a combination induced by that of each of its components. Our study necessitates the investigation of products of comonads. In particular, we characterise when a monad lifts to the category of coalgebras for a product comonad, providing constructions with which one can readily calculate.